|
| program_state (const extrinsic_state &ext_state) |
|
| program_state (const program_state &other) |
|
program_state & | operator= (const program_state &other) |
|
| program_state (program_state &&other) |
|
| ~program_state () |
|
hashval_t | hash () const |
|
bool | operator== (const program_state &other) const |
|
bool | operator!= (const program_state &other) const |
|
void | print (const extrinsic_state &ext_state, pretty_printer *pp) const |
|
void | dump_to_pp (const extrinsic_state &ext_state, bool simple, bool multiline, pretty_printer *pp) const |
|
void | dump_to_file (const extrinsic_state &ext_state, bool simple, bool multiline, FILE *outf) const |
|
void | dump (const extrinsic_state &ext_state, bool simple) const |
|
void | dump () const |
|
std::unique_ptr< json::object > | to_json (const extrinsic_state &ext_state) const |
|
std::unique_ptr< text_art::tree_widget > | make_dump_widget (const text_art::dump_widget_info &dwi) const |
|
void | push_frame (const extrinsic_state &ext_state, const function &fun) |
|
const function * | get_current_function () const |
|
void | push_call (exploded_graph &eg, exploded_node *enode, const gcall *call_stmt, uncertainty_t *uncertainty) |
|
void | returning_call (exploded_graph &eg, exploded_node *enode, const gcall *call_stmt, uncertainty_t *uncertainty) |
|
bool | on_edge (exploded_graph &eg, exploded_node *enode, const superedge *succ, uncertainty_t *uncertainty) |
|
program_state | prune_for_point (exploded_graph &eg, const program_point &point, exploded_node *enode_for_diag, uncertainty_t *uncertainty) const |
|
tree | get_representative_tree (const svalue *sval) const |
|
bool | can_purge_p (const extrinsic_state &ext_state, const svalue *sval) const |
|
bool | can_purge_base_region_p (const extrinsic_state &ext_state, const region *base_reg) const |
|
bool | can_merge_with_p (const program_state &other, const extrinsic_state &ext_state, const program_point &point, program_state *out) const |
|
void | validate (const extrinsic_state &ext_state) const |
|
bool | replay_call_summary (call_summary_replay &r, const program_state &summary) |
|
void | impl_call_analyzer_dump_state (const gcall *call, const extrinsic_state &ext_state, region_model_context *ctxt) |
|
A class for representing the state of interest at a given path of
analysis.
Currently this is a combination of:
(a) a region_model, giving:
(a.1) a hierarchy of memory regions
(a.2) values for the regions
(a.3) inequalities between values
(b) sm_state_maps per state machine, giving a sparse mapping of
values to states.