cprover
invariant_propagationt Class Reference

#include <invariant_propagation.h>

Inheritance diagram for invariant_propagationt:
[legend]
Collaboration diagram for invariant_propagationt:
[legend]

Public Types

typedef ait< invariant_set_domaintbaset
 
- Public Types inherited from ait< invariant_set_domaint >
typedef goto_programt::const_targett locationt
 
- Public Types inherited from ai_baset
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_settlookup (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)
 
- Public Member Functions inherited from ait< invariant_set_domaint >
 ait ()
 
invariant_set_domaintoperator[] (locationt l)
 
const invariant_set_domaintoperator[] (locationt l) const
 
void clear () override
 
- Public Member Functions inherited from ai_baset
 ai_baset ()
 
virtual ~ai_baset ()
 
void operator() (const goto_programt &goto_program, const namespacet &ns)
 
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 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
 
- Protected Types inherited from ait< invariant_set_domaint >
typedef std::unordered_map< locationt, invariant_set_domaint, const_target_hashstate_mapt
 
- Protected Types inherited from ai_baset
typedef std::map< unsigned, locationtworking_sett
 
typedef std::set< irep_idtrecursion_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
 
- Protected Member Functions inherited from ait< invariant_set_domaint >
virtual statetget_state (locationt l) override
 
const statetfind_state (locationt l) const override
 
bool merge (const statet &src, locationt from, locationt to) override
 
statetmake_temporary_state (const statet &s) override
 
void fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) override
 
- Protected Member Functions inherited from ai_baset
virtual void initialize (const goto_functionst::goto_functiont &)
 
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 namespacetns
 
value_setstvalue_sets
 
inv_object_storet object_store
 
- Protected Attributes inherited from ait< invariant_set_domaint >
state_mapt state_map
 
- Protected Attributes inherited from ai_baset
recursion_sett recursion_set
 

Detailed Description

Definition at line 20 of file invariant_propagation.h.

Member Typedef Documentation

§ baset

§ object_listt

typedef std::list<unsigned> invariant_propagationt::object_listt
protected

Definition at line 56 of file invariant_propagation.h.

Constructor & Destructor Documentation

§ invariant_propagationt()

invariant_propagationt::invariant_propagationt ( const namespacet _ns,
value_setst _value_sets 
)
inline

Definition at line 24 of file invariant_propagation.h.

Member Function Documentation

§ add_objects() [1/2]

void invariant_propagationt::add_objects ( const goto_programt goto_program)
protected

§ add_objects() [2/2]

void invariant_propagationt::add_objects ( const goto_functionst goto_functions)
protected

§ check_type()

bool invariant_propagationt::check_type ( const typet type) const
protected

Definition at line 187 of file invariant_propagation.cpp.

References namespace_baset::follow(), irept::id(), and ns.

Referenced by get_objects_rec().

§ get_globals()

void invariant_propagationt::get_globals ( object_listt globals)
protected

§ get_objects()

void invariant_propagationt::get_objects ( const symbolt symbol,
object_listt dest 
)
protected

§ get_objects_rec()

void invariant_propagationt::get_objects_rec ( const exprt src,
std::list< exprt > &  dest 
)
protected

§ initialize() [1/2]

§ initialize() [2/2]

void invariant_propagationt::initialize ( const goto_functionst goto_functions)
virtual

Reimplemented from ai_baset.

Definition at line 228 of file invariant_propagation.cpp.

References forall_goto_functions, initialize(), and ai_baset::initialize().

§ lookup()

const invariant_sett& invariant_propagationt::lookup ( locationt  l) const
inline

Definition at line 34 of file invariant_propagation.h.

References initialize(), make_all_false(), make_all_true(), and simplify().

§ make_all_false()

void invariant_propagationt::make_all_false ( )

Definition at line 25 of file invariant_propagation.cpp.

References ait< invariant_set_domaint >::state_map.

Referenced by lookup().

§ make_all_true()

void invariant_propagationt::make_all_true ( )

Definition at line 19 of file invariant_propagation.cpp.

References ait< invariant_set_domaint >::state_map.

Referenced by lookup().

§ simplify() [1/2]

void invariant_propagationt::simplify ( goto_programt goto_program)

§ simplify() [2/2]

void invariant_propagationt::simplify ( goto_functionst goto_functions)

Definition at line 236 of file invariant_propagation.cpp.

References Forall_goto_functions, and simplify().

Member Data Documentation

§ ns

const namespacet& invariant_propagationt::ns
protected

§ object_store

inv_object_storet invariant_propagationt::object_store
protected

Definition at line 54 of file invariant_propagation.h.

Referenced by get_objects(), and initialize().

§ value_sets

value_setst& invariant_propagationt::value_sets
protected

Definition at line 52 of file invariant_propagation.h.

Referenced by initialize().


The documentation for this class was generated from the following files: