diff options
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/SMT-COMP/BitVector_ArraysEx.smt | 74 | ||||
| -rw-r--r-- | docs/SMT-COMP/BitVectors.smt | 187 | ||||
| -rw-r--r-- | docs/SMT-COMP/QF_AUFBV.smt | 19 | ||||
| -rw-r--r-- | docs/SMT-COMP/QF_BV.smt | 261 | ||||
| -rw-r--r-- | docs/doxygen.cfg | 1291 | ||||
| -rw-r--r-- | docs/intro | 10 | ||||
| -rw-r--r-- | docs/overview | 104 |
7 files changed, 1946 insertions, 0 deletions
diff --git a/docs/SMT-COMP/BitVector_ArraysEx.smt b/docs/SMT-COMP/BitVector_ArraysEx.smt new file mode 100644 index 00000000..a60413ca --- /dev/null +++ b/docs/SMT-COMP/BitVector_ArraysEx.smt @@ -0,0 +1,74 @@ +(theory BitVector_ArraysEx + + :written_by {Clark Barrett} + :date {May 7, 2007} + +:sorts_description { + All sort symbols of the form BitVec[m], + where m is a numeral greater than 0. + + All sort symbols of the form Array[m:n], + where m and n are numerals with m > 0 and n > 0. +} + +:funs_description { + All functions from the theory Fixed_Size_Bitvectors. +} + +:funs_description { + All function symbols with arity of the form + + (select Array[m:n] BitVec[m] BitVec[n]) + + where + - m,n are numerals + - m > 0, n > 0 +} + +:funs_description { + All function symbols with arity of the form + + (store Array[m:n] BitVec[m] BitVec[n] Array[m:n]) + + where + - m,n are numerals + - m > 0, n > 0 +} + +:preds_description { + All predicates from the theory Fixed_Size_Bitvectors. +} + + + :definition + "This is a theory containing an infinite number of copies of the theory of + functional arrays with extensionality: one for each pair of bitvector sorts. + It can be formally defined as the union of the SMT-LIB theory + Fixed_Size_Bitvectors and an infinite number of variants of the SMT-LIB + theory ArraysEx: one for each distinct signature morphism mapping the sort Index + to BitVec[m] and the sort Element to Bitvec[n] where m and n range over all + positive numerals. In each of the copies of ArraysEx, the sort Array is + renamed to Array[m:n] and each copy of ArraysEx contributes exactly one select + function and one store function to the infinite polymorphic family of select + and store functions described above. + " + + :notes + "As in the theory Fixed_Size_Bitvectors, this theory does not + provide a value for the formal attributes :sorts, :funs, and :preds because + there are an infinite number of them. See the notes in theory + Fixed_Size_Bitvectors for details. + + If for i=1,2, T_i is an SMT-LIB theory with sorts S_i, function symbols F_i, + predicate symbols P_i, and axioms A_i, by \"union\" of T_1 and T_2 + we mean the theory T with sorts S_1 U S_2, function symbols F_1 U F_2, + predicate symbols P_1 U P_2, and axioms A_1 U A_2 (where U stands for set + theoretic union). + + The theory T is a well-defined SMT-LIB theory whenever S_1, S_2, F_1, F_2, + P_1, P_2 are all pairwise disjoint, as is the case for the component theories + considered here. + " +) + + diff --git a/docs/SMT-COMP/BitVectors.smt b/docs/SMT-COMP/BitVectors.smt new file mode 100644 index 00000000..f2cde1b3 --- /dev/null +++ b/docs/SMT-COMP/BitVectors.smt @@ -0,0 +1,187 @@ +(theory Fixed_Size_BitVectors + +:written_by {Silvio Ranise, Cesare Tinelli, and Clark Barrett} + +:date {May 7, 2007} + +:notes + "Against the requirements of the current SMT-LIB standard this theory does + not provide a value for the formal attributes :sorts, :funs, and :preds. + The reason is that the theory has an infinite number of sort, function, and + predicate symbols, and so they cannot be specified formally in the current + SMT-LIB language. While extending SMT-LIB's type system with dependent + types would allow a finitary formal specification of all the symbols in + this theory's signature, such an extension does not seem to be worth the + trouble at the moment. As a temporary ad-hoc solution, this theory + declaration specifies the signature, in English, in the user-defined + attributes :sorts_description, :funs_description, and :preds_description. + " + +:sorts_description { + All sort symbols of the form BitVec[m], + where m is a numeral greater than 0. +} + +:funs_description { + Constant symbols bit0 and bit1 of sort BitVec[1] +} + +:funs_description { + All function symbols with arity of the form + + (concat BitVec[i] BitVec[j] BitVec[m]) + + where + - i,j,m are numerals + - i,j > 0 + - i + j = m +} + +:funs_description { + All function symbols with arity of the form + + (extract[i:j] BitVec[m] BitVec[n]) + + where + - i,j,m,n are numerals + - m > i >= j >= 0, + - n = i-j+1. +} + +:funs_description { + All function symbols with arity of the form + + (op1 BitVec[m] BitVec[m]) + or + (op2 BitVec[m] BitVec[m] BitVec[m]) + + where + - op1 is from {bvnot, bvneg} + - op2 is from {bvand, bvor, bvadd, bvmul, bvudiv, bvurem, bvshl, bvlshr} + - m is a numeral greater than 0 +} + +:preds_description { + All predicate symbols with arity of the form + + (pred BitVec[m] BitVec[m]) + + where + - pred is from {bvult} + - m is a numeral greater than 0 +} + +:definition + "This is a core theory for fixed-size bitvectors where the operations + of concatenation and extraction of bitvectors as well as the usual + logical and arithmetic operations are overloaded. + The theory is defined semantically as follows. + + The sort BitVec[m] (for m > 0) is the set of finite functions + whose domain is the initial segment of the naturals [0...m), meaning + that 0 is included and m is excluded, and the co-domain is {0,1}. + + The semantic interpretation [[_]] of well-sorted BitVec-terms is + inductively defined as follows. + + - Variables + + If v is a variable of sort BitVec[m] with 0 < m, then + [[v]] is some element of [{0,...,m-1} -> {0,1}], the set of total + functions from {0,...,m-1} to {0,1}. + + - Constant symbols bit0 and bit1 of sort BitVec[1] + + [[bit0]] := \lambda x : [0,1). 0 + [[bit1]] := \lambda x : [0,1). 1 + + - Function symbols for concatenation + + [[(concat s t)]] := \lambda x : [0...n+m). + if (x<m) then [[t]](x) else [[s]](x-m) + where + s and t are terms of sort BitVec[n] and BitVec[m], respectively, + 0 < n, 0 < m. + + - Function symbols for extraction + + [[(extract[i:j] s)]] := \lambda x : [0...i-j+1). [[s]](j+x) + where s is of sort BitVec[l], 0 <= j <= i < l. + + - Bit-wise operations + + [[(bvnot s)]] := \lambda x : [0...m). if [[s]](x) = 0 then 1 else 0 + + [[(bvand s t)]] := \lambda x : [0...m). + if [[s]](x) = 0 then 0 else [[t]](x) + + [[(bvor s t)]] := \lambda x : [0...m). + if [[s]](x) = 1 then 1 else [[t]](x) + + where s and t are both of sort BitVec[m] and 0 < m. + + - Arithmetic operations + + To define the semantics of the bitvector arithmetic operators, we first + introduce some additional definitions: + + o (x div y) where x and y are integers with x >= 0 and y > 0 returns the + integer part of x divided by y (i.e., truncated integer division). + + o (x rem y) where x and y are integers with x >= 0 and y > 0 returns the + remainder when x is divided by y. Note that we always have the following + equivalence (for y > 0): (x div y) * y + (x rem y) = x. + + o bv2nat which takes a bitvector b: [0...m) --> {0,1} + with 0 < m, and returns an integer in the range [0...2^m), + and is defined as follows: + + bv2nat(b) := b(m-1)*2^{m-1} + b(m-2)*2^{m-2} + ... + b(0)*2^0 + + o nat2bv[m], with 0 < m, which takes a non-negative integer + n and returns the (unique) bitvector b: [0,...,m) -> {0,1} + such that + + b(m-1)*2^{m-1} + ... + b(0)*2^0 = n rem 2^m + + Now, we can define the following operations. Suppose s and t are both terms + of sort BitVec[m], m > 0. + + [[(bvneg s)]] := nat2bv[m](2^m - bv2nat([[s]])) + + [[(bvadd s t)]] := nat2bv[m](bv2nat([[s]]) + bv2nat([[t]])) + + [[(bvmul s t)]] := nat2bv[m](bv2nat([[s]]) * bv2nat([[t]])) + + [[(bvudiv s t)]] := if bv2nat([[t]]) != 0 then + nat2bv[m](bv2nat([[s]]) div bv2nat([[t]])) + + [[(bvurem s t)]] := if bv2nat([[t]]) != 0 then + nat2bv[m](bv2nat([[s]]) rem bv2nat([[t]])) + + - Shift operations + + Suppose s and t are both terms of sort BitVec[m], m > 0. We make use of the + definitions given for the arithmetic operations, above. + + [[(bvshl s t)]] := nat2bv[m](bv2nat([[s]]) * 2^(bv2nat([[t]]))) + + [[(bvlshr s t)]] := nat2bv[m](bv2nat([[s]]) div 2^(bv2nat([[t]]))) + + Finally, we can define the binary predicate bvult: + + (bvult s t) is interpreted to be true iff bv2nat([[s]]) < bv2nat([[t]]) + + Note that the semantic interpretation above is underspecified because it + does not specify the meaning of (bvudiv s t) or (bvurem s t) in case + bv2nat([[t]]) is 0. Since the semantics of SMT-LIB's underlying logic + associates *total* functions to function symbols, we then consider as models + of this theory *any* interpretation conforming to the specifications above + (and defining bvudiv and bvurem arbitrarily when the second argument + evaluates to 0). Benchmarks using this theory should only include a + :status sat or :status unsat attribute if the status is independent of + the particular choice of model for the theory. + + " + +) diff --git a/docs/SMT-COMP/QF_AUFBV.smt b/docs/SMT-COMP/QF_AUFBV.smt new file mode 100644 index 00000000..bc055c35 --- /dev/null +++ b/docs/SMT-COMP/QF_AUFBV.smt @@ -0,0 +1,19 @@ +(logic QF_AUFBV + + :written_by {Clark Barrett} + :date {May 7, 2007} + + :theory BV_ArraysEx + + :language + "Closed quantifier-free formulas built over an arbitrary expansion of the + BV_ArraysEx signature with free function and predicate symbols over + the sorts of BV_ArraysEx. Formulas in ite terms must satisfy the same + restriction as well, with the exception that they need not be closed (because + they may be in the scope of a let expression). + " + :extensions + "As in the logic QF_BV." +) + + diff --git a/docs/SMT-COMP/QF_BV.smt b/docs/SMT-COMP/QF_BV.smt new file mode 100644 index 00000000..edf02241 --- /dev/null +++ b/docs/SMT-COMP/QF_BV.smt @@ -0,0 +1,261 @@ +(logic QF_BV + +:written_by {Silvio Ranise, Cesare Tinelli, and Clark Barrett} +:date {May 7, 2007} + +:theory Fixed_Size_BitVectors + +:language + + "Closed quantifier-free formulas built over an arbitrary expansion of the + Fixed_Size_BitVectors signature with free constant symbols over the sorts + BitVec[m] for 0 < m. Formulas in ite terms must satisfy the same restriction + as well, with the exception that they need not be closed (because they may be + in the scope of a let expression). + " + +:notes + "For quick reference, the following is a brief and informal summary of the + legal symbols in this logic and their meaning (formal definitions are found + either in the Fixed_Size_Bitvectors theory, or in the extensions below). + + Defined in theory Fixed_Size_Bitvectors: + + Functions/Constants: + + (bit0 BitVec[1]) + - the constant consisting of a single bit with value 0 + (bit1 BitVec[1]) + - the constant consisting of a single bit with value 1 + (concat BitVec[i] BitVec[j] BitVec[m]) + - concatenation of bitvectors of size i and j to get a new bitvector of + size m, where m = i + j + (extract[i:j] BitVec[m] BitVec[n]) + - extraction of bits i down to j from a bitvector of size m to yield a + new bitvector of size n, where n = i - j + 1 + (bvnot BitVec[m] BitVec[m]) + - bitwise negation + (bvand BitVec[m] BitVec[m] BitVec[m]) + - bitwise and + (bvor BitVec[m] BitVec[m] BitVec[m]) + - bitwise or + (bvneg BitVec[m] BitVec[m]) + - 2's complement unary minus + (bvadd BitVec[m] BitVec[m] BitVec[m]) + - addition modulo 2^m + (bvmul BitVec[m] BitVec[m] BitVec[m]) + - multiplication modulo 2^m + (bvudiv BitVec[m] BitVec[m] BitVec[m]) + - unsigned division, truncating towards 0 (undefined if divisor is 0) + (bvurem BitVec[m] BitVec[m] BitVec[m]) + - unsigned remainder from truncating division (undefined if divisor is 0) + (bvshl BitVec[m] BitVec[m] BitVec[m]) + - shift left (equivalent to multiplication by 2^x where x is the value of + the second argument) + (bvlshr BitVec[m] BitVec[m] BitVec[m]) + - logical shift right (equivalent to unsigned division by 2^x where x is + the value of the second argument) + + Predicates: + + (bvult BitVec[m] BitVec[m]) + - binary predicate for unsigned less than + + Defined below: + + Functions/Constants: + + Bitvector constants: + - bvX[m] where X is a numeral in base 10 defines the bitvector constant + with numeric value X of size m. + - bvbinX where X is a binary numeral of length m defines the + bitvector constant with value X and size m. + - bvhexX where X is a hexadecimal numeral of length m defines the + bitvector constant with value X and size 4*m. + (bvnand BitVec[m] BitVec[m] BitVec[m]) + - bitwise nand (negation of and) + (bvnor BitVec[m] BitVec[m] BitVec[m]) + - bitwise nor (negation of or) + (bvxor BitVec[m] BitVec[m] BitVec[m]) + - bitwise exclusive or + (bvxnor BitVec[m] BitVec[m] BitVec[m]) + - bitwise equivalence (equivalently, negation of bitwise exclusive or) + (bvcomp BitVec[m] BitVec[m] BitVec[1]) + - bit comparator: equals bit1 iff all bits are equal + (bvsub BitVec[m] BitVec[m] BitVec[m]) + - 2's complement subtraction modulo 2^m + (bvsdiv BitVec[m] BitVec[m] BitVec[m]) + - 2's complement signed division + (bvsrem BitVec[m] BitVec[m] BitVec[m]) + - 2's complement signed remainder (sign follows dividend) + (bvsmod BitVec[m] BitVec[m] BitVec[m]) + - 2's complement signed remainder (sign follows divisor) + (bvashr BitVec[m] BitVec[m] BitVec[m]) + - Arithmetic shift right, like logical shift right except that the most + significant bits of the result always copy the most significant + bit of the first argument. + + The following symbols are parameterized by the numeral i, where i >= 0. + + (repeat[i] BitVec[m] BitVec[i*m]) + - (repeat[i] x) means concatenate i copies of x + (zero_extend[i] BitVec[m] BitVec[m+i]) + - (zero_extend[i] x) means extend x with zeroes to the (unsigned) + equivalent bitvector of size m+i + (sign_extend[i] BitVec[m] BitVec[m+i]) + - (sign_extend[i] x) means extend x to the (signed) equivalent bitvector + of size m+i + (rotate_left[i] BitVec[m] BitVec[m]) + - (rotate_left[i] x) means rotate bits of x to the left i times + (rotate_right[i] BitVec[m] BitVec[m]) + - (rotate_right[i] x) means rotate bits of x to the right y times + + Predicates: + + (bvule BitVec[m] BitVec[m]) + - binary predicate for unsigned less than or equal + (bvugt BitVec[m] BitVec[m]) + - binary predicate for unsigned greater than + (bvuge BitVec[m] BitVec[m]) + - binary predicate for unsigned greater than or equal + (bvslt BitVec[m] BitVec[m]) + - binary predicate for signed less than + (bvsle BitVec[m] BitVec[m]) + - binary predicate for signed less than or equal + (bvsgt BitVec[m] BitVec[m]) + - binary predicate for signed greater than + (bvsge BitVec[m] BitVec[m]) + - binary predicate for signed greater than or equal + + " + +:extensions + "Below, let |exp| denote the integer resulting from the evaluation + of the arithmetic expression exp. + + - Bitvector Constants: + The string bv followed by the numeral n and a size [m] (as in bv13[32]) + abbreviates any term t of sort BitVec[m] built only out of the symbols in + {concat, bit0, bit1} such that + + [[t]] = nat2bv[m](n) for n=0, ..., 2^m - 1. + + See the specification of the theory's semantics for a definition + of the functions [[_]] and nat2bv. Note that this convention implicitly + considers the numeral n as a number written in base 10. + + For backward compatibility, if the size [m] is omitted, then the size is + assumed to be 32. + + The string bvbin followed by a sequence of 0's and 1's abbreviates the + concatenation of a similar sequence of bit0 and bit1 terms. Thus, + if n is the numeral represented in base 2 by the sequence of 0's and 1's + and m is the length of the sequence, then the term represents + nat2bv[m](n). For example bvbin0101 is equivalent to bv5[4]. + + The string bvhex followed by a sequence of digits and/or letters from A to + F is interpreted similarly as a concatenation of bit0 and bit1 as follows. + If n is the numeral represented in hexadecimal (base 16) by the sequence of + digits and letters from A to F and m is four times the length of the + sequence, then the term represents nat2bv[m](n). For example, bvbinFF is + equivalent to bv255[8]. Letters in the hexadecimal sequence may be in + either upper or lower case. + + - Bitwise operators + + For all terms s,t of sort BitVec[m], where 0 < m, + + (bvnand s t) abbreviates (bvnot (bvand s t)) + (bvnor s t) abbreviates (bvnot (bvor s t)) + (bvxor s t) abbreviates (bvor (bvand s (bvnot t)) (bvand (bvnot s) t)) + (bvxnor s t) abbreviates (bvor (bvand s t) (bvand (bvnot s) (bvnot t))) + (bvcomp s t) abbreviates (bvxnor s t) if m = 1, and + (bvand (bvxnor (extract[|m-1|:|m-1|] s) (extract[|m-1|:|m-1|] t)) + (bvcomp (extract[|m-2|:0] s) (extract[|m-2|:0] t))) otherwise + + - Arithmetic operators + + For all terms s,t of sort BitVec[m], where 0 < m, + + (bvsub s t) abbreviates (bvadd s (bvneg t)) + (bvsdiv s t) abbreviates + (let (?msb_s (extract[|m-1|:|m-1|] s)) + (let (?msb_t (extract[|m-1|:|m-1|] t)) + (ite (and (= ?msb_s bit0) (= ?msb_t bit0)) + (bvudiv s t) + (ite (and (= ?msb_s bit1) (= ?msb_t bit0)) + (bvneg (bvudiv (bvneg s) t)) + (ite (and (= ?msb_s bit0) (= ?msb_t bit1)) + (bvneg (bvudiv s (bvneg t))) + (bvudiv (bvneg s) (bvneg t))))))) + (bvsrem s t) abbreviates + (let (?msb_s (extract[|m-1|:|m-1|] s)) + (let (?msb_t (extract[|m-1|:|m-1|] t)) + (ite (and (= ?msb_s bit0) (= ?msb_t bit0)) + (bvurem s t) + (ite (and (= ?msb_s bit1) (= ?msb_t bit0)) + (bvneg (bvurem (bvneg s) t)) + (ite (and (= ?msb_s bit0) (= ?msb_t bit1)) + (bvurem s (bvneg t))) + (bvneg (bvurem (bvneg s) (bvneg t))))))) + (bvsmod s t) abbreviates + (let (?msb_s (extract[|m-1|:|m-1|] s)) + (let (?msb_t (extract[|m-1|:|m-1|] t)) + (ite (and (= ?msb_s bit0) (= ?msb_t bit0)) + (bvurem s t) + (ite (and (= ?msb_s bit1) (= ?msb_t bit0)) + (bvadd (bvneg (bvurem (bvneg s) t)) t) + (ite (and (= ?msb_s bit0) (= ?msb_t bit1)) + (bvadd (bvurem s (bvneg t)) t) + (bvneg (bvurem (bvneg s) (bvneg t))))))) + (bvule s t) abbreviates (or (bvult s t) (= s t)) + (bvugt s t) abbreviates (bvult t s) + (bvuge s t) abbreviates (or (bvult t s) (= s t)) + (bvslt s t) abbreviates: + (or (and (= (extract[|m-1|:|m-1|] s) bit1) + (= (extract[|m-1|:|m-1|] t) bit0)) + (and (= (extract[|m-1|:|m-1|] s) (extract[|m-1|:|m-1|] t)) + (bvult s t))) + (bvsle s t) abbreviates: + (or (and (= (extract[|m-1|:|m-1|] s) bit1) + (= (extract[|m-1|:|m-1|] t) bit0)) + (and (= (extract[|m-1|:|m-1|] s) (extract[|m-1|:|m-1|] t)) + (bvule s t))) + (bvsgt s t) abbreviates (bvslt t s) + (bvsge s t) abbreviates (bvsle t s) + + - Other operations + + For all numerals j > 1 and 0 < m, and all terms of s and t of + sort BitVec[m], + + (bvashr s t) abbreviates + (ite (= (extract[|m-1|:|m-1|] s) bit0) + (bvlshr s t) + (bvnot (bvlshr (bvnot s) t))) + + (repeat[1] t) stands for t + (repeat[j] t) abbreviates (concat t (repeat[|j-1|] t)) + + (zero_extend[0] t) stands for t + (zero_extend[j] t) abbreviates (concat (repeat[j] bit0) t) + + (sign_extend[0] t) stands for t + (sign_extend[j] t) abbreviates + (concat (repeat[j] (extract[|m-1|:|m-1|] t)) t) + + (rotate_left[0] t) stands for t + (rotate_left[j] t) abbreviates t if m = 1, and + (rotate_left[|j-1|] + (concat (extract[|m-2|:0] t) (extract[|m-1|:|m-1|] t)) + otherwise + + (rotate_right[0] t) stands for t + (rotate_right[j] t) abbreviates t if m = 1, and + (rotate_right[|j-1|] + (concat (extract[0:0] t) (extract[|m-1|:1] t))) + otherwise + + " +) + diff --git a/docs/doxygen.cfg b/docs/doxygen.cfg new file mode 100644 index 00000000..b13a65ec --- /dev/null +++ b/docs/doxygen.cfg @@ -0,0 +1,1291 @@ +# Doxyfile 1.5.3 + +# This file describes the settings to be used by the documentation system +# doxygen (www.doxygen.org) for a project +# +# All text after a hash (#) is considered a comment and will be ignored +# The format is: +# TAG = value [value, ...] +# For lists items can also be appended using: +# TAG += value [value, ...] +# Values that contain spaces should be placed between quotes (" ") + +#--------------------------------------------------------------------------- +# Project related configuration options +#--------------------------------------------------------------------------- + +# This tag specifies the encoding used for all characters in the config file that +# follow. The default is UTF-8 which is also the encoding used for all text before +# the first occurrence of this tag. Doxygen uses libiconv (or the iconv built into +# libc) for the transcoding. See http://www.gnu.org/software/libiconv for the list of +# possible encodings. + +DOXYFILE_ENCODING = UTF-8 + +# The PROJECT_NAME tag is a single word (or a sequence of words surrounded +# by quotes) that should identify the project. + +PROJECT_NAME = klee + +# The PROJECT_NUMBER tag can be used to enter a project or revision number. +# This could be handy for archiving the generated documentation or +# if some version control system is used. + +PROJECT_NUMBER = + +# The OUTPUT_DIRECTORY tag is used to specify the (relative or absolute) +# base path where the generated documentation will be put. +# If a relative path is entered, it will be relative to the location +# where doxygen was started. If left blank the current directory will be used. + +OUTPUT_DIRECTORY = docs/doxygen + +# If the CREATE_SUBDIRS tag is set to YES, then doxygen will create +# 4096 sub-directories (in 2 levels) under the output directory of each output +# format and will distribute the generated files over these directories. +# Enabling this option can be useful when feeding doxygen a huge amount of +# source files, where putting all generated files in the same directory would +# otherwise cause performance problems for the file system. + +CREATE_SUBDIRS = NO + +# The OUTPUT_LANGUAGE tag is used to specify the language in which all +# documentation generated by doxygen is written. Doxygen will use this +# information to generate all constant output in the proper language. +# The default language is English, other supported languages are: +# Afrikaans, Arabic, Brazilian, Catalan, Chinese, Chinese-Traditional, +# Croatian, Czech, Danish, Dutch, Finnish, French, German, Greek, Hungarian, +# Italian, Japanese, Japanese-en (Japanese with English messages), Korean, +# Korean-en, Lithuanian, Norwegian, Polish, Portuguese, Romanian, Russian, +# Serbian, Slovak, Slovene, Spanish, Swedish, and Ukrainian. + +OUTPUT_LANGUAGE = English + +# If the BRIEF_MEMBER_DESC tag is set to YES (the default) Doxygen will +# include brief member descriptions after the members that are listed in +# the file and class documentation (similar to JavaDoc). +# Set to NO to disable this. + +BRIEF_MEMBER_DESC = YES + +# If the REPEAT_BRIEF tag is set to YES (the default) Doxygen will prepend +# the brief description of a member or function before the detailed description. +# Note: if both HIDE_UNDOC_MEMBERS and BRIEF_MEMBER_DESC are set to NO, the +# brief descriptions will be completely suppressed. + +REPEAT_BRIEF = YES + +# This tag implements a quasi-intelligent brief description abbreviator +# that is used to form the text in various listings. Each string +# in this list, if found as the leading text of the brief description, will be +# stripped from the text and the result after processing the whole list, is +# used as the annotated text. Otherwise, the brief description is used as-is. +# If left blank, the following values are used ("$name" is automatically +# replaced with the name of the entity): "The $name class" "The $name widget" +# "The $name file" "is" "provides" "specifies" "contains" +# "represents" "a" "an" "the" + +ABBREVIATE_BRIEF = + +# If the ALWAYS_DETAILED_SEC and REPEAT_BRIEF tags are both set to YES then +# Doxygen will generate a detailed section even if there is only a brief +# description. + +ALWAYS_DETAILED_SEC = NO + +# If the INLINE_INHERITED_MEMB tag is set to YES, doxygen will show all +# inherited members of a class in the documentation of that class as if those +# members were ordinary class members. Constructors, destructors and assignment +# operators of the base classes will not be shown. + +INLINE_INHERITED_MEMB = NO + +# If the FULL_PATH_NAMES tag is set to YES then Doxygen will prepend the full +# path before files name in the file list and in the header files. If set +# to NO the shortest path that makes the file name unique will be used. + +FULL_PATH_NAMES = YES + +# If the FULL_PATH_NAMES tag is set to YES then the STRIP_FROM_PATH tag +# can be used to strip a user-defined part of the path. Stripping is +# only done if one of the specified strings matches the left-hand part of +# the path. The tag can be used to show relative paths in the file list. +# If left blank the directory from which doxygen is run is used as the +# path to strip. + +STRIP_FROM_PATH = + +# The STRIP_FROM_INC_PATH tag can be used to strip a user-defined part of +# the path mentioned in the documentation of a class, which tells +# the reader which header file to include in order to use a class. +# If left blank only the name of the header file containing the class +# definition is used. Otherwise one should specify the include paths that +# are normally passed to the compiler using the -I flag. + +STRIP_FROM_INC_PATH = + +# If the SHORT_NAMES tag is set to YES, doxygen will generate much shorter +# (but less readable) file names. This can be useful is your file systems +# doesn't support long names like on DOS, Mac, or CD-ROM. + +SHORT_NAMES = NO + +# If the JAVADOC_AUTOBRIEF tag is set to YES then Doxygen +# will interpret the first line (until the first dot) of a JavaDoc-style +# comment as the brief description. If set to NO, the JavaDoc +# comments will behave just like regular Qt-style comments +# (thus requiring an explicit @brief command for a brief description.) + +JAVADOC_AUTOBRIEF = NO + +# If the QT_AUTOBRIEF tag is set to YES then Doxygen will +# interpret the first line (until the first dot) of a Qt-style +# comment as the brief description. If set to NO, the comments +# will behave just like regular Qt-style comments (thus requiring +# an explicit \brief command for a brief description.) + +QT_AUTOBRIEF = NO + +# The MULTILINE_CPP_IS_BRIEF tag can be set to YES to make Doxygen +# treat a multi-line C++ special comment block (i.e. a block of //! or /// +# comments) as a brief description. This used to be the default behaviour. +# The new default is to treat a multi-line C++ comment block as a detailed +# description. Set this tag to YES if you prefer the old behaviour instead. + +MULTILINE_CPP_IS_BRIEF = NO + +# If the INHERIT_DOCS tag is set to YES (the default) then an undocumented +# member inherits the documentation from any documented member that it +# re-implements. + +INHERIT_DOCS = YES + +# If the SEPARATE_MEMBER_PAGES tag is set to YES, then doxygen will produce +# a new page for each member. If set to NO, the documentation of a member will +# be part of the file/class/namespace that contains it. + +SEPARATE_MEMBER_PAGES = NO + +# The TAB_SIZE tag can be used to set the number of spaces in a tab. +# Doxygen uses this value to replace tabs by spaces in code fragments. + +TAB_SIZE = 8 + +# This tag can be used to specify a number of aliases that acts +# as commands in the documentation. An alias has the form "name=value". +# For example adding "sideeffect=\par Side Effects:\n" will allow you to +# put the command \sideeffect (or @sideeffect) in the documentation, which +# will result in a user-defined paragraph with heading "Side Effects:". +# You can put \n's in the value part of an alias to insert newlines. + +ALIASES = + +# Set the OPTIMIZE_OUTPUT_FOR_C tag to YES if your project consists of C +# sources only. Doxygen will then generate output that is more tailored for C. +# For instance, some of the names that are used will be different. The list +# of all members will be omitted, etc. + +OPTIMIZE_OUTPUT_FOR_C = NO + +# Set the OPTIMIZE_OUTPUT_JAVA tag to YES if your project consists of Java +# sources only. Doxygen will then generate output that is more tailored for Java. +# For instance, namespaces will be presented as packages, qualified scopes +# will look different, etc. + +OPTIMIZE_OUTPUT_JAVA = NO + +# If you use STL classes (i.e. std::string, std::vector, etc.) but do not want to +# include (a tag file for) the STL sources as input, then you should +# set this tag to YES in order to let doxygen match functions declarations and +# definitions whose arguments contain STL classes (e.g. func(std::string); v.s. +# func(std::string) {}). This also make the inheritance and collaboration +# diagrams that involve STL classes more complete and accurate. + +BUILTIN_STL_SUPPORT = NO + +# If you use Microsoft's C++/CLI language, you should set this option to YES to +# enable parsing support. + +CPP_CLI_SUPPORT = NO + +# If member grouping is used in the documentation and the DISTRIBUTE_GROUP_DOC +# tag is set to YES, then doxygen will reuse the documentation of the first +# member in the group (if any) for the other members of the group. By default +# all members of a group must be documented explicitly. + +DISTRIBUTE_GROUP_DOC = NO + +# Set the SUBGROUPING tag to YES (the default) to allow class member groups of +# the same type (for instance a group of public functions) to be put as a +# subgroup of that type (e.g. under the Public Functions section). Set it to +# NO to prevent subgrouping. Alternatively, this can be done per class using +# the \nosubgrouping command. + +SUBGROUPING = YES + +#--------------------------------------------------------------------------- +# Build related configuration options +#--------------------------------------------------------------------------- + +# If the EXTRACT_ALL tag is set to YES doxygen will assume all entities in +# documentation are documented, even if no documentation was available. +# Private class members and static file members will be hidden unless +# the EXTRACT_PRIVATE and EXTRACT_STATIC tags are set to YES + +EXTRACT_ALL = YES + +# If the EXTRACT_PRIVATE tag is set to YES all private members of a class +# will be included in the documentation. + +EXTRACT_PRIVATE = YES + +# If the EXTRACT_STATIC tag is set to YES all static members of a file +# will be included in the documentation. + +EXTRACT_STATIC = YES + +# If the EXTRACT_LOCAL_CLASSES tag is set to YES classes (and structs) +# defined locally in source files will be included in the documentation. +# If set to NO only classes defined in header files are included. + +EXTRACT_LOCAL_CLASSES = YES + +# This flag is only useful for Objective-C code. When set to YES local +# methods, which are defined in the implementation section but not in +# the interface are included in the documentation. +# If set to NO (the default) only methods in the interface are included. + +EXTRACT_LOCAL_METHODS = NO + +# If this flag is set to YES, the members of anonymous namespaces will be extracted +# and appear in the documentation as a namespace called 'anonymous_namespace{file}', +# where file will be replaced with the base name of the file that contains the anonymous +# namespace. By default anonymous namespace are hidden. + +EXTRACT_ANON_NSPACES = NO + +# If the HIDE_UNDOC_MEMBERS tag is set to YES, Doxygen will hide all +# undocumented members of documented classes, files or namespaces. +# If set to NO (the default) these members will be included in the +# various overviews, but no documentation section is generated. +# This option has no effect if EXTRACT_ALL is enabled. + +HIDE_UNDOC_MEMBERS = YES + +# If the HIDE_UNDOC_CLASSES tag is set to YES, Doxygen will hide all +# undocumented classes that are normally visible in the class hierarchy. +# If set to NO (the default) these classes will be included in the various +# overviews. This option has no effect if EXTRACT_ALL is enabled. + +HIDE_UNDOC_CLASSES = YES + +# If the HIDE_FRIEND_COMPOUNDS tag is set to YES, Doxygen will hide all +# friend (class|struct|union) declarations. +# If set to NO (the default) these declarations will be included in the +# documentation. + +HIDE_FRIEND_COMPOUNDS = NO + +# If the HIDE_IN_BODY_DOCS tag is set to YES, Doxygen will hide any +# documentation blocks found inside the body of a function. +# If set to NO (the default) these blocks will be appended to the +# function's detailed documentation block. + +HIDE_IN_BODY_DOCS = NO + +# The INTERNAL_DOCS tag determines if documentation +# that is typed after a \internal command is included. If the tag is set +# to NO (the default) then the documentation will be excluded. +# Set it to YES to include the internal documentation. + +INTERNAL_DOCS = NO + +# If the CASE_SENSE_NAMES tag is set to NO then Doxygen will only generate +# file names in lower-case letters. If set to YES upper-case letters are also +# allowed. This is useful if you have classes or files whose names only differ +# in case and if your file system supports case sensitive file names. Windows +# and Mac users are advised to set this option to NO. + +CASE_SENSE_NAMES = YES + +# If the HIDE_SCOPE_NAMES tag is set to NO (the default) then Doxygen +# will show members with their full class and namespace scopes in the +# documentation. If set to YES the scope will be hidden. + +HIDE_SCOPE_NAMES = NO + +# If the SHOW_INCLUDE_FILES tag is set to YES (the default) then Doxygen +# will put a list of the files that are included by a file in the documentation +# of that file. + +SHOW_INCLUDE_FILES = YES + +# If the INLINE_INFO tag is set to YES (the default) then a tag [inline] +# is inserted in the documentation for inline members. + +INLINE_INFO = YES + +# If the SORT_MEMBER_DOCS tag is set to YES (the default) then doxygen +# will sort the (detailed) documentation of file and class members +# alphabetically by member name. If set to NO the members will appear in +# declaration order. + +SORT_MEMBER_DOCS = YES + +# If the SORT_BRIEF_DOCS tag is set to YES then doxygen will sort the +# brief documentation of file, namespace and class members alphabetically +# by member name. If set to NO (the default) the members will appear in +# declaration order. + +SORT_BRIEF_DOCS = NO + +# If the SORT_BY_SCOPE_NAME tag is set to YES, the class list will be +# sorted by fully-qualified names, including namespaces. If set to +# NO (the default), the class list will be sorted only by class name, +# not including the namespace part. +# Note: This option is not very useful if HIDE_SCOPE_NAMES is set to YES. +# Note: This option applies only to the class list, not to the +# alphabetical list. + +SORT_BY_SCOPE_NAME = NO + +# The GENERATE_TODOLIST tag can be used to enable (YES) or +# disable (NO) the todo list. This list is created by putting \todo +# commands in the documentation. + +GENERATE_TODOLIST = YES + +# The GENERATE_TESTLIST tag can be used to enable (YES) or +# disable (NO) the test list. This list is created by putting \test +# commands in the documentation. + +GENERATE_TESTLIST = YES + +# The GENERATE_BUGLIST tag can be used to enable (YES) or +# disable (NO) the bug list. This list is created by putting \bug +# commands in the documentation. + +GENERATE_BUGLIST = YES + +# The GENERATE_DEPRECATEDLIST tag can be used to enable (YES) or +# disable (NO) the deprecated list. This list is created by putting +# \deprecated commands in the documentation. + +GENERATE_DEPRECATEDLIST= YES + +# The ENABLED_SECTIONS tag can be used to enable conditional +# documentation sections, marked by \if sectionname ... \endif. + +ENABLED_SECTIONS = + +# The MAX_INITIALIZER_LINES tag determines the maximum number of lines +# the initial value of a variable or define consists of for it to appear in +# the documentation. If the initializer consists of more lines than specified +# here it will be hidden. Use a value of 0 to hide initializers completely. +# The appearance of the initializer of individual variables and defines in the +# documentation can be controlled using \showinitializer or \hideinitializer +# command in the documentation regardless of this setting. + +MAX_INITIALIZER_LINES = 30 + +# Set the SHOW_USED_FILES tag to NO to disable the list of files generated +# at the bottom of the documentation of classes and structs. If set to YES the +# list will mention the files that were used to generate the documentation. + +SHOW_USED_FILES = YES + +# If the sources in your project are distributed over multiple directories +# then setting the SHOW_DIRECTORIES tag to YES will show the directory hierarchy +# in the documentation. The default is NO. + +SHOW_DIRECTORIES = YES + +# The FILE_VERSION_FILTER tag can be used to specify a program or script that +# doxygen should invoke to get the current version for each file (typically from the +# version control system). Doxygen will invoke the program by executing (via +# popen()) the command <command> <input-file>, where <command> is the value of +# the FILE_VERSION_FILTER tag, and <input-file> is the name of an input file +# provided by doxygen. Whatever the program writes to standard output +# is used as the file version. See the manual for examples. + +FILE_VERSION_FILTER = + +#--------------------------------------------------------------------------- +# configuration options related to warning and progress messages +#--------------------------------------------------------------------------- + +# The QUIET tag can be used to turn on/off the messages that are generated +# by doxygen. Possible values are YES and NO. If left blank NO is used. + +QUIET = NO + +# The WARNINGS tag can be used to turn on/off the warning messages that are +# generated by doxygen. Possible values are YES and NO. If left blank +# NO is used. + +WARNINGS = YES + +# If WARN_IF_UNDOCUMENTED is set to YES, then doxygen will generate warnings +# for undocumented members. If EXTRACT_ALL is set to YES then this flag will +# automatically be disabled. + +WARN_IF_UNDOCUMENTED = YES + +# If WARN_IF_DOC_ERROR is set to YES, doxygen will generate warnings for +# potential errors in the documentation, such as not documenting some +# parameters in a documented function, or documenting parameters that +# don't exist or using markup commands wrongly. + +WARN_IF_DOC_ERROR = YES + +# This WARN_NO_PARAMDOC option can be abled to get warnings for +# functions that are documented, but have no documentation for their parameters +# or return value. If set to NO (the default) doxygen will only warn about +# wrong or incomplete parameter documentation, but not about the absence of +# documentation. + +WARN_NO_PARAMDOC = NO + +# The WARN_FORMAT tag determines the format of the warning messages that +# doxygen can produce. The string should contain the $file, $line, and $text +# tags, which will be replaced by the file and line number from which the +# warning originated and the warning text. Optionally the format may contain +# $version, which will be replaced by the version of the file (if it could +# be obtained via FILE_VERSION_FILTER) + +WARN_FORMAT = "$file:$line: $text" + +# The WARN_LOGFILE tag can be used to specify a file to which warning +# and error messages should be written. If left blank the output is written +# to stderr. + +WARN_LOGFILE = + +#--------------------------------------------------------------------------- +# configuration options related to the input files +#--------------------------------------------------------------------------- + +# The INPUT tag can be used to specify the files and/or directories that contain +# documented source files. You may enter file names like "myfile.cpp" or +# directories like "/usr/src/myproject". Separate the files or directories +# with spaces. + +INPUT = tools/ \ + lib/ \ + include/klee \ + docs/intro \ + docs/overview + +# This tag can be used to specify the character encoding of the source files that +# doxygen parses. Internally doxygen uses the UTF-8 encoding, which is also the default +# input encoding. Doxygen uses libiconv (or the iconv built into libc) for the transcoding. +# See http://www.gnu.org/software/libiconv for the list of possible encodings. + +INPUT_ENCODING = UTF-8 + +# If the value of the INPUT tag contains directories, you can use the +# FILE_PATTERNS tag to specify one or more wildcard pattern (like *.cpp +# and *.h) to filter out the source-files in the directories. If left +# blank the following patterns are tested: +# *.c *.cc *.cxx *.cpp *.c++ *.java *.ii *.ixx *.ipp *.i++ *.inl *.h *.hh *.hxx +# *.hpp *.h++ *.idl *.odl *.cs *.php *.php3 *.inc *.m *.mm *.py + +FILE_PATTERNS = + +# The RECURSIVE tag can be used to turn specify whether or not subdirectories +# should be searched for input files as well. Possible values are YES and NO. +# If left blank NO is used. + +RECURSIVE = YES + +# The EXCLUDE tag can be used to specify files and/or directories that should +# excluded from the INPUT source files. This way you can easily exclude a +# subdirectory from a directory tree whose root is specified with the INPUT tag. + +EXCLUDE = + +# The EXCLUDE_SYMLINKS tag can be used select whether or not files or +# directories that are symbolic links (a Unix filesystem feature) are excluded +# from the input. + +EXCLUDE_SYMLINKS = NO + +# If the value of the INPUT tag contains directories, you can use the +# EXCLUDE_PATTERNS tag to specify one or more wildcard patterns to exclude +# certain files from those directories. Note that the wildcards are matched +# against the file with absolute path, so to exclude all test directories +# for example use the pattern */test/* + +EXCLUDE_PATTERNS = */.svn* */Debug* + +# The EXCLUDE_SYMBOLS tag can be used to specify one or more symbol names +# (namespaces, classes, functions, etc.) that should be excluded from the output. +# The symbol name can be a fully qualified name, a word, or if the wildcard * is used, +# a substring. Examples: ANamespace, AClass, AClass::ANamespace, ANamespace::*Test + +EXCLUDE_SYMBOLS = + +# The EXAMPLE_PATH tag can be used to specify one or more files or +# directories that contain example code fragments that are included (see +# the \include command). + +EXAMPLE_PATH = + +# If the value of the EXAMPLE_PATH tag contains directories, you can use the +# EXAMPLE_PATTERNS tag to specify one or more wildcard pattern (like *.cpp +# and *.h) to filter out the source-files in the directories. If left +# blank all files are included. + +EXAMPLE_PATTERNS = + +# If the EXAMPLE_RECURSIVE tag is set to YES then subdirectories will be +# searched for input files to be used with the \include or \dontinclude +# commands irrespective of the value of the RECURSIVE tag. +# Possible values are YES and NO. If left blank NO is used. + +EXAMPLE_RECURSIVE = NO + +# The IMAGE_PATH tag can be used to specify one or more files or +# directories that contain image that are included in the documentation (see +# the \image command). + +IMAGE_PATH = + +# The INPUT_FILTER tag can be used to specify a program that doxygen should +# invoke to filter for each input file. Doxygen will invoke the filter program +# by executing (via popen()) the command <filter> <input-file>, where <filter> +# is the value of the INPUT_FILTER tag, and <input-file> is the name of an +# input file. Doxygen will then use the output that the filter program writes +# to standard output. If FILTER_PATTERNS is specified, this tag will be +# ignored. + +INPUT_FILTER = + +# The FILTER_PATTERNS tag can be used to specify filters on a per file pattern +# basis. Doxygen will compare the file name with each pattern and apply the +# filter if there is a match. The filters are a list of the form: +# pattern=filter (like *.cpp=my_cpp_filter). See INPUT_FILTER for further +# info on how filters are used. If FILTER_PATTERNS is empty, INPUT_FILTER +# is applied to all files. + +FILTER_PATTERNS = + +# If the FILTER_SOURCE_FILES tag is set to YES, the input filter (if set using +# INPUT_FILTER) will be used to filter the input files when producing source +# files to browse (i.e. when SOURCE_BROWSER is set to YES). + +FILTER_SOURCE_FILES = NO + +#--------------------------------------------------------------------------- +# configuration options related to source browsing +#--------------------------------------------------------------------------- + +# If the SOURCE_BROWSER tag is set to YES then a list of source files will +# be generated. Documented entities will be cross-referenced with these sources. +# Note: To get rid of all source code in the generated output, make sure also +# VERBATIM_HEADERS is set to NO. If you have enabled CALL_GRAPH or CALLER_GRAPH +# then you must also enable this option. If you don't then doxygen will produce +# a warning and turn it on anyway + +SOURCE_BROWSER = YES + +# Setting the INLINE_SOURCES tag to YES will include the body +# of functions and classes directly in the documentation. + +INLINE_SOURCES = NO + +# Setting the STRIP_CODE_COMMENTS tag to YES (the default) will instruct +# doxygen to hide any special comment blocks from generated source code +# fragments. Normal C and C++ comments will always remain visible. + +STRIP_CODE_COMMENTS = YES + +# If the REFERENCED_BY_RELATION tag is set to YES (the default) +# then for each documented function all documented +# functions referencing it will be listed. + +REFERENCED_BY_RELATION = YES + +# If the REFERENCES_RELATION tag is set to YES (the default) +# then for each documented function all documented entities +# called/used by that function will be listed. + +REFERENCES_RELATION = YES + +# If the REFERENCES_LINK_SOURCE tag is set to YES (the default) +# and SOURCE_BROWSER tag is set to YES, then the hyperlinks from +# functions in REFERENCES_RELATION and REFERENCED_BY_RELATION lists will +# link to the source code. Otherwise they will link to the documentstion. + +REFERENCES_LINK_SOURCE = YES + +# If the USE_HTAGS tag is set to YES then the references to source code +# will point to the HTML generated by the htags(1) tool instead of doxygen +# built-in source browser. The htags tool is part of GNU's global source +# tagging system (see http://www.gnu.org/software/global/global.html). You +# will need version 4.8.6 or higher. + +USE_HTAGS = NO + +# If the VERBATIM_HEADERS tag is set to YES (the default) then Doxygen +# will generate a verbatim copy of the header file for each class for +# which an include is specified. Set to NO to disable this. + +VERBATIM_HEADERS = YES + +#--------------------------------------------------------------------------- +# configuration options related to the alphabetical class index +#--------------------------------------------------------------------------- + +# If the ALPHABETICAL_INDEX tag is set to YES, an alphabetical index +# of all compounds will be generated. Enable this if the project +# contains a lot of classes, structs, unions or interfaces. + +ALPHABETICAL_INDEX = YES + +# If the alphabetical index is enabled (see ALPHABETICAL_INDEX) then +# the COLS_IN_ALPHA_INDEX tag can be used to specify the number of columns +# in which this list will be split (can be a number in the range [1..20]) + +COLS_IN_ALPHA_INDEX = 5 + +# In case all classes in a project start with a common prefix, all +# classes will be put under the same header in the alphabetical index. +# The IGNORE_PREFIX tag can be used to specify one or more prefixes that +# should be ignored while generating the index headers. + +IGNORE_PREFIX = + +#--------------------------------------------------------------------------- +# configuration options related to the HTML output +#--------------------------------------------------------------------------- + +# If the GENERATE_HTML tag is set to YES (the default) Doxygen will +# generate HTML output. + +GENERATE_HTML = YES + +# The HTML_OUTPUT tag is used to specify where the HTML docs will be put. +# If a relative path is entered the value of OUTPUT_DIRECTORY will be +# put in front of it. If left blank `html' will be used as the default path. + +HTML_OUTPUT = html + +# The HTML_FILE_EXTENSION tag can be used to specify the file extension for +# each generated HTML page (for example: .htm,.php,.asp). If it is left blank +# doxygen will generate files with .html extension. + +HTML_FILE_EXTENSION = .html + +# The HTML_HEADER tag can be used to specify a personal HTML header for +# each generated HTML page. If it is left blank doxygen will generate a +# standard header. + +HTML_HEADER = + +# The HTML_FOOTER tag can be used to specify a personal HTML footer for +# each generated HTML page. If it is left blank doxygen will generate a +# standard footer. + +HTML_FOOTER = + +# The HTML_STYLESHEET tag can be used to specify a user-defined cascading +# style sheet that is used by each HTML page. It can be used to +# fine-tune the look of the HTML output. If the tag is left blank doxygen +# will generate a default style sheet. Note that doxygen will try to copy +# the style sheet file to the HTML output directory, so don't put your own +# stylesheet in the HTML output directory as well, or it will be erased! + +HTML_STYLESHEET = + +# If the HTML_ALIGN_MEMBERS tag is set to YES, the members of classes, +# files or namespaces will be aligned in HTML using tables. If set to +# NO a bullet list will be used. + +HTML_ALIGN_MEMBERS = YES + +# If the GENERATE_HTMLHELP tag is set to YES, additional index files +# will be generated that can be used as input for tools like the +# Microsoft HTML help workshop to generate a compressed HTML help file (.chm) +# of the generated HTML documentation. + +GENERATE_HTMLHELP = NO + +# If the HTML_DYNAMIC_SECTIONS tag is set to YES then the generated HTML +# documentation will contain sections that can be hidden and shown after the +# page has loaded. For this to work a browser that supports +# JavaScript and DHTML is required (for instance Mozilla 1.0+, Firefox +# Netscape 6.0+, Internet explorer 5.0+, Konqueror, or Safari). + +HTML_DYNAMIC_SECTIONS = NO + +# If the GENERATE_HTMLHELP tag is set to YES, the CHM_FILE tag can +# be used to specify the file name of the resulting .chm file. You +# can add a path in front of the file if the result should not be +# written to the html output directory. + +CHM_FILE = + +# If the GENERATE_HTMLHELP tag is set to YES, the HHC_LOCATION tag can +# be used to specify the location (absolute path including file name) of +# the HTML help compiler (hhc.exe). If non-empty doxygen will try to run +# the HTML help compiler on the generated index.hhp. + +HHC_LOCATION = + +# If the GENERATE_HTMLHELP tag is set to YES, the GENERATE_CHI flag +# controls if a separate .chi index file is generated (YES) or that +# it should be included in the master .chm file (NO). + +GENERATE_CHI = NO + +# If the GENERATE_HTMLHELP tag is set to YES, the BINARY_TOC flag +# controls whether a binary table of contents is generated (YES) or a +# normal table of contents (NO) in the .chm file. + +BINARY_TOC = NO + +# The TOC_EXPAND flag can be set to YES to add extra items for group members +# to the contents of the HTML help documentation and to the tree view. + +TOC_EXPAND = NO + +# The DISABLE_INDEX tag can be used to turn on/off the condensed index at +# top of each HTML page. The value NO (the default) enables the index and +# the value YES disables it. + +DISABLE_INDEX = NO + +# This tag can be used to set the number of enum values (range [1..20]) +# that doxygen will group on one line in the generated HTML documentation. + +ENUM_VALUES_PER_LINE = 4 + +# If the GENERATE_TREEVIEW tag is set to YES, a side panel will be +# generated containing a tree-like index structure (just like the one that +# is generated for HTML Help). For this to work a browser that supports +# JavaScript, DHTML, CSS and frames is required (for instance Mozilla 1.0+, +# Netscape 6.0+, Internet explorer 5.0+, or Konqueror). Windows users are +# probably better off using the HTML help feature. + +GENERATE_TREEVIEW = YES + +# If the treeview is enabled (see GENERATE_TREEVIEW) then this tag can be +# used to set the initial width (in pixels) of the frame in which the tree +# is shown. + +TREEVIEW_WIDTH = 250 + +#--------------------------------------------------------------------------- +# configuration options related to the LaTeX output +#--------------------------------------------------------------------------- + +# If the GENERATE_LATEX tag is set to YES (the default) Doxygen will +# generate Latex output. + +GENERATE_LATEX = NO + +# The LATEX_OUTPUT tag is used to specify where the LaTeX docs will be put. +# If a relative path is entered the value of OUTPUT_DIRECTORY will be +# put in front of it. If left blank `latex' will be used as the default path. + +LATEX_OUTPUT = latex + +# The LATEX_CMD_NAME tag can be used to specify the LaTeX command name to be +# invoked. If left blank `latex' will be used as the default command name. + +LATEX_CMD_NAME = latex + +# The MAKEINDEX_CMD_NAME tag can be used to specify the command name to +# generate index for LaTeX. If left blank `makeindex' will be used as the +# default command name. + +MAKEINDEX_CMD_NAME = makeindex + +# If the COMPACT_LATEX tag is set to YES Doxygen generates more compact +# LaTeX documents. This may be useful for small projects and may help to +# save some trees in general. + +COMPACT_LATEX = NO + +# The PAPER_TYPE tag can be used to set the paper type that is used +# by the printer. Possible values are: a4, a4wide, letter, legal and +# executive. If left blank a4wide will be used. + +PAPER_TYPE = a4wide + +# The EXTRA_PACKAGES tag can be to specify one or more names of LaTeX +# packages that should be included in the LaTeX output. + +EXTRA_PACKAGES = + +# The LATEX_HEADER tag can be used to specify a personal LaTeX header for +# the generated latex document. The header should contain everything until +# the first chapter. If it is left blank doxygen will generate a +# standard header. Notice: only use this tag if you know what you are doing! + +LATEX_HEADER = + +# If the PDF_HYPERLINKS tag is set to YES, the LaTeX that is generated +# is prepared for conversion to pdf (using ps2pdf). The pdf file will +# contain links (just like the HTML output) instead of page references +# This makes the output suitable for online browsing using a pdf viewer. + +PDF_HYPERLINKS = NO + +# If the USE_PDFLATEX tag is set to YES, pdflatex will be used instead of +# plain latex in the generated Makefile. Set this option to YES to get a +# higher quality PDF documentation. + +USE_PDFLATEX = NO + +# If the LATEX_BATCHMODE tag is set to YES, doxygen will add the \\batchmode. +# command to the generated LaTeX files. This will instruct LaTeX to keep +# running if errors occur, instead of asking the user for help. +# This option is also used when generating formulas in HTML. + +LATEX_BATCHMODE = NO + +# If LATEX_HIDE_INDICES is set to YES then doxygen will not +# include the index chapters (such as File Index, Compound Index, etc.) +# in the output. + +LATEX_HIDE_INDICES = NO + +#--------------------------------------------------------------------------- +# configuration options related to the RTF output +#--------------------------------------------------------------------------- + +# If the GENERATE_RTF tag is set to YES Doxygen will generate RTF output +# The RTF output is optimized for Word 97 and may not look very pretty with +# other RTF readers or editors. + +GENERATE_RTF = NO + +# The RTF_OUTPUT tag is used to specify where the RTF docs will be put. +# If a relative path is entered the value of OUTPUT_DIRECTORY will be +# put in front of it. If left blank `rtf' will be used as the default path. + +RTF_OUTPUT = rtf + +# If the COMPACT_RTF tag is set to YES Doxygen generates more compact +# RTF documents. This may be useful for small projects and may help to +# save some trees in general. + +COMPACT_RTF = NO + +# If the RTF_HYPERLINKS tag is set to YES, the RTF that is generated +# will contain hyperlink fields. The RTF file will +# contain links (just like the HTML output) instead of page references. +# This makes the output suitable for online browsing using WORD or other +# programs which support those fields. +# Note: wordpad (write) and others do not support links. + +RTF_HYPERLINKS = NO + +# Load stylesheet definitions from file. Syntax is similar to doxygen's +# config file, i.e. a series of assignments. You only have to provide +# replacements, missing definitions are set to their default value. + +RTF_STYLESHEET_FILE = + +# Set optional variables used in the generation of an rtf document. +# Syntax is similar to doxygen's config file. + +RTF_EXTENSIONS_FILE = + +#--------------------------------------------------------------------------- +# configuration options related to the man page output +#--------------------------------------------------------------------------- + +# If the GENERATE_MAN tag is set to YES (the default) Doxygen will +# generate man pages + +GENERATE_MAN = NO + +# The MAN_OUTPUT tag is used to specify where the man pages will be put. +# If a relative path is entered the value of OUTPUT_DIRECTORY will be +# put in front of it. If left blank `man' will be used as the default path. + +MAN_OUTPUT = man + +# The MAN_EXTENSION tag determines the extension that is added to +# the generated man pages (default is the subroutine's section .3) + +MAN_EXTENSION = .3 + +# If the MAN_LINKS tag is set to YES and Doxygen generates man output, +# then it will generate one additional man file for each entity +# documented in the real man page(s). These additional files +# only source the real man page, but without them the man command +# would be unable to find the correct page. The default is NO. + +MAN_LINKS = NO + +#--------------------------------------------------------------------------- +# configuration options related to the XML output +#--------------------------------------------------------------------------- + +# If the GENERATE_XML tag is set to YES Doxygen will +# generate an XML file that captures the structure of +# the code including all documentation. + +GENERATE_XML = NO + +# The XML_OUTPUT tag is used to specify where the XML pages will be put. +# If a relative path is entered the value of OUTPUT_DIRECTORY will be +# put in front of it. If left blank `xml' will be used as the default path. + +XML_OUTPUT = xml + +# The XML_SCHEMA tag can be used to specify an XML schema, +# which can be used by a validating XML parser to check the +# syntax of the XML files. + +XML_SCHEMA = + +# The XML_DTD tag can be used to specify an XML DTD, +# which can be used by a validating XML parser to check the +# syntax of the XML files. + +XML_DTD = + +# If the XML_PROGRAMLISTING tag is set to YES Doxygen will +# dump the program listings (including syntax highlighting +# and cross-referencing information) to the XML output. Note that +# enabling this will significantly increase the size of the XML output. + +XML_PROGRAMLISTING = YES + +#--------------------------------------------------------------------------- +# configuration options for the AutoGen Definitions output +#--------------------------------------------------------------------------- + +# If the GENERATE_AUTOGEN_DEF tag is set to YES Doxygen will +# generate an AutoGen Definitions (see autogen.sf.net) file +# that captures the structure of the code including all +# documentation. Note that this feature is still experimental +# and incomplete at the moment. + +GENERATE_AUTOGEN_DEF = NO + +#--------------------------------------------------------------------------- +# configuration options related to the Perl module output +#--------------------------------------------------------------------------- + +# If the GENERATE_PERLMOD tag is set to YES Doxygen will +# generate a Perl module file that captures the structure of +# the code including all documentation. Note that this +# feature is still experimental and incomplete at the +# moment. + +GENERATE_PERLMOD = NO + +# If the PERLMOD_LATEX tag is set to YES Doxygen will generate +# the necessary Makefile rules, Perl scripts and LaTeX code to be able +# to generate PDF and DVI output from the Perl module output. + +PERLMOD_LATEX = NO + +# If the PERLMOD_PRETTY tag is set to YES the Perl module output will be +# nicely formatted so it can be parsed by a human reader. This is useful +# if you want to understand what is going on. On the other hand, if this +# tag is set to NO the size of the Perl module output will be much smaller +# and Perl will parse it just the same. + +PERLMOD_PRETTY = YES + +# The names of the make variables in the generated doxyrules.make file +# are prefixed with the string contained in PERLMOD_MAKEVAR_PREFIX. +# This is useful so different doxyrules.make files included by the same +# Makefile don't overwrite each other's variables. + +PERLMOD_MAKEVAR_PREFIX = + +#--------------------------------------------------------------------------- +# Configuration options related to the preprocessor +#--------------------------------------------------------------------------- + +# If the ENABLE_PREPROCESSING tag is set to YES (the default) Doxygen will +# evaluate all C-preprocessor directives found in the sources and include +# files. + +ENABLE_PREPROCESSING = YES + +# If the MACRO_EXPANSION tag is set to YES Doxygen will expand all macro +# names in the source code. If set to NO (the default) only conditional +# compilation will be performed. Macro expansion can be done in a controlled +# way by setting EXPAND_ONLY_PREDEF to YES. + +MACRO_EXPANSION = NO + +# If the EXPAND_ONLY_PREDEF and MACRO_EXPANSION tags are both set to YES +# then the macro expansion is limited to the macros specified with the +# PREDEFINED and EXPAND_AS_DEFINED tags. + +EXPAND_ONLY_PREDEF = NO + +# If the SEARCH_INCLUDES tag is set to YES (the default) the includes files +# in the INCLUDE_PATH (see below) will be search if a #include is found. + +SEARCH_INCLUDES = YES + +# The INCLUDE_PATH tag can be used to specify one or more directories that +# contain include files that are not input files but should be processed by +# the preprocessor. + +INCLUDE_PATH = + +# You can use the INCLUDE_FILE_PATTERNS tag to specify one or more wildcard +# patterns (like *.h and *.hpp) to filter out the header-files in the +# directories. If left blank, the patterns specified with FILE_PATTERNS will +# be used. + +INCLUDE_FILE_PATTERNS = + +# The PREDEFINED tag can be used to specify one or more macro names that +# are defined before the preprocessor is started (similar to the -D option of +# gcc). The argument of the tag is a list of macros of the form: name +# or name=definition (no spaces). If the definition and the = are +# omitted =1 is assumed. To prevent a macro definition from being +# undefined via #undef or recursively expanded use the := operator +# instead of the = operator. + +PREDEFINED = + +# If the MACRO_EXPANSION and EXPAND_ONLY_PREDEF tags are set to YES then +# this tag can be used to specify a list of macro names that should be expanded. +# The macro definition that is found in the sources will be used. +# Use the PREDEFINED tag if you want to use a different macro definition. + +EXPAND_AS_DEFINED = + +# If the SKIP_FUNCTION_MACROS tag is set to YES (the default) then +# doxygen's preprocessor will remove all function-like macros that are alone +# on a line, have an all uppercase name, and do not end with a semicolon. Such +# function macros are typically used for boiler-plate code, and will confuse +# the parser if not removed. + +SKIP_FUNCTION_MACROS = YES + +#--------------------------------------------------------------------------- +# Configuration::additions related to external references +#--------------------------------------------------------------------------- + +# The TAGFILES option can be used to specify one or more tagfiles. +# Optionally an initial location of the external documentation +# can be added for each tagfile. The format of a tag file without +# this location is as follows: +# TAGFILES = file1 file2 ... +# Adding location for the tag files is done as follows: +# TAGFILES = file1=loc1 "file2 = loc2" ... +# where "loc1" and "loc2" can be relative or absolute paths or +# URLs. If a location is present for each tag, the installdox tool +# does not have to be run to correct the links. +# Note that each tag file must have a unique name +# (where the name does NOT include the path) +# If a tag file is not located in the directory in which doxygen +# is run, you must also specify the path to the tagfile here. + +TAGFILES = + +# When a file name is specified after GENERATE_TAGFILE, doxygen will create +# a tag file that is based on the input files it reads. + +GENERATE_TAGFILE = + +# If the ALLEXTERNALS tag is set to YES all external classes will be listed +# in the class index. If set to NO only the inherited external classes +# will be listed. + +ALLEXTERNALS = NO + +# If the EXTERNAL_GROUPS tag is set to YES all external groups will be listed +# in the modules index. If set to NO, only the current project's groups will +# be listed. + +EXTERNAL_GROUPS = YES + +# The PERL_PATH should be the absolute path and name of the perl script +# interpreter (i.e. the result of `which perl'). + +PERL_PATH = /usr/bin/perl + +#--------------------------------------------------------------------------- +# Configuration options related to the dot tool +#--------------------------------------------------------------------------- + +# If the CLASS_DIAGRAMS tag is set to YES (the default) Doxygen will +# generate a inheritance diagram (in HTML, RTF and LaTeX) for classes with base +# or super classes. Setting the tag to NO turns the diagrams off. Note that +# this option is superseded by the HAVE_DOT option below. This is only a +# fallback. It is recommended to install and use dot, since it yields more +# powerful graphs. + +CLASS_DIAGRAMS = YES + +# You can define message sequence charts within doxygen comments using the \msc +# command. Doxygen will then run the mscgen tool (see http://www.mcternan.me.uk/mscgen/) to +# produce the chart and insert it in the documentation. The MSCGEN_PATH tag allows you to +# specify the directory where the mscgen tool resides. If left empty the tool is assumed to +# be found in the default search path. + +MSCGEN_PATH = + +# If set to YES, the inheritance and collaboration graphs will hide +# inheritance and usage relations if the target is undocumented +# or is not a class. + +HIDE_UNDOC_RELATIONS = YES + +# If you set the HAVE_DOT tag to YES then doxygen will assume the dot tool is +# available from the path. This tool is part of Graphviz, a graph visualization +# toolkit from AT&T and Lucent Bell Labs. The other options in this section +# have no effect if this option is set to NO (the default) + +HAVE_DOT = YES + +# If the CLASS_GRAPH and HAVE_DOT tags are set to YES then doxygen +# will generate a graph for each documented class showing the direct and +# indirect inheritance relations. Setting this tag to YES will force the +# the CLASS_DIAGRAMS tag to NO. + +CLASS_GRAPH = YES + +# If the COLLABORATION_GRAPH and HAVE_DOT tags are set to YES then doxygen +# will generate a graph for each documented class showing the direct and +# indirect implementation dependencies (inheritance, containment, and +# class references variables) of the class with other documented classes. + +COLLABORATION_GRAPH = YES + +# If the GROUP_GRAPHS and HAVE_DOT tags are set to YES then doxygen +# will generate a graph for groups, showing the direct groups dependencies + +GROUP_GRAPHS = YES + +# If the UML_LOOK tag is set to YES doxygen will generate inheritance and +# collaboration diagrams in a style similar to the OMG's Unified Modeling +# Language. + +UML_LOOK = NO + +# If set to YES, the inheritance and collaboration graphs will show the +# relations between templates and their instances. + +TEMPLATE_RELATIONS = YES + +# If the ENABLE_PREPROCESSING, SEARCH_INCLUDES, INCLUDE_GRAPH, and HAVE_DOT +# tags are set to YES then doxygen will generate a graph for each documented +# file showing the direct and indirect include dependencies of the file with +# other documented files. + +INCLUDE_GRAPH = YES + +# If the ENABLE_PREPROCESSING, SEARCH_INCLUDES, INCLUDED_BY_GRAPH, and +# HAVE_DOT tags are set to YES then doxygen will generate a graph for each +# documented header file showing the documented files that directly or +# indirectly include this file. + +INCLUDED_BY_GRAPH = YES + +# If the CALL_GRAPH, SOURCE_BROWSER and HAVE_DOT tags are set to YES then doxygen will +# generate a call dependency graph for every global function or class method. +# Note that enabling this option will significantly increase the time of a run. +# So in most cases it will be better to enable call graphs for selected +# functions only using the \callgraph command. + +CALL_GRAPH = YES + +# If the CALLER_GRAPH, SOURCE_BROWSER and HAVE_DOT tags are set to YES then doxygen will +# generate a caller dependency graph for every global function or class method. +# Note that enabling this option will significantly increase the time of a run. +# So in most cases it will be better to enable caller graphs for selected +# functions only using the \callergraph command. + +CALLER_GRAPH = YES + +# If the GRAPHICAL_HIERARCHY and HAVE_DOT tags are set to YES then doxygen +# will graphical hierarchy of all classes instead of a textual one. + +GRAPHICAL_HIERARCHY = YES + +# If the DIRECTORY_GRAPH, SHOW_DIRECTORIES and HAVE_DOT tags are set to YES +# then doxygen will show the dependencies a directory has on other directories +# in a graphical way. The dependency relations are determined by the #include +# relations between the files in the directories. + +DIRECTORY_GRAPH = YES + +# The DOT_IMAGE_FORMAT tag can be used to set the image format of the images +# generated by dot. Possible values are png, jpg, or gif +# If left blank png will be used. + +DOT_IMAGE_FORMAT = png + +# The tag DOT_PATH can be used to specify the path where the dot tool can be +# found. If left blank, it is assumed the dot tool can be found in the path. + +DOT_PATH = + +# The DOTFILE_DIRS tag can be used to specify one or more directories that +# contain dot files that are included in the documentation (see the +# \dotfile command). + +DOTFILE_DIRS = + +# The MAX_DOT_GRAPH_MAX_NODES tag can be used to set the maximum number of +# nodes that will be shown in the graph. If the number of nodes in a graph +# becomes larger than this value, doxygen will truncate the graph, which is +# visualized by representing a node as a red box. Note that doxygen if the number +# of direct children of the root node in a graph is already larger than +# MAX_DOT_GRAPH_NOTES then the graph will not be shown at all. Also note +# that the size of a graph can be further restricted by MAX_DOT_GRAPH_DEPTH. + +DOT_GRAPH_MAX_NODES = 50 + +# The MAX_DOT_GRAPH_DEPTH tag can be used to set the maximum depth of the +# graphs generated by dot. A depth value of 3 means that only nodes reachable +# from the root by following a path via at most 3 edges will be shown. Nodes +# that lay further from the root node will be omitted. Note that setting this +# option to 1 or 2 may greatly reduce the computation time needed for large +# code bases. Also note that the size of a graph can be further restricted by +# DOT_GRAPH_MAX_NODES. Using a depth of 0 means no depth restriction. + +MAX_DOT_GRAPH_DEPTH = 0 + +# Set the DOT_TRANSPARENT tag to YES to generate images with a transparent +# background. This is disabled by default, which results in a white background. +# Warning: Depending on the platform used, enabling this option may lead to +# badly anti-aliased labels on the edges of a graph (i.e. they become hard to +# read). + +DOT_TRANSPARENT = NO + +# Set the DOT_MULTI_TARGETS tag to YES allow dot to generate multiple output +# files in one run (i.e. multiple -o and -T options on the command line). This +# makes dot run faster, but since only newer versions of dot (>1.8.10) +# support this, this feature is disabled by default. + +DOT_MULTI_TARGETS = NO + +# If the GENERATE_LEGEND tag is set to YES (the default) Doxygen will +# generate a legend page explaining the meaning of the various boxes and +# arrows in the dot generated graphs. + +GENERATE_LEGEND = YES + +# If the DOT_CLEANUP tag is set to YES (the default) Doxygen will +# remove the intermediate dot files that are used to generate +# the various graphs. + +DOT_CLEANUP = YES + +#--------------------------------------------------------------------------- +# Configuration::additions related to the search engine +#--------------------------------------------------------------------------- + +# The SEARCHENGINE tag specifies whether or not a search engine should be +# used. If set to NO the values of all tags below this one will be ignored. + +SEARCHENGINE = YES diff --git a/docs/intro b/docs/intro new file mode 100644 index 00000000..c3451789 --- /dev/null +++ b/docs/intro @@ -0,0 +1,10 @@ +/// @mainpage KLEE +/// +/// @section main_intro Introduction +/// Welcome to KLEE. KLEE is a symbolic execution engine that works on LLVM +/// bitcode. +/// +/// @section Documentation +/// The documentation of KLEE is composed of the Doxygen documentation +/// of the code as well as the following documents: +/// - @subpage overview diff --git a/docs/overview b/docs/overview new file mode 100644 index 00000000..666a23d9 --- /dev/null +++ b/docs/overview @@ -0,0 +1,104 @@ +/// @page overview High level overview of KLEE. +/// This document contains a high level overview of the inner workings of KLEE. +/// +/// KLEE implements symbolic execution by interpreting LLVM bitcode. Symbolic +/// memory is defined by inserting special calls to KLEE (namely +/// klee_make_symbolic) +/// During execution, KLEE tracks all uses of symbolic memory. Constraints +/// on symbolic memory usage are collected. Memory +/// that is defined using previously declared symbolic memory become +/// symbolic as well. +/// Whenever a branch refering to symbolic memory is encountered, KLEE forks +/// the entire states and explores each side of the branch for which a possible +/// solution to the symbolic constraints can be found. +/// KLEE makes queries to STP to solve symbolic constraints. +/// +/// The rest of this document describes some of the important components of KLEE +/// +/// @section executor Interpreter +/// klee::Interpreter is the main abstract class defining the interface of the +/// bitcode interpreter. klee::Executor is the main concrete instance of this +/// class. +/// Application states (i.e. memory, registers and PC) are stored in instances of +/// class klee::ExecutionState. There is one such instance for each path beeing +/// executed (except when some states are merged together). +/// On a branch, if condition is symbolic, klee::Executor::fork returns a +/// klee::ExecutionState::StatePair which is a pair of ExecutionState to be +/// executed. +/// +/// @section memory Memory model +/// MemoryObject's represent allocation sites in the program (calls to malloc, stack +/// objects, global variables) +/// and, at least conceptually, can be thought of as the unique name for the object +/// allocated at that site. +/// ObjectState's are used to store the actual contents of a MemoryObject in a +/// particular ExecutionState (but +/// can be shared). I need better names for these two things. +/// +/// Each ExecutionState stores a mapping of MemoryObjects -> ObjectState using the +/// AddressSpace data +/// structure (implemented as an immutable tree so that copying is cheap and the +/// shared structure is exploited). +/// Each AddressSpace may "own" some subset of the ObjectStates in the mapping. When +/// an AddressSpace +/// is duplicated it loses ownership of the ObjectState in the map. Any subsequent +/// write to an ObjectState will +/// create a copy of the object (AddressSpace::getWriteable). This is the COW +/// mechanism (which gets used +/// for all objects, not just globals). +/// +/// From the point of view of the state and this mapping there is no distinction +/// between stack, heap, and global +/// objects. The only special handling for stack objects is that the MemoryObject is +/// marked as isLocal and the +/// MemoryObject is stored in the StackFrame alloca list. When the StackFrame is +/// popped these objects are +/// then unbound so that the state can no longer access the memory directly +/// (references to the memory object +/// may still remain in ReadExprs, but conceptually the actual memory is no longer +/// addressable). +/// +/// It is also important that the AddressSpace mapping is ordered. We use this when +/// we need to resolve a symbolic +/// address to an ObjectState by first getting a particular value for the symbolic +/// address, and using that value to start +/// looking for objects that the pointer can fall within. +/// Difference betweens MemoryObjects and ObjectStates ? +/// +/// @section expression Expressions +/// The various Expr classes mostly model the llvm instruction set. ref<Expr> is +/// used to maintain the reference count +/// but also embeds any constant expressions. In fact in the current code base +/// ConstantExprs should almost never be +/// created. Most of the Expr's are straightforward. Some of the most important ones +/// are Concat?Expr, which join +/// some number of bytes into a larger type, ExtractExpr which extracts smaller +/// types from larger ones, and ReadExpr +/// which is a symbolic array access. +/// +/// The way memory is implemented all accesses are broken down into byte level +/// operations. This means that the +/// memory system (by which I mean the ObjectState data structure) tends to use a +/// lot of ExtractExpr and Concat?Expr, +/// so it is very important that these expressions fold their operands when +/// possible. +/// +/// The ReadExpr is probably the most important one. Conceptually it is simply an +/// index and a list of (index, value) +/// updates (writes). The ReadExpr evaluates to all the values for which the two +/// indices can be equal. The ObjectState +/// structure uses a cache for concrete writes and for symbolic writes at concrete +/// indices, but for writes at symbolic +/// indices it must construct a list of such updates. These are stored in the +/// UpdateList and UpdateNode structures +/// which are again immutable data structures so that copy is cheap and the sharing +/// is exploited. +/// +/// @section searcher Searcher +/// Base classe: klee::Searcher. The Executor uses a Searcher to select the next +/// state (i.e. program instance following a single path) for which an +/// instruction +/// will be executed. There are multiple implementations of Searcher in klee, +/// implementing different search policies. klee::RandomSearcher selects the next state randomly. +/// klee::DFSSearcher uses a depth first approach. klee::MergingSearcher tries +/// to merge states ? |