cprover
constant_propagator_ait Class Reference

#include <constant_propagator.h>

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

Public Types

typedef std::function< bool(const exprt &, const namespacet &)> should_track_valuet
 
- Public Types inherited from ait< constant_propagator_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

 constant_propagator_ait (const goto_functionst &goto_functions, should_track_valuet should_track_value=track_all_values)
 
 constant_propagator_ait (const goto_functiont &goto_function, should_track_valuet should_track_value=track_all_values)
 
 constant_propagator_ait (goto_modelt &goto_model, should_track_valuet should_track_value=track_all_values)
 
 constant_propagator_ait (goto_functionst::goto_functiont &goto_function, const namespacet &ns, should_track_valuet should_track_value=track_all_values)
 
- Public Member Functions inherited from ait< constant_propagator_domaint >
 ait ()
 
constant_propagator_domaintoperator[] (locationt l)
 
const constant_propagator_domaintoperator[] (locationt l) const
 
std::unique_ptr< statetabstract_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...
 
- Public Member Functions inherited from ai_baset
 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< statetabstract_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
 

Static Public Member Functions

static bool track_all_values (const exprt &, const namespacet &)
 

Public Attributes

dirtyt dirty
 

Protected Member Functions

void replace (goto_functionst::goto_functiont &, const namespacet &)
 
void replace (goto_functionst &, const namespacet &)
 
void replace_types_rec (const replace_symbolt &replace_const, exprt &expr)
 
- Protected Member Functions inherited from ait< constant_propagator_domaint >
virtual statetget_state (locationt l) override
 
const statetfind_state (locationt l) const override
 
bool merge (const statet &src, locationt from, locationt to) override
 
std::unique_ptr< 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_programt &)
 
virtual void initialize (const goto_functionst::goto_functiont &)
 
virtual void initialize (const goto_functionst &)
 
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

should_track_valuet should_track_value
 
- Protected Attributes inherited from ait< constant_propagator_domaint >
state_mapt state_map
 

Friends

class constant_propagator_domaint
 

Additional Inherited Members

- Protected Types inherited from ait< constant_propagator_domaint >
typedef std::unordered_map< locationt, constant_propagator_domaint, const_target_hash, pointee_address_equaltstate_mapt
 
- Protected Types inherited from ai_baset
typedef std::map< unsigned, locationtworking_sett
 

Detailed Description

Definition at line 162 of file constant_propagator.h.

Member Typedef Documentation

◆ should_track_valuet

typedef std::function<bool(const exprt &, const namespacet &)> constant_propagator_ait::should_track_valuet

Definition at line 166 of file constant_propagator.h.

Constructor & Destructor Documentation

◆ constant_propagator_ait() [1/4]

constant_propagator_ait::constant_propagator_ait ( const goto_functionst goto_functions,
should_track_valuet  should_track_value = track_all_values 
)
inlineexplicit

Definition at line 173 of file constant_propagator.h.

◆ constant_propagator_ait() [2/4]

constant_propagator_ait::constant_propagator_ait ( const goto_functiont goto_function,
should_track_valuet  should_track_value = track_all_values 
)
inlineexplicit

Definition at line 181 of file constant_propagator.h.

◆ constant_propagator_ait() [3/4]

constant_propagator_ait::constant_propagator_ait ( goto_modelt goto_model,
should_track_valuet  should_track_value = track_all_values 
)
inline

◆ constant_propagator_ait() [4/4]

constant_propagator_ait::constant_propagator_ait ( goto_functionst::goto_functiont goto_function,
const namespacet ns,
should_track_valuet  should_track_value = track_all_values 
)
inline

Definition at line 200 of file constant_propagator.h.

References ai_baset::operator()(), and replace().

Member Function Documentation

◆ replace() [1/2]

◆ replace() [2/2]

void constant_propagator_ait::replace ( goto_functionst goto_functions,
const namespacet ns 
)
protected

Definition at line 591 of file constant_propagator.cpp.

References Forall_goto_functions.

◆ replace_types_rec()

void constant_propagator_ait::replace_types_rec ( const replace_symbolt replace_const,
exprt expr 
)
protected

Definition at line 650 of file constant_propagator.cpp.

References Forall_operands, and exprt::type().

◆ track_all_values()

static bool constant_propagator_ait::track_all_values ( const exprt ,
const namespacet  
)
inlinestatic

Definition at line 168 of file constant_propagator.h.

Friends And Related Function Documentation

◆ constant_propagator_domaint

friend class constant_propagator_domaint
friend

Definition at line 214 of file constant_propagator.h.

Member Data Documentation

◆ dirty

dirtyt constant_propagator_ait::dirty

Definition at line 211 of file constant_propagator.h.

Referenced by constant_propagator_domaint::transform().

◆ should_track_value

should_track_valuet constant_propagator_ait::should_track_value
protected

Definition at line 228 of file constant_propagator.h.

Referenced by constant_propagator_domaint::assign_rec().


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