CBMC
Public Types | Public Member Functions | Static Public Member Functions | Protected Types | Protected Member Functions | Static Protected Member Functions | Protected Attributes | List of all members
static_analysis_baset Class Referenceabstract

#include <static_analysis.h>

+ Inheritance diagram for static_analysis_baset:
+ Collaboration diagram for static_analysis_baset:

Public Types

typedef domain_baset statet
 
typedef goto_programt::const_targett locationt
 

Public Member Functions

 static_analysis_baset (const namespacet &_ns)
 
virtual void initialize (const goto_programt &goto_program)
 
virtual void initialize (const goto_functionst &goto_functions)
 
virtual void update (const goto_programt &goto_program)
 
virtual void update (const goto_functionst &goto_functions)
 
virtual void operator() (const irep_idt &function_identifier, const goto_programt &goto_program)
 
virtual void operator() (const goto_functionst &goto_functions)
 
virtual ~static_analysis_baset ()
 
virtual void clear ()
 
virtual void output (const goto_functionst &goto_functions, std::ostream &out) const
 
void output (const goto_programt &goto_program, std::ostream &out) const
 
virtual bool has_location (locationt l) const =0
 
void insert (locationt l)
 

Static Public Member Functions

static exprt get_guard (locationt from, locationt to)
 
static exprt get_return_lhs (locationt to)
 

Protected Types

typedef std::map< unsigned, locationt > working_sett
 
typedef std::set< irep_idt > functions_donet
 
typedef std::set< irep_idt > recursion_sett
 
typedef domain_baset::expr_sett expr_sett
 

Protected Member Functions

virtual void output (const goto_programt &goto_program, const irep_idt &identifier, std::ostream &out) const
 
locationt get_next (working_sett &working_set)
 
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)
 
virtual void fixedpoint (const goto_functionst &goto_functions)=0
 
void sequential_fixedpoint (const goto_functionst &goto_functions)
 
void concurrent_fixedpoint (const goto_functionst &goto_functions)
 
