CBMC
Loading...
Searching...
No Matches
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
axiomst Class Reference

#include <axioms.h>

+ Collaboration diagram for axiomst:

Public Member Functions

 axiomst (decision_proceduret &__dest, const std::unordered_set< symbol_exprt, irep_hash > &__address_taken, bool __verbose, const namespacet &__ns)
 
void set_to_true (exprt)
 
void set_to_false (exprt)
 
void emit ()
 
exprt translate (exprt) const
 

Protected Member Functions

exprt replace (exprt)
 
typet replace (typet)
 
void node (const exprt &)
 
void add (const state_ok_exprt &)
 
void ok_fc ()
 
void evaluate_fc ()
 
void add (const state_is_cstring_exprt &, bool recursive)
 
void is_cstring_fc ()
 
void is_dynamic_object_fc ()
 
void live_object ()
 
void live_object_fc ()
 
void writeable_object ()
 
void writeable_object_fc ()
 
void object_size ()
 
void object_size_fc ()
 
void is_sentinel_dll ()
 
void initial_state ()
 

Protected Attributes

decision_proceduret & dest
 
const std::unordered_set< symbol_exprt, irep_hash > & address_taken
 
bool verbose = false
 
const namespacet & ns
 
std::vector< exprt > constraints
 
std::unordered_map< exprt, symbol_exprt, irep_hash > replacement_map
 
std::map< irep_idt, std::size_t > counters
 
std::set< address_of_exprt > address_of_exprs
 
std::set< object_address_exprt > object_address_exprs
 
std::set< state_ok_exprt > ok_exprs
 
std::set< evaluate_exprt > evaluate_exprs
 
std::set< state_is_cstring_exprt > is_cstring_exprs
 
std::set< state_is_dynamic_object_exprt > is_dynamic_object_exprs
 
std::set< state_live_object_exprt > live_object_exprs
 
std::set< state_writeable_object_exprt > writeable_object_exprs
 
std::set< state_object_size_exprt > object_size_exprs
 
std::set< state_is_sentinel_dll_exprt > is_sentinel_dll_exprs
 
std::set< initial_state_exprt > initial_state_exprs
 

Detailed Description

Definition at line 28 of file axioms.h.

Constructor & Destructor Documentation

◆ axiomst()

axiomst::axiomst ( decision_proceduret &  __dest,
const std::unordered_set< symbol_exprt, irep_hash > &  __address_taken,
bool  __verbose,
const namespacet &  __ns 
)
inline

Definition at line 31 of file axioms.h.

Member Function Documentation

◆ add() [1/2]

void axiomst::add ( const state_is_cstring_exprt &  is_cstring_expr,
bool  recursive 
)
protected

Definition at line 700 of file axioms.cpp.

◆ add() [2/2]

void axiomst::add ( const state_ok_exprt &  ok_expr)
protected

Definition at line 628 of file axioms.cpp.

◆ emit()

void axiomst::emit ( )

Definition at line 749 of file axioms.cpp.

◆ evaluate_fc()

void axiomst::evaluate_fc ( )
protected

Definition at line 58 of file axioms.cpp.

◆ initial_state()

void axiomst::initial_state ( )
protected

Definition at line 324 of file axioms.cpp.

◆ is_cstring_fc()

void axiomst::is_cstring_fc ( )
protected

Definition at line 85 of file axioms.cpp.

◆ is_dynamic_object_fc()

void axiomst::is_dynamic_object_fc ( )
protected

Definition at line 219 of file axioms.cpp.

◆ is_sentinel_dll()

void axiomst::is_sentinel_dll ( )
protected

◆ live_object()

void axiomst::live_object ( )
protected

Definition at line 108 of file axioms.cpp.

◆ live_object_fc()

void axiomst::live_object_fc ( )
protected

Definition at line 126 of file axioms.cpp.

◆ node()

void axiomst::node ( const exprt &  src)
protected

