cprover
|
#include <invariant_propagation.h>
Public Types | |
typedef ait< invariant_set_domaint > | baset |
![]() | |
typedef goto_programt::const_targett | locationt |
![]() | |
typedef ai_domain_baset | statet |
typedef goto_programt::const_targett | locationt |
Public Member Functions | |
invariant_propagationt (const namespacet &_ns, value_setst &_value_sets) | |
const invariant_sett & | lookup (locationt l) const |
virtual void | initialize (const goto_programt &goto_program) |
virtual void | initialize (const goto_functionst &goto_functions) |
void | make_all_true () |
void | make_all_false () |
void | simplify (goto_programt &goto_program) |
void | simplify (goto_functionst &goto_functions) |
![]() | |
ait () | |
invariant_set_domaint & | operator[] (locationt l) |
const invariant_set_domaint & | operator[] (locationt l) const |
std::unique_ptr< statet > | abstract_state_before (locationt t) const override |
Accessing individual domains at particular locations (without needing to know what kind of domain or history is used) A pointer to a copy as the method should be const and there are some non-trivial cases including merging domains, etc. More... | |
void | clear () override |
Resets the domain. More... | |
![]() | |
ai_baset () | |
virtual | ~ai_baset () |
void | operator() (const goto_programt &goto_program, const namespacet &ns) |
Running the interpreter. More... | |
void | operator() (const goto_functionst &goto_functions, const namespacet &ns) |
void | operator() (const goto_modelt &goto_model) |
void | operator() (const goto_functionst::goto_functiont &goto_function, const namespacet &ns) |
virtual std::unique_ptr< statet > | abstract_state_after (locationt l) const |
Returns the abstract state after the given instruction. More... | |
virtual void | output (const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const |
void | output (const goto_modelt &goto_model, std::ostream &out) const |
void | output (const namespacet &ns, const goto_programt &goto_program, std::ostream &out) const |
void | output (const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const |
virtual jsont | output_json (const namespacet &ns, const goto_functionst &goto_functions) const |
Output the domains for the whole program as JSON. More... | |
jsont | output_json (const goto_modelt &goto_model) const |
jsont | output_json (const namespacet &ns, const goto_programt &goto_program) const |
jsont | output_json (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const |
virtual xmlt | output_xml (const namespacet &ns, const goto_functionst &goto_functions) const |
Output the domains for the whole program as XML. More... | |
xmlt | output_xml (const goto_modelt &goto_model) const |
xmlt | output_xml (const namespacet &ns, const goto_programt &goto_program) const |
xmlt | output_xml (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const |
Protected Types | |
typedef std::list< unsigned > | object_listt |
![]() | |
typedef std::unordered_map< locationt, invariant_set_domaint, const_target_hash, pointee_address_equalt > | state_mapt |
![]() | |
typedef std::map< unsigned, locationt > | working_sett |
Protected Member Functions | |
void | add_objects (const goto_programt &goto_program) |
void | add_objects (const goto_functionst &goto_functions) |
void | get_objects (const symbolt &symbol, object_listt &dest) |
void | get_objects_rec (const exprt &src, std::list< exprt > &dest) |
void | get_globals (object_listt &globals) |
bool | check_type (const typet &type) const |
![]() | |
virtual statet & | get_state (locationt l) override |
const statet & | find_state (locationt l) const override |
bool | merge (const statet &src, locationt from, locationt to) override |
std::unique_ptr< statet > | make_temporary_state (const statet &s) override |
void | fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) override |
![]() | |
virtual void | initialize (const goto_functionst::goto_functiont &) |
virtual void | finalize () |
void | entry_state (const goto_programt &) |
void | entry_state (const goto_functionst &) |
virtual void | output (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier, std::ostream &out) const |
virtual jsont | output_json (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const |
Output the domains 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 domains for a single function as XML. More... | |
locationt | get_next (working_sett &working_set) |
void | put_in_working_set (working_sett &working_set, locationt l) |
bool | fixedpoint (const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
void | sequential_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) |
void | concurrent_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) |
bool | visit (locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
bool | do_function_call_rec (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 (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) |
Protected Attributes | |
const namespacet & | ns |
value_setst & | value_sets |
inv_object_storet | object_store |
![]() | |
state_mapt | state_map |
Definition at line 20 of file invariant_propagation.h.
Definition at line 48 of file invariant_propagation.h.
|
protected |
Definition at line 56 of file invariant_propagation.h.
|
inline |
Definition at line 24 of file invariant_propagation.h.
|
protected |
Definition at line 31 of file invariant_propagation.cpp.
References forall_goto_program_instructions, goto_programt::get_decl_identifiers(), get_globals(), get_objects(), goto_program, namespacet::lookup(), and ns.
Referenced by initialize().
|
protected |
Definition at line 119 of file invariant_propagation.cpp.
References forall_goto_functions, forall_goto_program_instructions, get_globals(), get_local_identifiers(), get_objects(), goto_program, namespacet::lookup(), and ns.
|
protected |
Definition at line 183 of file invariant_propagation.cpp.
References namespace_baset::follow(), irept::id(), and ns.
Referenced by get_objects_rec().
|
protected |
Definition at line 170 of file invariant_propagation.cpp.
References get_objects(), namespacet::get_symbol_table(), ns, and symbol_table_baset::symbols.
Referenced by add_objects().
|
protected |
Definition at line 77 of file invariant_propagation.cpp.
References inv_object_storet::add(), get_objects_rec(), object_store, and symbolt::symbol_expr().
Referenced by add_objects(), and get_globals().
|
protected |
Definition at line 89 of file invariant_propagation.cpp.
References check_type(), struct_union_typet::components(), namespace_baset::follow(), irept::id(), ns, to_struct_type(), and exprt::type().
Referenced by get_objects().
|
virtual |
Reimplemented from ai_baset.
Definition at line 203 of file invariant_propagation.cpp.
References add_objects(), forall_goto_program_instructions, goto_program, ai_baset::initialize(), goto_programt::instructions, invariant_sett::make_false(), invariant_sett::make_true(), ns, object_store, invariant_sett::set_namespace(), invariant_sett::set_object_store(), invariant_sett::set_value_sets(), and value_sets.
Referenced by initialize().
|
virtual |
Reimplemented from ai_baset.
Definition at line 224 of file invariant_propagation.cpp.
References forall_goto_functions, initialize(), and ai_baset::initialize().
|
inline |
Definition at line 34 of file invariant_propagation.h.
void invariant_propagationt::make_all_false | ( | ) |
Definition at line 25 of file invariant_propagation.cpp.
References ait< invariant_set_domaint >::state_map.
void invariant_propagationt::make_all_true | ( | ) |
Definition at line 19 of file invariant_propagation.cpp.
References ait< invariant_set_domaint >::state_map.
void invariant_propagationt::simplify | ( | goto_programt & | goto_program | ) |
Definition at line 238 of file invariant_propagation.cpp.
References Forall_goto_program_instructions, goto_program, invariant_sett::implies(), tvt::is_true(), ns, and invariant_sett::simplify().
Referenced by simplify().
void invariant_propagationt::simplify | ( | goto_functionst & | goto_functions | ) |
Definition at line 232 of file invariant_propagation.cpp.
References Forall_goto_functions, and simplify().
|
protected |
Definition at line 51 of file invariant_propagation.h.
Referenced by add_objects(), check_type(), get_globals(), get_objects_rec(), initialize(), and simplify().
|
protected |
Definition at line 54 of file invariant_propagation.h.
Referenced by get_objects(), and initialize().
|
protected |
Definition at line 52 of file invariant_propagation.h.
Referenced by initialize().