cprover
|
#include <axioms.h>
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 |
|
inline |
|
protected |
Definition at line 701 of file axioms.cpp.
|
protected |
Definition at line 629 of file axioms.cpp.
void axiomst::emit | ( | ) |
Definition at line 750 of file axioms.cpp.
|
protected |
Definition at line 59 of file axioms.cpp.
|
protected |
Definition at line 325 of file axioms.cpp.
|
protected |
Definition at line 86 of file axioms.cpp.
|
protected |
Definition at line 220 of file axioms.cpp.
|
protected |
|
protected |
Definition at line 109 of file axioms.cpp.
|
protected |
Definition at line 127 of file axioms.cpp.
|
protected |
Definition at line 400 of file axioms.cpp.
|
protected |
Definition at line 242 of file axioms.cpp.
|
protected |
Definition at line 279 of file axioms.cpp.
|
protected |
Definition at line 299 of file axioms.cpp.
Definition at line 360 of file axioms.cpp.
Definition at line 40 of file axioms.cpp.
void axiomst::set_to_false | ( | exprt | src | ) |
Definition at line 35 of file axioms.cpp.
void axiomst::set_to_true | ( | exprt | src | ) |
Definition at line 30 of file axioms.cpp.
Definition at line 351 of file axioms.cpp.
|
protected |
Definition at line 147 of file axioms.cpp.
|
protected |
Definition at line 198 of file axioms.cpp.
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |