cprover
value_set_analysis_fi.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set Propagation (flow insensitive)
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FI_H
13 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FI_H
14 
16 
17 #include "value_set_domain_fi.h"
18 #include "value_sets.h"
19 
21  public value_setst,
22  public flow_insensitive_analysist<value_set_domain_fit>
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 protected:
43 
44  bool check_type(const typet &type);
45  void get_globals(std::list<value_set_fit::entryt> &dest);
46  void add_vars(const goto_functionst &goto_functions);
47  void add_vars(const goto_programt &goto_programa);
48 
49  void get_entries(
50  const symbolt &symbol,
51  std::list<value_set_fit::entryt> &dest);
52 
53  void get_entries_rec(
54  const irep_idt &identifier,
55  const std::string &suffix,
56  const typet &type,
57  std::list<value_set_fit::entryt> &dest);
58 
59 public:
60  // interface value_sets
61  DEPRECATED(SINCE(2019, 05, 22, "Use the version returning list instead"))
62  void get_values(
63  const irep_idt &function_id,
64  locationt l,
65  const exprt &expr,
66  std::list<exprt> &dest) override
67  {
69  state.value_set.function_numbering.number(function_id);
71  state.value_set.function_numbering.number(function_id);
72  state.value_set.from_target_index = l->location_number;
73  state.value_set.to_target_index = l->location_number;
74  state.value_set.get_value_set(expr, dest, ns);
75  }
76 
77  std::vector<exprt> get_values(
78  const irep_idt &function_id,
79  locationt l,
80  const exprt &expr) override;
81 };
82 
83 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FI_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
flow_insensitive_analysist< value_set_domain_fit >::locationt
goto_programt::const_targett locationt
Definition: flow_insensitive_analysis.h:244
value_set_fit::function_numbering
static hash_numbering< irep_idt, irep_id_hash > function_numbering
Definition: value_set_fi.h:42
value_set_analysis_fit::baset
flow_insensitive_analysist< value_set_domain_fit > baset
Definition: value_set_analysis_fi.h:36
typet
The type of an expression, extends irept.
Definition: type.h:29
value_set_analysis_fit::get_entries_rec
void get_entries_rec(const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fit::entryt > &dest)
Definition: value_set_analysis_fi.cpp:91
value_set_analysis_fit::value_set_analysis_fit
value_set_analysis_fit(const namespacet &_ns, track_optionst _track_options=TRACK_ALL_POINTERS)
Definition: value_set_analysis_fi.h:28
value_set_fit::from_function
unsigned from_function
Definition: value_set_fi.h:39
exprt
Base class for all expressions.
Definition: expr.h:53
value_set_domain_fit::value_set
value_set_fit value_set
Definition: value_set_domain_fi.h:23
value_set_fit::from_target_index
unsigned from_target_index
Definition: value_set_fi.h:40
value_set_fit::to_target_index
unsigned to_target_index
Definition: value_set_fi.h:40
value_set_analysis_fit
Definition: value_set_analysis_fi.h:23
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_analysis_fit::initialize
void initialize(const goto_programt &goto_program) override
Definition: value_set_analysis_fi.cpp:22
value_set_domain_fi.h
Value Set (Flow Insensitive)
value_set_fit::get_value_set
void get_value_set(const exprt &expr, std::list< exprt > &dest, const namespacet &ns) const
Definition: value_set_fi.cpp:297
value_set_analysis_fit::get_globals
void get_globals(std::list< value_set_fit::entryt > &dest)
Definition: value_set_analysis_fi.cpp:145
value_set_analysis_fit::track_optionst
track_optionst
Definition: value_set_analysis_fi.h:25
flow_insensitive_analysis.h
Flow Insensitive Static Analysis.
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
value_set_analysis_fit::check_type
bool check_type(const typet &type)
Definition: value_set_analysis_fi.cpp:158
flow_insensitive_analysis_baset::ns
const namespacet & ns
Definition: flow_insensitive_analysis.h:156
value_set_analysis_fit::TRACK_FUNCTION_POINTERS
@ TRACK_FUNCTION_POINTERS
Definition: value_set_analysis_fi.h:25
flow_insensitive_analysist< value_set_domain_fit >::state
value_set_domain_fit state
Definition: flow_insensitive_analysis.h:256
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
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
symbolt
Symbol table entry.
Definition: symbol.h:28
value_set_analysis_fit::get_entries
void get_entries(const symbolt &symbol, std::list< value_set_fit::entryt > &dest)
Definition: value_set_analysis_fi.cpp:84
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
value_set_domain_fit
Definition: value_set_domain_fi.h:21
value_set_fit::to_function
unsigned to_function
Definition: value_set_fi.h:39
value_set_analysis_fit::get_values
void get_values(const irep_idt &function_id, locationt l, const exprt &expr, std::list< exprt > &dest) override
Definition: value_set_analysis_fi.h:62
value_set_analysis_fit::track_options
track_optionst track_options
Definition: value_set_analysis_fi.h:42
value_set_analysis_fit::add_vars
void add_vars(const goto_functionst &goto_functions)
Definition: value_set_analysis_fi.cpp:118
value_set_analysis_fit::TRACK_ALL_POINTERS
@ TRACK_ALL_POINTERS
Definition: value_set_analysis_fi.h:25
flow_insensitive_analysist
Definition: flow_insensitive_analysis.h:236