cprover
value_set_analysis_fivrns.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set Analysis (Flow Insensitive, Validity Regions)
4 
5 Author: Daniel Kroening, kroening@kroening.com,
6  CM Wintersteiger
7 
8 \*******************************************************************/
9 
12 
13 #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FIVRNS_H
14 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FIVRNS_H
15 
17 
19 #include "value_sets.h"
20 
22  public value_setst,
23  public flow_insensitive_analysist<value_set_domain_fivrnst>
24 {
25 public:
27 
28  // constructor
30  const namespacet &_ns,
31  track_optionst _track_options=TRACK_ALL_POINTERS):
33  track_options(_track_options)
34  {
35  }
36 
38 
39  virtual void initialize(const goto_programt &goto_program);
40  virtual void initialize(const goto_functionst &goto_functions);
41 
42  using baset::output;
43 
44  virtual void output(locationt l, std::ostream &out)
45  {
46  state.value_set.set_from(l->function, l->location_number);
47  state.value_set.set_to(l->function, l->location_number);
48  state.output(ns, out);
49  }
50 
51  void output(const goto_programt &goto_program, std::ostream &out)
52  {
53  forall_goto_program_instructions(it, goto_program)
54  {
55  out << "**** " << it->source_location << '\n';
56  output(it, out);
57  out << '\n';
58  goto_program.output_instruction(ns, "", out, it);
59  out << '\n';
60  }
61  }
62 
63 protected:
65 
66  bool check_type(const typet &type);
67  void get_globals(std::list<value_set_fivrnst::entryt> &dest);
68  void add_vars(const goto_functionst &goto_functions);
69  void add_vars(const goto_programt &goto_programa);
70 
71  void get_entries(
72  const symbolt &symbol,
73  std::list<value_set_fivrnst::entryt> &dest);
74 
75  void get_entries_rec(
76  const irep_idt &identifier,
77  const std::string &suffix,
78  const typet &type,
79  std::list<value_set_fivrnst::entryt> &dest);
80 
81 public:
82  // interface value_sets
83  virtual void get_values(
84  locationt l,
85  const exprt &expr,
86  std::list<exprt> &dest)
87  {
92  state.value_set.from_target_index = l->location_number;
93  state.value_set.to_target_index = l->location_number;
94  state.value_set.get_value_set(expr, dest, ns);
95  }
96 };
97 
98 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FIVRNS_H
The type of an expression.
Definition: type.h:20
void output(const goto_programt &goto_program, std::ostream &out)
virtual void output(const namespacet &ns, std::ostream &out) const
void get_globals(std::list< value_set_fivrnst::entryt > &dest)
Value Set Domain (Flow Insensitive, Validity Regions)
void set_to(const irep_idt &function, unsigned inx)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
virtual void get_values(locationt l, const exprt &expr, std::list< exprt > &dest)
void get_entries(const symbolt &symbol, std::list< value_set_fivrnst::entryt > &dest)
goto_programt::const_targett locationt
Value Set Propagation.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
flow_insensitive_analysist< value_set_domain_fivrnst > baset
Flow Insensitive Static Analysis.
static hash_numbering< irep_idt, irep_id_hash > function_numbering
virtual void initialize(const goto_programt &goto_program)
Base class for all expressions.
Definition: expr.h:46
void get_entries_rec(const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fivrnst::entryt > &dest)
void get_value_set(const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const
value_set_analysis_fivrnst(const namespacet &_ns, track_optionst _track_options=TRACK_ALL_POINTERS)
std::ostream & output_instruction(const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const
See below.
virtual void output(locationt l, std::ostream &out)
number_type number(const T &a)
Definition: numbering.h:80
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
virtual void output(const goto_functionst &goto_functions, std::ostream &out)
unsigned from_target_index
void set_from(const irep_idt &function, unsigned inx)
void add_vars(const goto_functionst &goto_functions)