|
| ai_baset () |
|
virtual | ~ai_baset () |
|
void | operator() (const irep_idt &function_identifier, const goto_programt &goto_program, const namespacet &ns) |
| Run abstract interpretation on a single function. More...
|
|
void | operator() (const goto_functionst &goto_functions, const namespacet &ns) |
| Run abstract interpretation on a whole program. More...
|
|
void | operator() (const goto_modelt &goto_model) |
| Run abstract interpretation on a whole program. More...
|
|
void | operator() (const irep_idt &function_identifier, const goto_functionst::goto_functiont &goto_function, const namespacet &ns) |
| Run abstract interpretation on a single function. More...
|
|
virtual std::unique_ptr< statet > | abstract_state_before (locationt l) const =0 |
| Get a copy of the abstract state before the given instruction, without needing to know what kind of domain or history is used. More...
|
|
virtual std::unique_ptr< statet > | abstract_state_after (locationt l) const |
| Get a copy of the abstract state after the given instruction, without needing to know what kind of domain or history is used. More...
|
|
virtual void | clear () |
| Reset the abstract state. More...
|
|
virtual void | output (const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const |
| Output the abstract states for a whole program. More...
|
|
void | output (const goto_modelt &goto_model, std::ostream &out) const |
| Output the abstract states for a whole program. More...
|
|
void | output (const namespacet &ns, const goto_programt &goto_program, std::ostream &out) const |
| Output the abstract states for a function. More...
|
|
void | output (const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const |
| Output the abstract states for a function. More...
|
|
virtual jsont | output_json (const namespacet &ns, const goto_functionst &goto_functions) const |
| Output the abstract states for the whole program as JSON. More...
|
|
jsont | output_json (const goto_modelt &goto_model) const |
| Output the abstract states for a whole program as JSON. More...
|
|
jsont | output_json (const namespacet &ns, const goto_programt &goto_program) const |
| Output the abstract states for a single function as JSON. More...
|
|
jsont | output_json (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const |
| Output the abstract states for a single function as JSON. More...
|
|
virtual xmlt | output_xml (const namespacet &ns, const goto_functionst &goto_functions) const |
| Output the abstract states for the whole program as XML. More...
|
|
xmlt | output_xml (const goto_modelt &goto_model) const |
| Output the abstract states for the whole program as XML. More...
|
|
xmlt | output_xml (const namespacet &ns, const goto_programt &goto_program) const |
| Output the abstract states for a single function as XML. More...
|
|
xmlt | output_xml (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const |
| Output the abstract states for a single function as XML. More...
|
|
|
virtual void | initialize (const goto_programt &goto_program) |
| Initialize all the abstract states for a single function. More...
|
|
virtual void | initialize (const goto_functionst::goto_functiont &goto_function) |
| Initialize all the abstract states for a single function. More...
|
|
virtual void | initialize (const goto_functionst &goto_functions) |
| Initialize all the abstract states for a whole program. More...
|
|
virtual void | finalize () |
| Override this to add a cleanup or post-processing step after fixedpoint has run. More...
|
|
void | entry_state (const goto_programt &goto_program) |
| Set the abstract state of the entry location of a single function to the entry state required by the analysis. More...
|
|
void | entry_state (const goto_functionst &goto_functions) |
| Set the abstract state of the entry location of a whole program to the entry state required by the analysis. More...
|
|
virtual void | output (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier, std::ostream &out) const |
| Output the abstract states for a single function. More...
|
|
virtual jsont | output_json (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const |
| Output the abstract states for a single function as JSON. More...
|
|
virtual xmlt | output_xml (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const |
| Output the abstract states for a single function as XML. More...
|
|
locationt | get_next (working_sett &working_set) |
| Get the next location from the work queue. More...
|
|
void | put_in_working_set (working_sett &working_set, locationt l) |
|
bool | fixedpoint (const irep_idt &function_identifier, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
| Run the fixedpoint algorithm until it reaches a fixed point. More...
|
|
virtual void | fixedpoint (const goto_functionst &goto_functions, const namespacet &ns)=0 |
|
void | sequential_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) |
|
void | concurrent_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) |
|
bool | visit (const irep_idt &function_identifier, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
| Perform one step of abstract interpretation from location l Depending on the instruction type it may compute a number of "edges" or applications of the abstract transformer. More...
|
|
bool | do_function_call_rec (const irep_idt &calling_function_identifier, locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, const goto_functionst &goto_functions, const namespacet &ns) |
|
bool | do_function_call (const irep_idt &calling_function_identifier, locationt l_call, locationt l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, const namespacet &ns) |
|
virtual bool | merge (const statet &src, locationt from, locationt to)=0 |
|
virtual bool | merge_shared (const statet &src, locationt from, locationt to, const namespacet &ns)=0 |
|
virtual statet & | get_state (locationt l)=0 |
| Get the state for the given location, creating it in a default way if it doesn't exist. More...
|
|
virtual const statet & | find_state (locationt l) const =0 |
| Get the state for the given location if it already exists; throw an exception if it doesn't. More...
|
|
virtual std::unique_ptr< statet > | make_temporary_state (const statet &s)=0 |
| Make a copy of a state. More...
|
|
The basic interface of an abstract interpreter.
This should be enough to create, run and query an abstract interpreter.
Note: this is just a base class. ait should be used instead.
Definition at line 32 of file ai.h.
virtual std::unique_ptr<statet> ai_baset::abstract_state_before |
( |
locationt |
l | ) |
const |
|
pure virtual |
Get a copy of the abstract state before the given instruction, without needing to know what kind of domain or history is used.
Note: intended for users of the abstract interpreter; derived classes should use get_state or find_state to access the actual underlying state. PRECONDITION(l is dereferenceable)
- Parameters
-
l | The location before which we want the abstract state |
- Returns
- The abstract state before
l
. We return a pointer to a copy as the method should be const and there are some non-trivial cases including merging abstract states, etc.
Implemented in ait< domainT >, ait< escape_domaint >, ait< invariant_set_domaint >, ait< global_may_alias_domaint >, ait< rd_range_domaint >, ait< constant_propagator_domaint >, ait< uninitialized_domaint >, ait< custom_bitvector_domaint >, and ait< dep_graph_domaint >.