cprover
static_analysis_baset Class Referenceabstract

#include <static_analysis.h>

Inheritance diagram for static_analysis_baset:
[legend]
Collaboration diagram for static_analysis_baset:
[legend]

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 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, locationtworking_sett
 
typedef std::set< irep_idtfunctions_donet
 
typedef std::set< irep_idtrecursion_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 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 (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 (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 (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 statetget_state (locationt l)=0
 
virtual const statetget_state (locationt l) const =0
 
virtual statetmake_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 namespacetns
 
functions_donet functions_done
 
recursion_sett recursion_set
 
bool initialized
 

Detailed Description

Definition at line 94 of file static_analysis.h.

Member Typedef Documentation

§ expr_sett

Definition at line 257 of file static_analysis.h.

§ functions_donet

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

Definition at line 221 of file static_analysis.h.

§ locationt

§ recursion_sett

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

Definition at line 224 of file static_analysis.h.

§ statet

Definition at line 97 of file static_analysis.h.

§ working_sett

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

Definition at line 179 of file static_analysis.h.

Constructor & Destructor Documentation

§ static_analysis_baset()

static_analysis_baset::static_analysis_baset ( const namespacet _ns)
inlineexplicit

Definition at line 100 of file static_analysis.h.

§ ~static_analysis_baset()

virtual static_analysis_baset::~static_analysis_baset ( )
inlinevirtual

Definition at line 135 of file static_analysis.h.

Member Function Documentation

§ clear()

virtual void static_analysis_baset::clear ( void  )
inlinevirtual

§ concurrent_fixedpoint()

§ do_function_call()

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

§ do_function_call_rec()

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

§ fixedpoint() [1/2]

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

§ fixedpoint() [2/2]

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

§ generate_state()

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

§ generate_states() [1/2]

void static_analysis_baset::generate_states ( const goto_functionst goto_functions)
protected

Definition at line 113 of file static_analysis.cpp.

References forall_goto_functions.

§ generate_states() [2/2]

void static_analysis_baset::generate_states ( const goto_programt goto_program)
protected

Definition at line 120 of file static_analysis.cpp.

References forall_goto_program_instructions, and generate_state().

§ get_guard()

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

Definition at line 23 of file static_analysis.cpp.

References exprt::make_not().

§ get_next()

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

Definition at line 156 of file static_analysis.cpp.

Referenced by concurrent_fixedpoint(), and fixedpoint().

§ get_reference_set()

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

§ get_return_lhs()

exprt static_analysis_baset::get_return_lhs ( locationt  to)
static

Definition at line 43 of file static_analysis.cpp.

References get_nil_irep(), and to_code_function_call().

Referenced by value_set_domaint::transform().

§ get_state() [1/2]

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

§ get_state() [2/2]

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

§ has_location()

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

§ initialize() [1/2]

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

Reimplemented in value_set_analysist.

Definition at line 106 of file static_analysis.h.

Referenced by value_set_analysist::initialize(), and operator()().

§ initialize() [2/2]

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

Reimplemented in value_set_analysist.

Definition at line 116 of file static_analysis.h.

§ insert()

void static_analysis_baset::insert ( locationt  l)
inline

Definition at line 157 of file static_analysis.h.

§ make_temporary_state()

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

§ merge()

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

§ merge_shared()

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

§ operator()() [1/2]

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

Definition at line 68 of file static_analysis.cpp.

References fixedpoint(), and initialize().

§ operator()() [2/2]

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

Definition at line 61 of file static_analysis.cpp.

References fixedpoint(), and initialize().

§ output() [1/3]

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

Definition at line 76 of file static_analysis.cpp.

References forall_goto_functions.

Referenced by show_value_sets().

§ output() [2/3]

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

Definition at line 148 of file static_analysis.h.

References domain_baset::output().

§ output() [3/3]

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

§ put_in_working_set()

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

Definition at line 183 of file static_analysis.h.

Referenced by concurrent_fixedpoint(), fixedpoint(), and visit().

§ sequential_fixedpoint()

void static_analysis_baset::sequential_fixedpoint ( const goto_functionst goto_functions)
protected

Definition at line 420 of file static_analysis.cpp.

References fixedpoint(), forall_goto_functions, and functions_done.

Referenced by concurrent_fixedpoint().

§ successor()

static locationt static_analysis_baset::successor ( locationt  l)
inlinestaticprotected

Definition at line 211 of file static_analysis.h.

§ update() [1/2]

void static_analysis_baset::update ( const goto_programt goto_program)
virtual

§ update() [2/2]

void static_analysis_baset::update ( const goto_functionst goto_functions)
virtual

Definition at line 127 of file static_analysis.cpp.

References forall_goto_functions, and update().

§ visit()

Member Data Documentation

§ functions_done

functions_donet static_analysis_baset::functions_done
protected

Definition at line 222 of file static_analysis.h.

Referenced by do_function_call(), and sequential_fixedpoint().

§ initialized

bool static_analysis_baset::initialized
protected

Definition at line 233 of file static_analysis.h.

§ ns

§ recursion_set

recursion_sett static_analysis_baset::recursion_set
protected

Definition at line 225 of file static_analysis.h.

Referenced by do_function_call_rec().


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