memory_model.h File Reference

#include <ilang/mcm/ast_helper.h>
#include <ilang/mcm/axiom_helper.h>
#include <ilang/target-smt/z3_expr_adapter.h>

Go to the source code of this file.

Classes
class	ilang::TraceStep
	The class for trace step (an instance of instruction) As in the unrolling, there may be multiple instances of the same instructions, so we have the trace steps. More...
class	ilang::MemoryModel
	The base class for memory models. More...

Namespaces
	ilang

Macros
#define	FINAL_STEP_SUFFIX   "final"

Enumerations
enum	ilang::AccessType { READ, WRITE, EITHER }
	Type of state read or write.

Detailed Description

Header for memory model