cprover
constant_propagator_ait Class Reference

#include <constant_propagator.h>

+ Inheritance diagram for constant_propagator_ait:
+ Collaboration diagram for constant_propagator_ait:

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 (const irep_idt &function_identifier, 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
 Get a copy of the abstract state before the given instruction, without needing to know what kind of domain or history is used. More...
 
void clear () override
 Reset the abstract state. More...
 
- Public Member Functions inherited from ai_baset
 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< statetabstract_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 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...
 

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
 Get the state for the given location, creating it in a default way if it doesn't exist. More...
 
const statetfind_state (locationt l) const override
 Get the state for the given location if it already exists; throw an exception if it doesn't. More...
 
bool merge (const statet &src, locationt from, locationt to) override
 
std::unique_ptr< statetmake_temporary_state (const statet &s) override
 Make a copy of a state. More...
 
void fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) override
 
- Protected Member Functions inherited from ai_baset
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...
 
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)
 

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
 The work queue, sorted by location number. More...
 

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

Definition at line 189 of file constant_propagator.h.

◆ constant_propagator_ait() [4/4]

constant_propagator_ait::constant_propagator_ait ( const irep_idt function_identifier,
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.

Member Function Documentation

◆ replace() [1/2]

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

Definition at line 600 of file constant_propagator.cpp.

◆ replace() [2/2]

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

Definition at line 609 of file constant_propagator.cpp.

◆ replace_types_rec()

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

Definition at line 660 of file constant_propagator.cpp.

◆ 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.

◆ should_track_value

should_track_valuet constant_propagator_ait::should_track_value
protected

Definition at line 228 of file constant_propagator.h.


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