bool visit (const irep_idt &function_identifier, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
 
virtual bool merge (statet &a, const statet &b, locationt to)=0
 
virtual bool merge_shared (statet &a, const statet &b, locationt to)=0
 
void generate_states (const goto_functionst &goto_functions)
 
void generate_states (const goto_programt &goto_program)
 
void do_function_call_rec (const irep_idt &calling_function, locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
 
void do_function_call (const irep_idt &calling_function, locationt l_call, locationt l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, statet &new_state)
 
virtual void generate_state (locationt l)=0
 
virtual statet & get_state (locationt l)=0
 
virtual const statet & get_state (locationt l) const =0
 
virtual std::unique_ptr< statet > make_temporary_state (statet &s)=0
 
virtual void get_reference_set (locationt l, const exprt &expr, std::list< exprt > &dest)=0
 

Static Protected Member Functions

static locationt successor (locationt l)
 

Protected Attributes

const namespacet & ns
 
functions_donet functions_done
 
recursion_sett recursion_set
 
bool initialized
 

Detailed Description

Definition at line 99 of file static_analysis.h.

Member Typedef Documentation

◆ expr_sett

typedef domain_baset::expr_sett static_analysis_baset::expr_sett
protected

Definition at line 269 of file static_analysis.h.

◆ functions_donet

typedef std::set<irep_idt> static_analysis_baset::functions_donet
protected

Definition at line 229 of file static_analysis.h.

◆ locationt

typedef goto_programt::const_targett static_analysis_baset::locationt

Definition at line 103 of file static_analysis.h.

◆ recursion_sett

typedef std::set<irep_idt> static_analysis_baset::recursion_sett
protected

Definition at line 232 of file static_analysis.h.

◆ statet

typedef domain_baset static_analysis_baset::statet

Definition at line 102 of file static_analysis.h.

◆ working_sett

typedef std::map<unsigned, locationt> static_analysis_baset::working_sett
protected

Definition at line 185 of file static_analysis.h.

Constructor & Destructor Documentation

◆ static_analysis_baset()

static_analysis_baset::static_analysis_baset ( const namespacet &  _ns)
inlineexplicit

Definition at line 105 of file static_analysis.h.

◆ ~static_analysis_baset()

virtual static_analysis_baset::~static_analysis_baset ( )
inlinevirtual

Definition at line 141 of file static_analysis.h.

Member Function Documentation

◆ clear()

virtual void static_analysis_baset::clear ( )
inlinevirtual

Reimplemented in static_analysist< T >, and static_analysist< VSDT >.

Definition at line 145 of file static_analysis.h.

◆ concurrent_fixedpoint()

void static_analysis_baset::concurrent_fixedpoint ( const goto_functionst &  goto_functions)
protected

Definition at line 441 of file static_analysis.cpp.

◆ do_function_call()

void static_analysis_baset::do_function_call ( const irep_idt &  calling_function,
locationt  l_call,
locationt  l_return,
const goto_functionst &  goto_functions,
const goto_functionst::function_mapt::const_iterator  f_it,
const exprt::operandst &  arguments,
statet &  new_state 
)
protected

Definition at line 239 of file static_analysis.cpp.

◆ do_function_call_rec()

void static_analysis_baset::do_function_call_rec ( const irep_idt &  calling_function,
locationt  l_call,
locationt  l_return,
const exprt &  function,
const exprt::operandst &  arguments,
statet &  new_state,
const goto_functionst &  goto_functions 
)
protected

Definition at line 313 of file static_analysis.cpp.

◆ fixedpoint() [1/2]

virtual void static_analysis_baset::fixedpoint ( const goto_functionst &  goto_functions)
protectedpure virtual

Implemented in concurrency_aware_static_analysist< T >, static_analysist< T >, and static_analysist< VSDT >.

◆ fixedpoint() [2/2]

bool static_analysis_baset::fixedpoint ( const irep_idt &  function_identifier,
const goto_programt &  goto_program,
const goto_functionst &  goto_functions 
)
protected

Definition at line 158 of file static_analysis.cpp.

◆ generate_state()

virtual void static_analysis_baset::generate_state ( locationt  l)
protectedpure virtual

Implemented in static_analysist< T >, and static_analysist< VSDT >.

◆ generate_states() [1/2]

void static_analysis_baset::generate_states ( const goto_functionst &  goto_functions)
protected

Definition at line 103 of file static_analysis.cpp.

◆ generate_states() [2/2]

void static_analysis_baset::generate_states ( const goto_programt &  goto_program)
protected

Definition at line 110 of file static_analysis.cpp.

◆ get_guard()

exprt static_analysis_baset::get_guard ( locationt  from,
locationt  to 
)
static

Definition at line 23 of file static_analysis.cpp.

◆ get_next()

static_analysis_baset::locationt static_analysis_baset::get_next ( working_sett &  working_set)
protected

Definition at line 146 of file static_analysis.cpp.

◆ get_reference_set()

virtual void static_analysis_baset::get_reference_set ( locationt  l,
const exprt &  expr,
std::list< exprt > &  dest 
)
protectedpure virtual

Implemented in static_analysist< T >, and static_analysist< VSDT >.

◆ get_return_lhs()

exprt static_analysis_baset::get_return_lhs ( locationt  to)
static

Definition at line 35 of file static_analysis.cpp.

◆ get_state() [1/2]

virtual const statet& static_analysis_baset::get_state ( locationt  l) const
protectedpure virtual

Implemented in static_analysist< T >, and static_analysist< VSDT >.

◆ get_state() [2/2]

virtual statet& static_analysis_baset::get_state ( locationt  l)
protectedpure virtual

Implemented in static_analysist< T >, and static_analysist< VSDT >.

◆ has_location()

virtual bool static_analysis_baset::has_location ( locationt  l) const
pure virtual

Implemented in static_analysist< T >, and static_analysist< VSDT >.

◆ initialize() [1/2]

virtual void static_analysis_baset::initialize ( const goto_functionst &  goto_functions)
inlinevirtual

Definition at line 121 of file static_analysis.h.

◆ initialize() [2/2]

virtual void static_analysis_baset::initialize ( const goto_programt &  goto_program)
inlinevirtual

Definition at line 111 of file static_analysis.h.

◆ insert()

void static_analysis_baset::insert ( locationt  l)
inline

Definition at line 163 of file static_analysis.h.

◆ make_temporary_state()

virtual std::unique_ptr<statet> static_analysis_baset::make_temporary_state ( statet &  s)
protectedpure virtual

Implemented in static_analysist< T >, and static_analysist< VSDT >.

◆ merge()

virtual bool static_analysis_baset::merge ( statet &  a,
const statet &  b,
locationt  to 
)
protectedpure virtual

Implemented in static_analysist< T >, and static_analysist< VSDT >.

◆ merge_shared()

virtual bool static_analysis_baset::merge_shared ( statet &  a,
const statet &  b,
locationt  to 
)
protectedpure virtual

Implemented in concurrency_aware_static_analysist< T >, static_analysist< T >, and static_analysist< VSDT >.

◆ operator()() [1/2]

void static_analysis_baset::operator() ( const goto_functionst &  goto_functions)
virtual

Definition at line 50 of file static_analysis.cpp.

◆ operator()() [2/2]

void static_analysis_baset::operator() ( const irep_idt &  function_identifier,
const goto_programt &  goto_program 
)
virtual

Definition at line 57 of file static_analysis.cpp.

◆ output() [1/3]

void static_analysis_baset::output ( const goto_functionst &  goto_functions,
std::ostream &  out 
) const
virtual

Definition at line 66 of file static_analysis.cpp.

◆ output() [2/3]

void static_analysis_baset::output ( const goto_programt &  goto_program,
const irep_idt &  identifier,
std::ostream &  out 
) const
protectedvirtual

Definition at line 84 of file static_analysis.cpp.

◆ output() [3/3]

void static_analysis_baset::output ( const goto_programt &  goto_program,
std::ostream &  out 
) const
inline

Definition at line 154 of file static_analysis.h.

◆ put_in_working_set()

void static_analysis_baset::put_in_working_set ( working_sett &  working_set,
locationt  l 
)
inlineprotected

Definition at line 189 of file static_analysis.h.

◆ sequential_fixedpoint()

void static_analysis_baset::sequential_fixedpoint ( const goto_functionst &  goto_functions)
protected

Definition at line 429 of file static_analysis.cpp.

◆ successor()

static locationt static_analysis_baset::successor ( locationt  l)
inlinestaticprotected

Definition at line 219 of file static_analysis.h.

◆ update() [1/2]

void static_analysis_baset::update ( const goto_functionst &  goto_functions)
virtual

Definition at line 117 of file static_analysis.cpp.

◆ update() [2/2]

void static_analysis_baset::update ( const goto_programt &  goto_program)
virtual

Definition at line 124 of file static_analysis.cpp.

◆ visit()

bool static_analysis_baset::visit ( const irep_idt &  function_identifier,
locationt  l,
working_sett &  working_set,
const goto_programt &  goto_program,
const goto_functionst &  goto_functions 
)
protected

Definition at line 185 of file static_analysis.cpp.

Member Data Documentation

◆ functions_done

functions_donet static_analysis_baset::functions_done
protected

Definition at line 230 of file static_analysis.h.

◆ initialized

bool static_analysis_baset::initialized
protected

Definition at line 241 of file static_analysis.h.

◆ ns

const namespacet& static_analysis_baset::ns
protected

Definition at line 178 of file static_analysis.h.

◆ recursion_set

recursion_sett static_analysis_baset::recursion_set
protected

Definition at line 233 of file static_analysis.h.

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