CBMC
custom_bitvector_analysist Class Reference

#include <custom_bitvector_analysis.h>

+ Inheritance diagram for custom_bitvector_analysist:
+ Collaboration diagram for custom_bitvector_analysist:

Public Types

typedef numberingt< irep_idtbitst
 
- Public Types inherited from ait< custom_bitvector_domaint >
typedef goto_programt::const_targett locationt
 
- Public Types inherited from ai_baset
typedef ai_domain_baset statet
 
typedef ai_storage_baset::cstate_ptrt cstate_ptrt
 
typedef ai_history_baset::trace_ptrt trace_ptrt
 
typedef ai_history_baset::trace_sett trace_sett
 
typedef ai_storage_baset::ctrace_set_ptrt ctrace_set_ptrt
 
typedef goto_programt::const_targett locationt
 

Public Member Functions

void instrument (goto_functionst &)
 
void check (const goto_modelt &, bool xml, std::ostream &)
 
exprt eval (const exprt &src, locationt loc)
 
unsigned get_bit_nr (const exprt &)
 
- Public Member Functions inherited from ait< custom_bitvector_domaint >
 ait ()
 
 ait (std::unique_ptr< ai_domain_factory_baset > &&df)
 
const custom_bitvector_domaintoperator[] (locationt l) const
 Find the analysis result for a given location. More...
 
- Public Member Functions inherited from ai_recursive_interproceduralt
 ai_recursive_interproceduralt (std::unique_ptr< ai_history_factory_baset > &&hf, std::unique_ptr< ai_domain_factory_baset > &&df, std::unique_ptr< ai_storage_baset > &&st, message_handlert &mh)
 
- Public Member Functions inherited from ai_baset
 ai_baset (std::unique_ptr< ai_history_factory_baset > &&hf, std::unique_ptr< ai_domain_factory_baset > &&df, std::unique_ptr< ai_storage_baset > &&st, message_handlert &mh)
 
virtual ~ai_baset ()
 
void operator() (const irep_idt &function_id, 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 abstract_goto_modelt &goto_model)
 Run abstract interpretation on a whole program. More...
 
