ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
static_analysist< T > Class Template Reference

#include <static_analysis.h>

Inheritance diagram for static_analysist< T >:
[legend]

Public Types

typedef goto_programt::const_targett locationt
Public Types inherited from static_analysis_baset
typedef abstract_domain_baset statet
typedef goto_programt::const_targett locationt

Public Member Functions

 static_analysist (const namespacet &_ns)
T & operator[] (locationtlocationt l)
const T & operator[] (locationtlocationt l) const
void clear () override
bool has_location (locationtlocationt l) const override
Public Member Functions inherited from static_analysis_baset
 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 goto_programt &goto_program)
virtual void operator() (const goto_functionst &goto_functions)
virtual ~static_analysis_baset ()=default
virtual void output (const goto_functionst &goto_functions, std::ostream &out) const
void output (const goto_programt &goto_program, std::ostream &out) const
void insert (locationtlocationt l)

Protected Types

typedef std::map< locationtlocationt, T > state_mapt
Protected Types inherited from static_analysis_baset
typedef std::map< unsigned, locationtlocationt > working_sett
typedef std::set< irep_idt > functions_donet
typedef std::set< irep_idt > recursion_sett

Protected Member Functions

statet & get_state (locationtlocationt l) override
const statet & get_state (locationtlocationt l) const override
bool merge (statet &a, const statet &b, bool keepnew=false) override
statet * make_temporary_state (statet &s) override
void generate_state (locationtlocationt l) override
void get_reference_set (locationtlocationt l, const expr2tc &expr, std::list< expr2tc > &dest) override
Protected Member Functions inherited from static_analysis_baset
virtual void output (const goto_programt &goto_program, const irep_idt &identifier, std::ostream &out) const
locationtlocationt get_next (working_sett &working_set)
void put_in_working_set (working_sett &working_set, locationtlocationt l)
bool fixedpoint (const goto_programt &goto_program, const goto_functionst &goto_functions)
bool fixedpoint (goto_functionst::function_mapt::const_iterator it, const goto_functionst &goto_functions)
void fixedpoint (const goto_functionst &goto_functions)
bool visit (locationtlocationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
void generate_states (const goto_functionst &goto_functions)
void generate_states (const goto_programt &goto_program)
void do_function_call_rec (locationtlocationt l_call, const expr2tc &function, const std::vector< expr2tc > &arguments, statet &new_state, const goto_functionst &goto_functions)
void do_function_call (locationtlocationt l_call, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const std::vector< expr2tc > &arguments, statet &new_state)

Protected Attributes

state_mapt state_map
Protected Attributes inherited from static_analysis_baset
const namespacet & ns
functions_donet functions_done
recursion_sett recursion_set
bool initialized

Additional Inherited Members

Static Protected Member Functions inherited from static_analysis_baset
static locationtlocationt successor (locationtlocationt l)

Member Typedef Documentation

◆ locationt

template<typename T>
typedef goto_programt::const_targett static_analysist< T >::locationt

◆ state_mapt

template<typename T>
typedef std::map<locationtlocationt, T> static_analysist< T >::state_mapt
protected

Constructor & Destructor Documentation

◆ static_analysist()

template<typename T>
static_analysist< T >::static_analysist ( const namespacet & _ns)
inline

Member Function Documentation

◆ clear()

template<typename T>
void static_analysist< T >::clear ( )
inlineoverridevirtual

Reimplemented from static_analysis_baset.

◆ generate_state()

template<typename T>
void static_analysist< T >::generate_state ( locationtlocationt l)
inlineoverrideprotectedvirtual

Implements static_analysis_baset.

◆ get_reference_set()

template<typename T>
void static_analysist< T >::get_reference_set ( locationtlocationt l,
const expr2tc & expr,
std::list< expr2tc > & dest )
inlineoverrideprotectedvirtual

Implements static_analysis_baset.

◆ get_state() [1/2]

template<typename T>
const statet & static_analysist< T >::get_state ( locationtlocationt l) const
inlineoverrideprotectedvirtual

Implements static_analysis_baset.

◆ get_state() [2/2]

template<typename T>
statet & static_analysist< T >::get_state ( locationtlocationt l)
inlineoverrideprotectedvirtual

Implements static_analysis_baset.

◆ has_location()

template<typename T>
bool static_analysist< T >::has_location ( locationtlocationt l) const
inlineoverridevirtual

Implements static_analysis_baset.

Reimplemented in value_set_analysist.

◆ make_temporary_state()

template<typename T>
statet * static_analysist< T >::make_temporary_state ( statet & s)
inlineoverrideprotectedvirtual

Implements static_analysis_baset.

◆ merge()

template<typename T>
bool static_analysist< T >::merge ( statet & a,
const statet & b,
bool keepnew = false )
inlineoverrideprotectedvirtual

Implements static_analysis_baset.

◆ operator[]() [1/2]

template<typename T>
T & static_analysist< T >::operator[] ( locationtlocationt l)
inline

◆ operator[]() [2/2]

template<typename T>
const T & static_analysist< T >::operator[] ( locationtlocationt l) const
inline

Member Data Documentation

◆ state_map

template<typename T>
state_mapt static_analysist< T >::state_map
protected
The documentation for this class was generated from the following file: