ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
static_analysis_baset Class Referenceabstract

#include <static_analysis.h>

Inheritance diagram for static_analysis_baset:
[legend]

Public Types

typedef abstract_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 goto_programt &goto_program)
virtual void operator() (const goto_functionst &goto_functions)
virtual ~static_analysis_baset ()=default
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 (locationtlocationt l) const =0
void insert (locationtlocationt l)

Protected Types

typedef std::map< unsigned, locationtlocationt > working_sett
typedef std::set< irep_idt > functions_donet
typedef std::set< irep_idt > recursion_sett

Protected Member Functions

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)
virtual bool merge (statet &a, const statet &b, bool keepnew=false)=0
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)
virtual void generate_state (locationtlocationt l)=0
virtual statet & get_state (locationtlocationt l)=0
virtual const statet & get_state (locationtlocationt l) const =0
virtual statet * make_temporary_state (statet &s)=0
virtual void get_reference_set (locationtlocationt l, const expr2tc &expr, std::list< expr2tc > &dest)=0

Static Protected Member Functions

static locationtlocationt successor (locationtlocationt l)

Protected Attributes

const namespacet & ns
functions_donet functions_done
recursion_sett recursion_set
bool initialized

Member Typedef Documentation

◆ functions_donet

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

◆ locationt

typedef goto_programt::const_targett static_analysis_baset::locationt

◆ recursion_sett

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

◆ statet

typedef abstract_domain_baset static_analysis_baset::statet

◆ working_sett

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

Constructor & Destructor Documentation

◆ static_analysis_baset()

static_analysis_baset::static_analysis_baset ( const namespacet & _ns)
inline

◆ ~static_analysis_baset()

virtual static_analysis_baset::~static_analysis_baset ( )
virtualdefault

Member Function Documentation

◆ clear()

virtual void static_analysis_baset::clear ( )
inlinevirtual

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

◆ do_function_call()

void static_analysis_baset::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

◆ do_function_call_rec()

void static_analysis_baset::do_function_call_rec ( locationtlocationt l_call,
const expr2tc & function,
const std::vector< expr2tc > & arguments,
statet & new_state,
const goto_functionst & goto_functions )
protected

◆ fixedpoint() [1/3]

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

◆ fixedpoint() [2/3]

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

◆ fixedpoint() [3/3]

bool static_analysis_baset::fixedpoint ( goto_functionst::function_mapt::const_iterator it,
const goto_functionst & goto_functions )
protected

◆ generate_state()

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

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

◆ generate_states() [1/2]

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

◆ generate_states() [2/2]

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

◆ get_next()

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

◆ get_reference_set()

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

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

◆ get_state() [1/2]

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

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

◆ get_state() [2/2]

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

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

◆ has_location()

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

Implemented in static_analysist< T >, static_analysist< value_set_domaint >, and value_set_analysist.

◆ initialize() [1/2]

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

Reimplemented in value_set_analysist.

◆ initialize() [2/2]

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

Reimplemented in value_set_analysist.

◆ insert()

void static_analysis_baset::insert ( locationtlocationt l)
inline

◆ make_temporary_state()

virtual statet * static_analysis_baset::make_temporary_state ( statet & s)
protectedpure virtual

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

◆ merge()

virtual bool static_analysis_baset::merge ( statet & a,
const statet & b,
bool keepnew = false )
protectedpure virtual

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

◆ operator()() [1/2]

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

◆ operator()() [2/2]

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

◆ output() [1/3]

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

◆ output() [2/3]

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

◆ output() [3/3]

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

◆ put_in_working_set()

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

◆ successor()

locationtlocationt static_analysis_baset::successor ( locationtlocationt l)
inlinestaticprotected

◆ update() [1/2]

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

◆ update() [2/2]

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

◆ visit()

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

Member Data Documentation

◆ functions_done

functions_donet static_analysis_baset::functions_done
protected

◆ initialized

bool static_analysis_baset::initialized
protected

◆ ns

const namespacet& static_analysis_baset::ns
protected

◆ recursion_set

recursion_sett static_analysis_baset::recursion_set
protected
The documentation for this class was generated from the following files: