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:

[フレーム]

[legend]

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:

/home/runner/work/cbmc/cbmc/src/cprover/axioms.h
/home/runner/work/cbmc/cbmc/src/cprover/axioms.cpp