Definition at line 399 of file axioms.cpp.

◆ object_size()

void axiomst::object_size ( )
protected

Definition at line 241 of file axioms.cpp.

◆ object_size_fc()

void axiomst::object_size_fc ( )
protected

Definition at line 278 of file axioms.cpp.

◆ ok_fc()

void axiomst::ok_fc ( )
protected

Definition at line 298 of file axioms.cpp.

◆ replace() [1/2]

exprt axiomst::replace ( exprt  src)
protected

Definition at line 359 of file axioms.cpp.

◆ replace() [2/2]

typet axiomst::replace ( typet  src)
protected

Definition at line 39 of file axioms.cpp.

◆ set_to_false()

void axiomst::set_to_false ( exprt  src)

Definition at line 34 of file axioms.cpp.

◆ set_to_true()

void axiomst::set_to_true ( exprt  src)

Definition at line 29 of file axioms.cpp.

◆ translate()

exprt axiomst::translate ( exprt  src) const

Definition at line 350 of file axioms.cpp.

◆ writeable_object()

void axiomst::writeable_object ( )
protected

Definition at line 146 of file axioms.cpp.

◆ writeable_object_fc()

void axiomst::writeable_object_fc ( )
protected

Definition at line 197 of file axioms.cpp.

Member Data Documentation

◆ address_of_exprs

std::set<address_of_exprt> axiomst::address_of_exprs
protected

Definition at line 61 of file axioms.h.

◆ address_taken

const std::unordered_set<symbol_exprt, irep_hash>& axiomst::address_taken
protected

Definition at line 48 of file axioms.h.

◆ constraints

std::vector<exprt> axiomst::constraints
protected

Definition at line 52 of file axioms.h.

◆ counters

std::map<irep_idt, std::size_t> axiomst::counters
protected

Definition at line 57 of file axioms.h.

◆ dest

decision_proceduret& axiomst::dest
protected

Definition at line 47 of file axioms.h.

◆ evaluate_exprs

std::set<evaluate_exprt> axiomst::evaluate_exprs
protected

Definition at line 69 of file axioms.h.

◆ initial_state_exprs

std::set<initial_state_exprt> axiomst::initial_state_exprs
protected

Definition at line 94 of file axioms.h.

◆ is_cstring_exprs

std::set<state_is_cstring_exprt> axiomst::is_cstring_exprs
protected

Definition at line 72 of file axioms.h.

◆ is_dynamic_object_exprs

std::set<state_is_dynamic_object_exprt> axiomst::is_dynamic_object_exprs
protected

Definition at line 76 of file axioms.h.

◆ is_sentinel_dll_exprs

std::set<state_is_sentinel_dll_exprt> axiomst::is_sentinel_dll_exprs
protected

Definition at line 91 of file axioms.h.

◆ live_object_exprs

std::set<state_live_object_exprt> axiomst::live_object_exprs
protected

Definition at line 79 of file axioms.h.

◆ ns

const namespacet& axiomst::ns
protected

Definition at line 50 of file axioms.h.

◆ object_address_exprs

std::set<object_address_exprt> axiomst::object_address_exprs
protected

Definition at line 63 of file axioms.h.

◆ object_size_exprs

std::set<state_object_size_exprt> axiomst::object_size_exprs
protected

Definition at line 87 of file axioms.h.

◆ ok_exprs

std::set<state_ok_exprt> axiomst::ok_exprs
protected

Definition at line 65 of file axioms.h.

◆ replacement_map

std::unordered_map<exprt, symbol_exprt, irep_hash> axiomst::replacement_map
protected

Definition at line 56 of file axioms.h.

◆ verbose

bool axiomst::verbose = false
protected

Definition at line 49 of file axioms.h.

◆ writeable_object_exprs

std::set<state_writeable_object_exprt> axiomst::writeable_object_exprs
protected

Definition at line 83 of file axioms.h.

The documentation for this class was generated from the following files: