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  void output(const irep_idt &function_id, locationt l, std::ostream &out)
45  {
46  state.value_set.set_from(function_id, l->location_number);
47  state.value_set.set_to(function_id, l->location_number);
48  state.output(ns, out);
49  }
50 
51  void output(
52  const irep_idt &function_id,
53  const goto_programt &goto_program,
54  std::ostream &out)
55  {
56  forall_goto_program_instructions(it, goto_program)
57  {
58  out << "**** " << it->source_location << '\n';
59  output(function_id, it, out);
60  out << '\n';
61  goto_program.output_instruction(ns, function_id, out, *it);
62  out << '\n';
63  }
64  }
65 
66 protected:
68 
69  bool check_type(const typet &type);
70  void get_globals(std::list<value_set_fivrnst::entryt> &dest);
71  void add_vars(const goto_functionst &goto_functions);
72  void add_vars(const goto_programt &goto_programa);
73 
75  const symbolt &symbol,
76  std::list<value_set_fivrnst::entryt> &dest);
77 
79  const irep_idt &identifier,
80  const std::string &suffix,
81  const typet &type,
82  std::list<value_set_fivrnst::entryt> &dest);
83 
84 public:
85  // interface value_sets
86  virtual void get_values(
87  const irep_idt &function_id,
88  locationt l,
89  const exprt &expr,
90  std::list<exprt> &dest)
91  {
93  state.value_set.function_numbering.number(function_id);
95  state.value_set.function_numbering.number(function_id);
96  state.value_set.from_target_index = l->location_number;
97  state.value_set.to_target_index = l->location_number;
98  state.value_set.get_value_set(expr, dest, ns);
99  }
100 };
101 
102 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FIVRNS_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
value_set_domain_fivrnst::value_set
value_set_fivrnst value_set
Definition: value_set_domain_fivrns.h:24
value_set_analysis_fivrnst::add_vars
void add_vars(const goto_functionst &goto_functions)
typet
The type of an expression, extends irept.
Definition: type.h:29
value_set_analysis_fivrnst::get_globals
void get_globals(std::list< value_set_fivrnst::entryt > &dest)
value_set_fivrnst::set_to
void set_to(const irep_idt &function, unsigned inx)
Definition: value_set_fivrns.h:48
value_set_analysis_fivrnst::get_values
virtual void get_values(const irep_idt &function_id, locationt l, const exprt &expr, std::list< exprt > &dest)
Definition: value_set_analysis_fivrns.h:86
value_set_fivrnst::to_target_index
unsigned to_target_index
Definition: value_set_fivrns.h:38
value_set_fivrnst::from_target_index
unsigned from_target_index
Definition: value_set_fivrns.h:38
value_set_analysis_fivrnst::add_vars
void add_vars(const goto_programt &goto_programa)
exprt
Base class for all expressions.
Definition: expr.h:53
value_set_analysis_fivrnst::get_entries
void get_entries(const symbolt &symbol, std::list< value_set_fivrnst::entryt > &dest)
value_set_analysis_fivrnst
Definition: value_set_analysis_fivrns.h:24
value_set_analysis_fivrnst::track_optionst
track_optionst
Definition: value_set_analysis_fivrns.h:26
value_set_fivrnst::get_value_set
void get_value_set(const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const
value_set_analysis_fivrnst::track_options
track_optionst track_options
Definition: value_set_analysis_fivrns.h:67
value_sets.h
Value Set Propagation.
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
value_set_fivrnst::function_numbering
static hash_numbering< irep_idt, irep_id_hash > function_numbering
Definition: value_set_fivrns.h:40
value_set_analysis_fivrnst::output
void output(const irep_idt &function_id, locationt l, std::ostream &out)
Definition: value_set_analysis_fivrns.h:44
value_set_domain_fivrnst::output
virtual void output(const namespacet &ns, std::ostream &out) const
Definition: value_set_domain_fivrns.h:28
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:41
value_set_analysis_fivrnst::initialize
virtual void initialize(const goto_functionst &goto_functions)
value_set_fivrnst::to_function
unsigned to_function
Definition: value_set_fivrns.h:37
flow_insensitive_analysis.h
Flow Insensitive Static Analysis.
value_set_analysis_fivrnst::baset
flow_insensitive_analysist< value_set_domain_fivrnst > baset
Definition: value_set_analysis_fivrns.h:37
value_set_fivrnst::set_from
void set_from(const irep_idt &function, unsigned inx)
Definition: value_set_fivrns.h:42
flow_insensitive_analysis_baset::output
virtual void output(const goto_functionst &goto_functions, std::ostream &out)
Definition: flow_insensitive_analysis.cpp:60
flow_insensitive_analysis_baset::ns
const namespacet & ns
Definition: flow_insensitive_analysis.h:156
flow_insensitive_analysist< value_set_domain_fivrnst >::state
value_set_domain_fivrnst state
Definition: flow_insensitive_analysis.h:256
value_set_fivrnst::from_function
unsigned from_function
Definition: value_set_fivrns.h:37
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
flow_insensitive_analysis_baset::locationt
goto_programt::const_targett locationt
Definition: flow_insensitive_analysis.h:94
value_setst
Definition: value_sets.h:22
value_set_analysis_fivrnst::output
void output(const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out)
Definition: value_set_analysis_fivrns.h:51
symbolt
Symbol table entry.
Definition: symbol.h:28
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
value_set_analysis_fivrnst::initialize
virtual void initialize(const goto_programt &goto_program)
value_set_analysis_fivrnst::get_entries_rec
void get_entries_rec(const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fivrnst::entryt > &dest)
value_set_analysis_fivrnst::check_type
bool check_type(const typet &type)
value_set_analysis_fivrnst::TRACK_ALL_POINTERS
@ TRACK_ALL_POINTERS
Definition: value_set_analysis_fivrns.h:26
value_set_analysis_fivrnst::TRACK_FUNCTION_POINTERS
@ TRACK_FUNCTION_POINTERS
Definition: value_set_analysis_fivrns.h:26
value_set_analysis_fivrnst::value_set_analysis_fivrnst
value_set_analysis_fivrnst(const namespacet &_ns, track_optionst _track_options=TRACK_ALL_POINTERS)
Definition: value_set_analysis_fivrns.h:29
value_set_domain_fivrnst
Definition: value_set_domain_fivrns.h:22
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
flow_insensitive_analysist
Definition: flow_insensitive_analysis.h:236
value_set_domain_fivrns.h
Value Set Domain (Flow Insensitive, Validity Regions)