cprover
Loading...
Searching...
No Matches
value_set_analysis.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Value Set Propagation
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "value_set_analysis.h"
13
14#include <util/xml_irep.h>
15
17 const std::function<const value_sett &(goto_programt::const_targett)>
18 &get_value_set,
19 const goto_programt &goto_program,
20 xmlt &dest)
21{
22 source_locationt previous_location;
23
24 forall_goto_program_instructions(i_it, goto_program)
25 {
26 const source_locationt &location = i_it->source_location();
27
28 if(location==previous_location)
29 continue;
30
31 if(location.is_nil() || location.get_file().empty())
32 continue;
33
34 // find value set
35 const value_sett &value_set=get_value_set(i_it);
36
37 xmlt &i=dest.new_element("instruction");
38 i.new_element()=::xml(location);
39
41 value_set.values.get_view(view);
42
43 for(const auto &values_entry : view)
44 {
45 xmlt &var=i.new_element("variable");
46 var.new_element("identifier").data = id2string(values_entry.first);
47
48#if 0
49 const value_sett::expr_sett &expr_set=
50 v_it->second.expr_set();
51
52 for(value_sett::expr_sett::const_iterator
53 e_it=expr_set.begin();
54 e_it!=expr_set.end();
55 e_it++)
56 {
57 std::string value_str=
58 from_expr(ns, identifier, *e_it);
59
60 var.new_element("value").data=
61 xmlt::escape(value_str);
62 }
63#endif
64 }
65 }
66}
67
69 const goto_functionst &goto_functions,
70 const value_set_analysist &value_set_analysis,
71 xmlt &dest)
72{
73 dest=xmlt("value_set_analysis");
74
75 for(goto_functionst::function_mapt::const_iterator
76 f_it=goto_functions.function_map.begin();
77 f_it!=goto_functions.function_map.end();
78 f_it++)
79 {
80 xmlt &f=dest.new_element("function");
81 f.new_element("identifier").data=id2string(f_it->first);
82 value_set_analysis.convert(f_it->second.body, f);
83 }
84}
85
87 const goto_programt &goto_program,
88 const value_set_analysist &value_set_analysis,
89 xmlt &dest)
90{
91 dest=xmlt("value_set_analysis");
92
93 value_set_analysis.convert(
94 goto_program,
95 dest.new_element("program"));
96}
bool empty() const
Definition dstring.h:88
A collection of goto functions.
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
bool is_nil() const
Definition irep.h:376
std::vector< view_itemt > viewt
View of the key-value pairs in the map.
void get_view(V &view) const
Get a view of the elements in the map A view is a list of pairs with the components being const refer...
const irep_idt & get_file() const
This template class implements a data-flow analysis which keeps track of what values different variab...
void convert(const goto_programt &goto_program, xmlt &dest) const
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition value_set.h:43
valuest values
Stores the LHS ID -> RHS expression set map.
Definition value_set.h:292
Definition xml.h:21
xmlt & new_element(const std::string &key)
Definition xml.h:95
std::string data
Definition xml.h:39
static void escape(const std::string &s, std::ostream &out)
escaping for XML elements
Definition xml.cpp:79
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
void convert(const goto_functionst &goto_functions, const value_set_analysist &value_set_analysis, xmlt &dest)
void value_sets_to_xml(const std::function< const value_sett &(goto_programt::const_targett)> &get_value_set, const goto_programt &goto_program, xmlt &dest)
Value Set Propagation.