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.

Referenced by initialize().

◆ 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.

References generate_states(), and initialized.

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.

References generate_states(), and initialized.

◆ insert()

void static_analysis_baset::insert ( locationt  l)
inline

Definition at line 157 of file static_analysis.h.

References generate_state().

◆ 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 output(), and 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 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

◆ 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.

Referenced by clear(), and initialize().

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