This wiki aims to summarize the class diagrams for the main library packages in TracerX that is built upon KLEE (version 1.0) repository.

1. Overview

In TracerX library, the klee and kleaver code is organized as follows:

• lib/Basic: Low level support for both klee and kleaver, independent of LLVM.
• lib/Support: Higher level support that is only used by klee, and using LLVM facilities (data structures, utilities, etc.) mainly.
• lib/Expr: The core kleaver expression library.
• lib/Solver: The kleaver solver library.
• lib/Module: klee facilities to function together with LLVM modules, which include the shadow module/instruction structures used during execution.
• lib/Core: The core symbolic virtual machine

2. Class Diagrams

2.1. lib/Basic

_____________________________________________________________

2.2. lib/Support

2.2.1 Overview

2.2.2 Klee Namespace

_____________________________________________________________

2.3. lib/Expr

2.3.1 Overview

2.3.2 Klee Namespace

---

2.4. lib/Solver

2.4.1 Overview

2.4.2 Klee Namespace

---

2.5. lib/Module

2.5.1 Overview

2.5.2 Klee Namespace

---

2.6. lib/Core

2.6.1 Overview

2.6.2 Klee Namespace (Please click on Figure and zoom in for better view)

_____________________________________________________________

3. TX Classes

Based on the current design of TX, the following classes can be identified, namely:

• TxPCConstraint
• TxAllocationContext
• TxVariable
• TxInterpolantValue
• TxStateAddress
• TxStateValue
• TxPrettyExpressionBuilder
• TxPartitionHelper
• TxTreeNode
• TxStore
• TxPathCondition
• TxSubsumptionTable
• TxSubsumptionTableEntry
• TxExprHelper
• TxDependency
• TxStoreEntry
• TxAllocationInfo
• TxShadowArray
• TxSpeculationHelper
• TxWPHelper
• TxWeakestPreCondition
• TxTree

3.1. TX Class Diagram(Please click on Figure and zoom in for better view)

_____________________________________________________________