void operator() (const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
 Run abstract interpretation on a single function. More...
 
virtual ctrace_set_ptrt abstract_traces_before (locationt l) const
 Returns all of the histories that have reached the start of the instruction. More...
 
virtual ctrace_set_ptrt abstract_traces_after (locationt l) const
 Returns all of the histories that have reached the end of the instruction. More...
 
virtual cstate_ptrt abstract_state_before (locationt l) const
 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 cstate_ptrt 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 cstate_ptrt abstract_state_before (const trace_ptrt &p) const
 The same interfaces but with histories. More...
 
virtual cstate_ptrt abstract_state_after (const trace_ptrt &p) const
 
virtual void clear ()
 Reset the abstract state. More...
 
virtual void output (const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
 Output the abstract states for a single function. More...
 
virtual jsont output_json (const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const
 Output the abstract states for a single function as JSON. More...
 
virtual xmlt output_xml (const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const
 Output the abstract states for a single function as XML. 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_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...
 

Public Attributes

bitst bits
 

Protected Member Functions

virtual void initialize (const goto_functionst &_goto_functions)
 Initialize all the abstract states for a whole program. More...
 
std::set< exprtaliases (const exprt &, locationt loc)
 
- Protected Member Functions inherited from ait< custom_bitvector_domaint >
virtual statetget_state (locationt l)
 
virtual statetget_state (trace_ptrt p)
 Get the state for the given history, creating it with the factory if it doesn't exist. More...
 
- Protected Member Functions inherited from ai_recursive_interproceduralt
bool visit_edge_function_call (const irep_idt &calling_function_id, trace_ptrt p_call, locationt l_return, const irep_idt &callee_function_id, working_sett &working_set, const goto_programt &callee, const goto_functionst &goto_functions, const namespacet &ns) override
 
- Protected Member Functions inherited from ai_baset
virtual void initialize (const irep_idt &function_id, const goto_programt &goto_program)
 Initialize all the abstract states for a single function. More...
 
virtual void initialize (const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function)
 Initialize all the abstract states for a single function. More...
 
virtual void finalize ()
 Override this to add a cleanup or post-processing step after fixedpoint has run. More...
 
trace_ptrt 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...
 
trace_ptrt 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...
 
trace_ptrt get_next (working_sett &working_set)
 Get the next location from the work queue. More...
 
void put_in_working_set (working_sett &working_set, trace_ptrt t)
 
virtual bool fixedpoint (trace_ptrt starting_trace, const irep_idt &function_id, 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 (trace_ptrt starting_trace, const goto_functionst &goto_functions, const namespacet &ns)
 
virtual bool visit (const irep_idt &function_id, trace_ptrt p, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
 Perform one step of abstract interpretation from trace t Depending on the instruction type it may compute a number of "edges" or applications of the abstract transformer. More...
 
virtual bool visit_function_call (const irep_idt &function_id, trace_ptrt p_call, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
 
virtual bool visit_end_function (const irep_idt &function_id, trace_ptrt p, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
 
bool visit_edge (const irep_idt &function_id, trace_ptrt p, const irep_idt &to_function_id, locationt to_l, trace_ptrt caller_history, const namespacet &ns, working_sett &working_set)
 
virtual bool merge (const statet &src, trace_ptrt from, trace_ptrt to)
 Merge the state src, flowing from tracet from to tracet to, into the state currently stored for tracet to. More...
 
virtual std::unique_ptr< statetmake_temporary_state (const statet &s)
 Make a copy of a state. More...
 
virtual statetget_state (trace_ptrt p)
 Get the state for the given history, creating it with the factory if it doesn't exist. More...
 

Protected Attributes

local_may_alias_factoryt local_may_alias_factory
 
- Protected Attributes inherited from ai_baset
std::unique_ptr< ai_history_factory_basethistory_factory
 For creating history objects. More...
 
std::unique_ptr< ai_domain_factory_basetdomain_factory
 For creating domain objects. More...
 
std::unique_ptr< ai_storage_basetstorage
 
message_handlertmessage_handler
 

Friends

class custom_bitvector_domaint
 

Additional Inherited Members

- Protected Types inherited from ai_baset
typedef trace_sett working_sett
 The work queue, sorted using the history's ordering operator. More...
 

Detailed Description

Definition at line 143 of file custom_bitvector_analysis.h.

Member Typedef Documentation

◆ bitst

Member Function Documentation

◆ aliases()

std::set< exprt > custom_bitvector_analysist::aliases ( const exprt src,
locationt  loc 
)
protected

Definition at line 192 of file custom_bitvector_analysis.cpp.

◆ check()

void custom_bitvector_analysist::check ( const goto_modelt goto_model,
bool  xml,
std::ostream &  out 
)

Definition at line 771 of file custom_bitvector_analysis.cpp.

◆ eval()

exprt custom_bitvector_analysist::eval ( const exprt src,
locationt  loc 
)
inline

Definition at line 151 of file custom_bitvector_analysis.h.

◆ get_bit_nr()

unsigned custom_bitvector_analysist::get_bit_nr ( const exprt string_expr)

Definition at line 177 of file custom_bitvector_analysis.cpp.

◆ initialize()

virtual void custom_bitvector_analysist::initialize ( const goto_functionst goto_functions)
inlineprotectedvirtual

Initialize all the abstract states for a whole program.

Override this to do custom per-analysis initialization.

Reimplemented from ai_baset.

Definition at line 162 of file custom_bitvector_analysis.h.

◆ instrument()

void custom_bitvector_analysist::instrument ( goto_functionst )

Definition at line 767 of file custom_bitvector_analysis.cpp.

Friends And Related Function Documentation

◆ custom_bitvector_domaint

friend class custom_bitvector_domaint
friend

Definition at line 168 of file custom_bitvector_analysis.h.

Member Data Documentation

◆ bits

bitst custom_bitvector_analysist::bits

Definition at line 159 of file custom_bitvector_analysis.h.

◆ local_may_alias_factory

local_may_alias_factoryt custom_bitvector_analysist::local_may_alias_factory
protected

Definition at line 170 of file custom_bitvector_analysis.h.


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