cprover
value_set_analysis_templatet< VSDT > Class Template Reference

This template class implements a data-flow analysis which keeps track of what values different variables might have at different points in the program. More...

#include <value_set_analysis.h>

+ Inheritance diagram for value_set_analysis_templatet< VSDT >:
+ Collaboration diagram for value_set_analysis_templatet< VSDT >:

Public Types

typedef VSDT domaint
 
typedef static_analysist< domaintbaset
 
typedef baset::locationt locationt
 
- Public Types inherited from value_setst
typedef std::list< exprtvaluest
 
- Public Types inherited from static_analysist< VSDT >
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_analysis_templatet (const namespacet &ns)
 
const value_settget_value_set (goto_programt::const_targett t)
 
void convert (const goto_programt &goto_program, xmlt &dest) const
 
void get_values (const irep_idt &, locationt l, const exprt &expr, value_setst::valuest &dest) override
 
- Public Member Functions inherited from value_setst
 value_setst ()
 
virtual ~value_setst ()
 
- Public Member Functions inherited from static_analysist< VSDT >
 static_analysist (const namespacet &_ns)
 
VSDT & operator[] (locationt l)
 
const VSDT & operator[] (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 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 irep_idt &function_identifier, 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< VSDT >
typedef std::map< locationt, VSDT > state_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< VSDT >
virtual statetget_state (locationt l)
 
virtual const statetget_state (locationt l) const
 
virtual bool merge (statet &a, const statet &b, locationt to)
 
virtual std::unique_ptr< 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 irep_idt &function_identifier, 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 (const irep_idt &function_identifier, 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 (const irep_idt &calling_function, 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 (const irep_idt &calling_function, 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< VSDT >
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

template<class VSDT>
class value_set_analysis_templatet< VSDT >

This template class implements a data-flow analysis which keeps track of what values different variables might have at different points in the program.

It is used through the alias value_set_analysist, so VSDT is value_set_domain_templatet<value_sett>.

Note: it is currently based on static_analysist, which is obsolete. It should be moved onto ait.

Definition at line 37 of file value_set_analysis.h.

Member Typedef Documentation

◆ baset

template<class VSDT >
typedef static_analysist<domaint> value_set_analysis_templatet< VSDT >::baset

Definition at line 43 of file value_set_analysis.h.

◆ domaint

template<class VSDT >
typedef VSDT value_set_analysis_templatet< VSDT >::domaint

Definition at line 42 of file value_set_analysis.h.

◆ locationt

template<class VSDT >
typedef baset::locationt value_set_analysis_templatet< VSDT >::locationt

Definition at line 44 of file value_set_analysis.h.

Constructor & Destructor Documentation

◆ value_set_analysis_templatet()

template<class VSDT >
value_set_analysis_templatet< VSDT >::value_set_analysis_templatet ( const namespacet ns)
inlineexplicit

Definition at line 46 of file value_set_analysis.h.

Member Function Documentation

◆ convert()

template<class VSDT >
void value_set_analysis_templatet< VSDT >::convert ( const goto_programt goto_program,
xmlt dest 
) const
inline

Definition at line 55 of file value_set_analysis.h.

◆ get_value_set()

template<class VSDT >
const value_sett& value_set_analysis_templatet< VSDT >::get_value_set ( goto_programt::const_targett  t)
inline

Definition at line 50 of file value_set_analysis.h.

◆ get_values()

template<class VSDT >
void value_set_analysis_templatet< VSDT >::get_values ( const irep_idt ,
locationt  l,
const exprt expr,
value_setst::valuest dest 
)
inlineoverridevirtual

Implements value_setst.

Definition at line 68 of file value_set_analysis.h.


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