cprover
value_set_analysis_fivr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set Propagation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FIVR_H
13 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FIVR_H
14 
16 
17 #include "value_set_domain_fivr.h"
18 #include "value_sets.h"
19 
21  public value_setst,
22  public flow_insensitive_analysist<value_set_domain_fivrt>
23 {
24 public:
26 
27  // constructor
29  const namespacet &_ns,
30  track_optionst _track_options=TRACK_ALL_POINTERS):
32  track_options(_track_options)
33  {
34  }
35 
37 
38  virtual void initialize(const goto_programt &goto_program);
39  virtual void initialize(const goto_functionst &goto_functions);
40 
41  using baset::output;
42  void output(locationt l, std::ostream &out)
43  {
44  state.value_set.set_from(l->function, l->location_number);
45  state.value_set.set_to(l->function, l->location_number);
46  state.output(ns, out);
47  }
48 
49  void output(const goto_programt &goto_program, std::ostream &out)
50  {
51  forall_goto_program_instructions(it, goto_program)
52  {
53  out << "**** " << it->source_location << '\n';
54  output(it, out);
55  out << '\n';
56  goto_program.output_instruction(ns, "", out, *it);
57  out << '\n';
58  }
59  }
60 
61 protected:
63 
64  bool check_type(const typet &type);
65  void get_globals(std::list<value_set_fivrt::entryt> &dest);
66  void add_vars(const goto_functionst &goto_functions);
67  void add_vars(const goto_programt &goto_programa);
68 
69  void get_entries(
70  const symbolt &symbol,
71  std::list<value_set_fivrt::entryt> &dest);
72 
73  void get_entries_rec(
74  const irep_idt &identifier,
75  const std::string &suffix,
76  const typet &type,
77  std::list<value_set_fivrt::entryt> &dest);
78 
79 public:
80  // interface value_sets
81  virtual void get_values(
82  locationt l,
83  const exprt &expr,
84  std::list<exprt> &dest)
85  {
87  state.value_set.function_numbering.number(l->function);
89  state.value_set.function_numbering.number(l->function);
90  state.value_set.from_target_index = l->location_number;
91  state.value_set.to_target_index = l->location_number;
92  state.value_set.get_value_set(expr, dest, ns);
93  }
94 };
95 
96 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FIVR_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
value_set_fivrt::to_target_index
unsigned to_target_index
Definition: value_set_fivr.h:35
typet
The type of an expression, extends irept.
Definition: type.h:27
value_set_analysis_fivrt::track_options
track_optionst track_options
Definition: value_set_analysis_fivr.h:62
value_set_domain_fivrt::output
virtual void output(const namespacet &ns, std::ostream &out) const
Definition: value_set_domain_fivr.h:27
value_set_fivrt::set_from
void set_from(const irep_idt &function, unsigned inx)
Definition: value_set_fivr.h:39
exprt
Base class for all expressions.
Definition: expr.h:54
value_set_domain_fivr.h
value_set_analysis_fivrt::TRACK_ALL_POINTERS
@ TRACK_ALL_POINTERS
Definition: value_set_analysis_fivr.h:25
value_set_analysis_fivrt::add_vars
void add_vars(const goto_functionst &goto_functions)
Definition: value_set_analysis_fivr.cpp:108
value_set_fivrt::from_function
unsigned from_function
Definition: value_set_fivr.h:34
value_set_analysis_fivrt::get_values
virtual void get_values(locationt l, const exprt &expr, std::list< exprt > &dest)
Definition: value_set_analysis_fivr.h:81
value_set_analysis_fivrt::get_entries
void get_entries(const symbolt &symbol, std::list< value_set_fivrt::entryt > &dest)
Definition: value_set_analysis_fivr.cpp:74
value_set_analysis_fivrt::check_type
bool check_type(const typet &type)
Definition: value_set_analysis_fivr.cpp:148
value_set_analysis_fivrt::get_entries_rec
void get_entries_rec(const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fivrt::entryt > &dest)
Definition: value_set_analysis_fivr.cpp:81
value_sets.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
value_set_fivrt::get_value_set
void get_value_set(const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const
Definition: value_set_fivr.cpp:407
value_set_fivrt::to_function
unsigned to_function
Definition: value_set_fivr.h:34
goto_programt::output_instruction
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
Definition: goto_program.cpp:37
value_set_fivrt::from_target_index
unsigned from_target_index
Definition: value_set_fivr.h:35
value_set_analysis_fivrt::output
void output(locationt l, std::ostream &out)
Definition: value_set_analysis_fivr.h:42
value_set_domain_fivrt::value_set
value_set_fivrt value_set
Definition: value_set_domain_fivr.h:23
value_set_fivrt::set_to
void set_to(const irep_idt &function, unsigned inx)
Definition: value_set_fivr.h:45
value_set_analysis_fivrt::TRACK_FUNCTION_POINTERS
@ TRACK_FUNCTION_POINTERS
Definition: value_set_analysis_fivr.h:25
value_set_domain_fivrt
Definition: value_set_domain_fivr.h:20
flow_insensitive_analysis.h
value_set_analysis_fivrt::baset
flow_insensitive_analysist< value_set_domain_fivrt > baset
Definition: value_set_analysis_fivr.h:36
value_set_analysis_fivrt::get_globals
void get_globals(std::list< value_set_fivrt::entryt > &dest)
Definition: value_set_analysis_fivr.cpp:135
flow_insensitive_analysis_baset::output
virtual void output(const goto_functionst &goto_functions, std::ostream &out)
Definition: flow_insensitive_analysis.cpp:64
value_set_analysis_fivrt::output
void output(const goto_programt &goto_program, std::ostream &out)
Definition: value_set_analysis_fivr.h:49
flow_insensitive_analysis_baset::ns
const namespacet & ns
Definition: flow_insensitive_analysis.h:156
flow_insensitive_analysist< value_set_domain_fivrt >::state
value_set_domain_fivrt state
Definition: flow_insensitive_analysis.h:257
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
flow_insensitive_analysis_baset::locationt
goto_programt::const_targett locationt
Definition: flow_insensitive_analysis.h:92
value_setst
Definition: value_sets.h:21
symbolt
Symbol table entry.
Definition: symbol.h:27
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
value_set_analysis_fivrt::initialize
virtual void initialize(const goto_programt &goto_program)
Definition: value_set_analysis_fivr.cpp:22
value_set_analysis_fivrt::track_optionst
track_optionst
Definition: value_set_analysis_fivr.h:25
value_set_fivrt::function_numbering
static hash_numbering< irep_idt, irep_id_hash > function_numbering
Definition: value_set_fivr.h:37
value_set_analysis_fivrt::value_set_analysis_fivrt
value_set_analysis_fivrt(const namespacet &_ns, track_optionst _track_options=TRACK_ALL_POINTERS)
Definition: value_set_analysis_fivr.h:28
value_set_analysis_fivrt
Definition: value_set_analysis_fivr.h:20
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
flow_insensitive_analysist
Definition: flow_insensitive_analysis.h:236