cprover
value_set_analysist Class Reference

#include <value_set_analysis.h>

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

Public Types

typedef static_analysist< value_set_domaintbaset
 
- Public Types inherited from value_setst
typedef std::list< exprtvaluest
 
- Public Types inherited from static_analysist< value_set_domaint >
typedef goto_programt::const_targett locationt
 
- Public Types inherited from static_analysis_baset
typedef domain_baset statet
 
typedef goto_programt::const_targett locationt
 

Public Member Functions

 value_set_analysist (const namespacet &_ns)
 
virtual void initialize (const goto_programt &goto_program)
 
virtual void initialize (const goto_functionst &goto_functions)
 
void convert (const goto_programt &goto_program, const irep_idt &identifier, xmlt &dest) const
 
virtual void get_values (locationt l, const exprt &expr, value_setst::valuest &dest)
 
- Public Member Functions inherited from value_setst
 value_setst ()
 
virtual ~value_setst ()
 
- Public Member Functions inherited from static_analysist< value_set_domaint >
 static_analysist (const namespacet &_ns)
 
value_set_domaintoperator[] (locationt l)
 
const value_set_domaintoperator[] (locationt l) const
 
virtual void clear ()
 
virtual bool has_location (locationt l) const
 
- Public Member Functions inherited from static_analysis_baset
 static_analysis_baset (const namespacet &_ns)
 
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 output (const goto_functionst &goto_functions, std::ostream &out) const
 
void output (const goto_programt &goto_program, std::ostream &out) const
 
void insert (locationt l)
 

Additional Inherited Members

- Static Public Member Functions inherited from static_analysis_baset
static exprt get_guard (locationt from, locationt to)
 
static exprt get_return_lhs (locationt to)
 
- Protected Types inherited from static_analysist< value_set_domaint >
typedef std::map< locationt, value_set_domaintstate_mapt
 
- Protected Types inherited from static_analysis_baset
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 inherited from static_analysist< value_set_domaint >
virtual statetget_state (locationt l)
 
virtual const statetget_state (locationt l) const
 
virtual bool merge (statet &a, const statet &b, locationt to)
 
virtual statetmake_temporary_state (statet &s)
 
virtual void generate_state (locationt l)
 
virtual void get_reference_set (locationt l, const exprt &expr, std::list< exprt > &dest)
 
virtual void fixedpoint (const goto_functionst &goto_functions)
 
- Protected Member Functions inherited from static_analysis_baset
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)
 
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)
 
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)
 
- Static Protected Member Functions inherited from static_analysis_baset
static locationt successor (locationt l)
 
- Protected Attributes inherited from static_analysist< value_set_domaint >
state_mapt state_map
 
- Protected Attributes inherited from static_analysis_baset
const namespacetns
 
functions_donet functions_done
 
recursion_sett recursion_set
 
bool initialized
 

Detailed Description

Definition at line 23 of file value_set_analysis.h.

Member Typedef Documentation

◆ baset

Constructor & Destructor Documentation

◆ value_set_analysist()

value_set_analysist::value_set_analysist ( const namespacet _ns)
inlineexplicit

Definition at line 28 of file value_set_analysis.h.

Member Function Documentation

◆ convert()

void value_set_analysist::convert ( const goto_programt goto_program,
const irep_idt identifier,
xmlt dest 
) const

◆ get_values()

virtual void value_set_analysist::get_values ( locationt  l,
const exprt expr,
value_setst::valuest dest 
)
inlinevirtual

Implements value_setst.

Definition at line 46 of file value_set_analysis.h.

References static_analysis_baset::ns.

◆ initialize() [1/2]

void value_set_analysist::initialize ( const goto_programt goto_program)
virtual

Reimplemented from static_analysis_baset.

Definition at line 21 of file value_set_analysis.cpp.

References static_analysis_baset::initialize().

◆ initialize() [2/2]

void value_set_analysist::initialize ( const goto_functionst goto_functions)
virtual

Reimplemented from static_analysis_baset.

Definition at line 27 of file value_set_analysis.cpp.

References static_analysis_baset::initialize().


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