Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8

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 ?