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  void initialize(const goto_programt &goto_program) override;
39  void initialize(const goto_functionst &goto_functions) override;
40 
41  using baset::output;
42  void output(const irep_idt &function_id, locationt l, std::ostream &out)
43  {
44  state.value_set.set_from(function_id, l->location_number);
45  state.value_set.set_to(function_id, l->location_number);
46  state.output(ns, out);
47  }
48 
49  void output(
50  const irep_idt &function_id,
51  const goto_programt &goto_program,
52  std::ostream &out) override
53  {
54  forall_goto_program_instructions(it, goto_program)
55  {
56  out << "**** " << it->source_location << '\n';
57  output(function_id, it, out);
58  out << '\n';
59  goto_program.output_instruction(ns, function_id, out, *it);
60  out << '\n';
61  }
62  }
63 
64 protected:
66 
67  bool check_type(const typet &type);
68  void get_globals(std::list<value_set_fivrt::entryt> &dest);
69  void add_vars(const goto_functionst &goto_functions);
70  void add_vars(const goto_programt &goto_programa);
71 
73  const symbolt &symbol,
74  std::list<value_set_fivrt::entryt> &dest);
75 
77  const irep_idt &identifier,
78  const std::string &suffix,
79  const typet &type,
80  std::list<value_set_fivrt::entryt> &dest);
81 
82 public:
83  // interface value_sets
84  void get_values(
85  const irep_idt &function_id,
86  locationt l,
87  const exprt &expr,
88  std::list<exprt> &dest) override
89  {
94  state.value_set.from_target_index = l->location_number;
95  state.value_set.to_target_index = l->location_number;
96  state.value_set.get_value_set(expr, dest, ns);
97  }
98 };
99 
100 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FIVR_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
virtual void output(const goto_functionst &goto_functions, std::ostream &out)
goto_programt::const_targett locationt
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
number_type number(const key_type &a)
Definition: numbering.h:37
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:28
void get_values(const irep_idt &function_id, locationt l, const exprt &expr, std::list< exprt > &dest) override
void initialize(const goto_programt &goto_program) override
bool check_type(const typet &type)
value_set_analysis_fivrt(const namespacet &_ns, track_optionst _track_options=TRACK_ALL_POINTERS)
void add_vars(const goto_programt &goto_programa)
flow_insensitive_analysist< value_set_domain_fivrt > baset
void get_entries_rec(const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fivrt::entryt > &dest)
void initialize(const goto_functionst &goto_functions) override
void output(const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) override
void output(const irep_idt &function_id, locationt l, std::ostream &out)
void get_globals(std::list< value_set_fivrt::entryt > &dest)
void add_vars(const goto_functionst &goto_functions)
void get_entries(const symbolt &symbol, std::list< value_set_fivrt::entryt > &dest)
void output(const namespacet &ns, std::ostream &out) const override
unsigned to_function
void get_value_set(const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const
unsigned to_target_index
unsigned from_target_index
static numberingt< irep_idt > function_numbering
void set_from(const irep_idt &function, unsigned inx)
unsigned from_function
void set_to(const irep_idt &function, unsigned inx)
Flow Insensitive Static Analysis.
#define forall_goto_program_instructions(it, program)
Value Set (Flow Insensitive, Sharing, Validity Regions)
Value Set Propagation.