cprover
flow_insensitive_analysis_baset Class Referenceabstract

#include <flow_insensitive_analysis.h>

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

Public Types

typedef flow_insensitive_abstract_domain_baset statet
 
typedef goto_programt::const_targett locationt
 

Public Member Functions

bool seen (const locationt &l)
 
 flow_insensitive_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 ~flow_insensitive_analysis_baset ()
 
virtual void clear ()
 
virtual void output (const goto_functionst &goto_functions, std::ostream &out)
 
virtual void output (const goto_programt &goto_program, std::ostream &out)
 

Public Attributes

std::set< locationtseen_locations
 
std::map< locationt, unsigned > statistics
 

Protected Types

typedef std::priority_queue< locationtworking_sett
 
typedef std::set< irep_idtfunctions_donet
 
typedef std::set< irep_idtrecursion_sett
 
typedef flow_insensitive_abstract_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)
 
bool fixedpoint (goto_functionst::function_mapt::const_iterator it, const goto_functionst &goto_functions)
 
void fixedpoint (const goto_functionst &goto_functions)
 
bool visit (locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
 
bool do_function_call_rec (locationt l_call, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
 
bool do_function_call (locationt l_call, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, statet &new_state)
 
virtual statetget_state ()=0
 
virtual const statetget_state () const =0
 
virtual void get_reference_set (const exprt &expr, expr_sett &expr_set)=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 77 of file flow_insensitive_analysis.h.

Member Typedef Documentation

◆ expr_sett

◆ functions_donet

Definition at line 190 of file flow_insensitive_analysis.h.

◆ locationt

◆ recursion_sett

Definition at line 193 of file flow_insensitive_analysis.h.

◆ statet

◆ working_sett

typedef std::priority_queue<locationt> flow_insensitive_analysis_baset::working_sett
protected

Definition at line 154 of file flow_insensitive_analysis.h.

Constructor & Destructor Documentation

◆ flow_insensitive_analysis_baset()

flow_insensitive_analysis_baset::flow_insensitive_analysis_baset ( const namespacet _ns)
inlineexplicit

Definition at line 92 of file flow_insensitive_analysis.h.

◆ ~flow_insensitive_analysis_baset()

virtual flow_insensitive_analysis_baset::~flow_insensitive_analysis_baset ( )
inlinevirtual

Definition at line 126 of file flow_insensitive_analysis.h.

Member Function Documentation

◆ clear()

◆ do_function_call()

bool flow_insensitive_analysis_baset::do_function_call ( locationt  l_call,
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()

bool flow_insensitive_analysis_baset::do_function_call_rec ( locationt  l_call,
const exprt function,
const exprt::operandst arguments,
statet new_state,
const goto_functionst goto_functions 
)
protected

◆ fixedpoint() [1/3]

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

◆ fixedpoint() [2/3]

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

Definition at line 407 of file flow_insensitive_analysis.cpp.

References fixedpoint(), and functions_done.

◆ fixedpoint() [3/3]

void flow_insensitive_analysis_baset::fixedpoint ( const goto_functionst goto_functions)
protected

◆ get_next()

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

Definition at line 94 of file flow_insensitive_analysis.cpp.

Referenced by fixedpoint().

◆ get_reference_set()

virtual void flow_insensitive_analysis_baset::get_reference_set ( const exprt expr,
expr_sett expr_set 
)
protectedpure virtual

◆ get_state() [1/2]

◆ get_state() [2/2]

◆ initialize() [1/2]

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

◆ initialize() [2/2]

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

◆ operator()() [1/2]

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

Definition at line 65 of file flow_insensitive_analysis.cpp.

References fixedpoint(), goto_program, and initialize().

◆ operator()() [2/2]

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

Definition at line 58 of file flow_insensitive_analysis.cpp.

References fixedpoint(), and initialize().

◆ output() [1/3]

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

Definition at line 73 of file flow_insensitive_analysis.cpp.

References forall_goto_functions.

Referenced by output().

◆ output() [2/3]

virtual void flow_insensitive_analysis_baset::output ( const goto_programt goto_program,
std::ostream &  out 
)
inlinevirtual

Reimplemented in value_set_analysis_fivrnst, and value_set_analysis_fivrt.

Definition at line 139 of file flow_insensitive_analysis.h.

References goto_program, and output().

◆ output() [3/3]

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

◆ put_in_working_set()

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

Definition at line 158 of file flow_insensitive_analysis.h.

Referenced by fixedpoint(), and visit().

◆ seen()

bool flow_insensitive_analysis_baset::seen ( const locationt l)
inline

Definition at line 87 of file flow_insensitive_analysis.h.

References seen_locations.

Referenced by visit().

◆ successor()

static locationt flow_insensitive_analysis_baset::successor ( locationt  l)
inlinestaticprotected

Definition at line 184 of file flow_insensitive_analysis.h.

◆ update() [1/2]

void flow_insensitive_analysis_baset::update ( const goto_programt goto_program)
virtual

Definition at line 421 of file flow_insensitive_analysis.cpp.

◆ update() [2/2]

void flow_insensitive_analysis_baset::update ( const goto_functionst goto_functions)
virtual

Definition at line 415 of file flow_insensitive_analysis.cpp.

◆ visit()

Member Data Documentation

◆ functions_done

functions_donet flow_insensitive_analysis_baset::functions_done
protected

Definition at line 191 of file flow_insensitive_analysis.h.

Referenced by do_function_call(), and fixedpoint().

◆ initialized

bool flow_insensitive_analysis_baset::initialized
protected

Definition at line 196 of file flow_insensitive_analysis.h.

Referenced by clear(), and initialize().

◆ ns

◆ recursion_set

recursion_sett flow_insensitive_analysis_baset::recursion_set
protected

Definition at line 194 of file flow_insensitive_analysis.h.

Referenced by do_function_call_rec().

◆ seen_locations

std::set<locationt> flow_insensitive_analysis_baset::seen_locations

Definition at line 83 of file flow_insensitive_analysis.h.

Referenced by seen(), and visit().

◆ statistics

std::map<locationt, unsigned> flow_insensitive_analysis_baset::statistics

Definition at line 85 of file flow_insensitive_analysis.h.

Referenced by visit().


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