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.
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.
Definition at line 35 of file axioms.cpp.
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 |