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 ait< domaint > | baset |
| typedef baset::locationt | locationt |
| Public Types inherited from value_setst | |
| typedef std::list< exprt > | valuest |
| Public Types inherited from ait< VSDT > | |
| typedef goto_programt::const_targett | locationt |
| Public Types inherited from ai_baset | |
| typedef ai_domain_baset | statet |
| typedef ai_storage_baset::cstate_ptrt | cstate_ptrt |
| typedef ai_history_baset::trace_ptrt | trace_ptrt |
| typedef ai_history_baset::trace_sett | trace_sett |
| typedef ai_storage_baset::ctrace_set_ptrt | ctrace_set_ptrt |
| typedef goto_programt::const_targett | locationt |
Public Member Functions | |
| value_set_analysis_templatet (const namespacet &_ns) | |
| std::vector< exprt > | get_values (const irep_idt &, locationt l, const exprt &expr) override |
| Public Member Functions inherited from value_setst | |
| value_setst () | |
| virtual | ~value_setst () |
| Public Member Functions inherited from ait< VSDT > | |
| ait () | |
| ait (std::unique_ptr< ai_domain_factory_baset > &&df) | |
| const VSDT & | operator[] (locationt l) const |
| Find the analysis result for a given location. More... | |
| Public Member Functions inherited from ai_recursive_interproceduralt | |
| ai_recursive_interproceduralt (std::unique_ptr< ai_history_factory_baset > &&hf, std::unique_ptr< ai_domain_factory_baset > &&df, std::unique_ptr< ai_storage_baset > &&st, message_handlert &mh) | |
| Public Member Functions inherited from ai_baset | |
| ai_baset (std::unique_ptr< ai_history_factory_baset > &&hf, std::unique_ptr< ai_domain_factory_baset > &&df, std::unique_ptr< ai_storage_baset > &&st, message_handlert &mh) | |
| virtual | ~ai_baset () |
| void | operator() (const irep_idt &function_id, const goto_programt &goto_program, const namespacet &ns) |
| Run abstract interpretation on a single function. More... | |
| void | operator() (const goto_functionst &goto_functions, const namespacet &ns) |
| Run abstract interpretation on a whole program. More... | |
| void | operator() (const abstract_goto_modelt &goto_model) |
| Run abstract interpretation on a whole program. More... | |
| void | operator() (const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function, const namespacet &ns) |
| Run abstract interpretation on a single function. More... | |
| virtual ctrace_set_ptrt | abstract_traces_before (locationt l) const |
| Returns all of the histories that have reached the start of the instruction. More... | |
| virtual ctrace_set_ptrt | abstract_traces_after (locationt l) const |
| Returns all of the histories that have reached the end of the instruction. More... | |
| virtual cstate_ptrt | abstract_state_before (locationt l) const |
| Get a copy of the abstract state before the given instruction, without needing to know what kind of domain or history is used. More... | |
| virtual cstate_ptrt | abstract_state_after (locationt l) const |
| Get a copy of the abstract state after the given instruction, without needing to know what kind of domain or history is used. More... | |
| virtual cstate_ptrt | abstract_state_before (const trace_ptrt &p) const |
| The same interfaces but with histories. More... | |
| virtual cstate_ptrt | abstract_state_after (const trace_ptrt &p) const |
| virtual void | clear () |
| Reset the abstract state. More... | |
| virtual void | output (const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const |
| Output the abstract states for a single function. More... | |
| virtual jsont | output_json (const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const |
| Output the abstract states for a single function as JSON. More... | |
| virtual xmlt | output_xml (const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const |
| Output the abstract states for a single function as XML. More... | |
| virtual void | output (const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const |
| Output the abstract states for a whole program. More... | |
| void | output (const goto_modelt &goto_model, std::ostream &out) const |
| Output the abstract states for a whole program. More... | |
| void | output (const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const |
| Output the abstract states for a function. More... | |
| virtual jsont | output_json (const namespacet &ns, const goto_functionst &goto_functions) const |
| Output the abstract states for the whole program as JSON. More... | |
| jsont | output_json (const goto_modelt &goto_model) const |
| Output the abstract states for a whole program as JSON. More... | |
| jsont | output_json (const namespacet &ns, const goto_programt &goto_program) const |
| Output the abstract states for a single function as JSON. More... | |
| jsont | output_json (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const |
| Output the abstract states for a single function as JSON. More... | |
| virtual xmlt | output_xml (const namespacet &ns, const goto_functionst &goto_functions) const |
| Output the abstract states for the whole program as XML. More... | |
| xmlt | output_xml (const goto_modelt &goto_model) const |
| Output the abstract states for the whole program as XML. More... | |
| xmlt | output_xml (const namespacet &ns, const goto_programt &goto_program) const |
| Output the abstract states for a single function as XML. More... | |
| xmlt | output_xml (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const |
| Output the abstract states for a single function as XML. More... | |
Private Attributes | |
| const namespacet & | ns |
Additional Inherited Members | |
| Protected Types inherited from ai_baset | |
| typedef trace_sett | working_sett |
| The work queue, sorted using the history's ordering operator. More... | |
| Protected Member Functions inherited from ait< VSDT > | |
| virtual statet & | get_state (locationt l) |
| virtual statet & | get_state (trace_ptrt p) |
| Get the state for the given history, creating it with the factory if it doesn't exist. More... | |
| Protected Member Functions inherited from ai_recursive_interproceduralt | |
| bool | visit_edge_function_call (const irep_idt &calling_function_id, trace_ptrt p_call, locationt l_return, const irep_idt &callee_function_id, working_sett &working_set, const goto_programt &callee, const goto_functionst &goto_functions, const namespacet &ns) override |
| Protected Member Functions inherited from ai_baset | |
| virtual void | initialize (const irep_idt &function_id, const goto_programt &goto_program) |
| Initialize all the abstract states for a single function. More... | |
| virtual void | initialize (const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function) |
| Initialize all the abstract states for a single function. More... | |
| virtual void | initialize (const goto_functionst &goto_functions) |
| Initialize all the abstract states for a whole program. More... | |
| virtual void | finalize () |
| Override this to add a cleanup or post-processing step after fixedpoint has run. More... | |
| trace_ptrt | entry_state (const goto_programt &goto_program) |
| Set the abstract state of the entry location of a single function to the entry state required by the analysis. More... | |
| trace_ptrt | entry_state (const goto_functionst &goto_functions) |
| Set the abstract state of the entry location of a whole program to the entry state required by the analysis. More... | |
| trace_ptrt | get_next (working_sett &working_set) |
| Get the next location from the work queue. More... | |
| void | put_in_working_set (working_sett &working_set, trace_ptrt t) |
| virtual bool | fixedpoint (trace_ptrt starting_trace, const irep_idt &function_id, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
| Run the fixedpoint algorithm until it reaches a fixed point. More... | |
| virtual void | fixedpoint (trace_ptrt starting_trace, const goto_functionst &goto_functions, const namespacet &ns) |
| virtual bool | visit (const irep_idt &function_id, trace_ptrt p, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
| Perform one step of abstract interpretation from trace t Depending on the instruction type it may compute a number of "edges" or applications of the abstract transformer. More... | |
| virtual bool | visit_function_call (const irep_idt &function_id, trace_ptrt p_call, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
| virtual bool | visit_end_function (const irep_idt &function_id, trace_ptrt p, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
| bool | visit_edge (const irep_idt &function_id, trace_ptrt p, const irep_idt &to_function_id, locationt to_l, trace_ptrt caller_history, const namespacet &ns, working_sett &working_set) |
| virtual bool | merge (const statet &src, trace_ptrt from, trace_ptrt to) |
Merge the state src, flowing from tracet from to tracet to, into the state currently stored for tracet to. More... | |
| virtual std::unique_ptr< statet > | make_temporary_state (const statet &s) |
| Make a copy of a state. More... | |
| virtual statet & | get_state (trace_ptrt p) |
| Get the state for the given history, creating it with the factory if it doesn't exist. More... | |
| Protected Attributes inherited from ai_baset | |
| std::unique_ptr< ai_history_factory_baset > | history_factory |
| For creating history objects. More... | |
| std::unique_ptr< ai_domain_factory_baset > | domain_factory |
| For creating domain objects. More... | |
| std::unique_ptr< ai_storage_baset > | storage |
| message_handlert & | message_handler |
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>.
Definition at line 25 of file value_set_analysis.h.
Member Typedef Documentation
◆ baset
template<class VSDT >
| typedef ait<domaint> value_set_analysis_templatet< VSDT >::baset |
Definition at line 32 of file value_set_analysis.h.
◆ domaint
template<class VSDT >
| typedef VSDT value_set_analysis_templatet< VSDT >::domaint |
Definition at line 31 of file value_set_analysis.h.
◆ locationt
template<class VSDT >
| typedef baset::locationt value_set_analysis_templatet< VSDT >::locationt |
Definition at line 33 of file value_set_analysis.h.
Constructor & Destructor Documentation
◆ value_set_analysis_templatet()
template<class VSDT >
|
inlineexplicit |
Definition at line 35 of file value_set_analysis.h.
Member Function Documentation
◆ get_values()
template<class VSDT >
|
inlineoverridevirtual |
Implements value_setst.
Definition at line 43 of file value_set_analysis.h.
Member Data Documentation
◆ ns
template<class VSDT >
|
private |
Definition at line 28 of file value_set_analysis.h.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/pointer-analysis/value_set_analysis.h
