CBMC
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Public Attributes | Protected Member Functions | Protected Attributes | Friends | List of all members
custom_bitvector_analysist Class Reference

#include <custom_bitvector_analysis.h>

+ Inheritance diagram for custom_bitvector_analysist:
[フレーム]
[legend]
+ Collaboration diagram for custom_bitvector_analysist:
[フレーム]
[legend]

Public Types

typedef numberingt< irep_idt >  bitst
 
- 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_domaint &  operator[] (locationt l) const
  Find the analysis result for a given location.
 
- 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.
 
void  operator() (const goto_functionst &goto_functions, const namespacet &ns)
  Run abstract interpretation on a whole program.
 
void  operator() (const abstract_goto_modelt &goto_model)
  Run abstract interpretation on a whole program.
 
void  operator() (const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
  Run abstract interpretation on a single function.
 
virtual ctrace_set_ptrt  abstract_traces_before (locationt l) const
  Returns all of the histories that have reached the start of the instruction.
 
virtual ctrace_set_ptrt  abstract_traces_after (locationt l) const
  Returns all of the histories that have reached the end of the instruction.
 
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.
 
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.
 
virtual cstate_ptrt  abstract_state_before (const trace_ptrt &p) const
  The same interfaces but with histories.
 
virtual cstate_ptrt  abstract_state_after (const trace_ptrt &p) const
 
virtual void  clear ()
  Reset the abstract state.
 
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.
 
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.
 
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.
 
virtual void  output (const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
  Output the abstract states for a whole program.
 
void  output (const goto_modelt &goto_model, std::ostream &out) const
  Output the abstract states for a whole program.
 
void  output (const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const
  Output the abstract states for a function.
 
virtual jsont  output_json (const namespacet &ns, const goto_functionst &goto_functions) const
  Output the abstract states for the whole program as JSON.
 
jsont  output_json (const goto_modelt &goto_model) const
  Output the abstract states for a whole program as JSON.
 
jsont  output_json (const namespacet &ns, const goto_programt &goto_program) const
  Output the abstract states for a single function as JSON.
 
jsont  output_json (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
  Output the abstract states for a single function as JSON.
 
virtual xmlt  output_xml (const namespacet &ns, const goto_functionst &goto_functions) const
  Output the abstract states for the whole program as XML.
 
xmlt  output_xml (const goto_modelt &goto_model) const
  Output the abstract states for the whole program as XML.
 
xmlt  output_xml (const namespacet &ns, const goto_programt &goto_program) const
  Output the abstract states for a single function as XML.
 
xmlt  output_xml (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
  Output the abstract states for a single function as XML.
 

Public Attributes

bitst  bits
 

Protected Member Functions

virtual void  initialize (const goto_functionst &_goto_functions)
  Initialize all the abstract states for a whole program.
 
std::set< exprt >  aliases (const exprt &, locationt loc)
 
- Protected Member Functions inherited from ait< custom_bitvector_domaint >
virtual statet &  get_state (locationt l)
 
virtual statet &  get_state (trace_ptrt p)
  Get the state for the given history, creating it with the factory if it doesn't exist.
 
- 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.
 
virtual void  initialize (const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function)
  Initialize all the abstract states for a single function.
 
virtual void  finalize ()
  Override this to add a cleanup or post-processing step after fixedpoint has run.
 
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.
 
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.
 
trace_ptrt  get_next (working_sett &working_set)
  Get the next location from the work queue.
 
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.
 
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.
 
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.
 
virtual std::unique_ptr< statet >  make_temporary_state (const statet &s)
  Make a copy of a state.
 

Protected Attributes

local_may_alias_factoryt  local_may_alias_factory
 
- Protected Attributes inherited from ai_baset
std::unique_ptr< ai_history_factory_baset >  history_factory
  For creating history objects.
 
std::unique_ptr< ai_domain_factory_baset >  domain_factory
  For creating domain objects.
 
std::unique_ptr< ai_storage_baset >  storage
 
message_handlert &  message_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.
 

Detailed Description

Definition at line 143 of file custom_bitvector_analysis.h.

Member Typedef Documentation

◆  bitst

typedef numberingt<irep_idt> custom_bitvector_analysist::bitst

Definition at line 158 of file custom_bitvector_analysis.h.

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 Symbol 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:

AltStyle によって変換されたページ (->オリジナル) /