CBMC
havoc_utils.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Utilities for building havoc code for expressions.
4 
5 Author: Saswat Padhi, saspadhi@amazon.com
6 
7 Date: July 2021
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_INSTRUMENT_HAVOC_UTILS_H
15 #define CPROVER_GOTO_INSTRUMENT_HAVOC_UTILS_H
16 
17 #include <util/expr.h>
18 #include <util/expr_util.h>
19 
20 #include <set>
21 
22 class goto_programt;
23 
24 typedef std::set<exprt> assignst;
25 
28 {
29 public:
31  const assignst &mod,
32  const namespacet &ns)
34  {
35  }
36 
37  bool is_constant(const exprt &expr) const override
38  {
39  // Besides the "usual" constants (checked in
40  // can_forward_propagatet::is_constant), we also treat unmodified symbols as
41  // constants
42  if(expr.id() == ID_symbol && assigns.find(expr) == assigns.end())
43  return true;
44 
46  }
47 
48 protected:
49  const assignst &assigns;
50 };
51 
53 {
54 public:
55  explicit havoc_utilst(const assignst &mod, const namespacet &ns)
56  : assigns(mod), is_constant(mod, ns)
57  {
58  }
59 
67  void
69 
81  virtual void append_havoc_code_for_expr(
82  const source_locationt location,
83  const exprt &expr,
84  goto_programt &dest);
85 
92  const source_locationt location,
93  const exprt &expr,
94  goto_programt &dest) const;
95 
102  const source_locationt location,
103  const exprt &expr,
104  goto_programt &dest) const;
105 
106 protected:
109 };
110 
111 #endif // CPROVER_GOTO_INSTRUMENT_HAVOC_UTILS_H
Determine whether an expression is constant.
Definition: expr_util.h:91
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
Definition: expr_util.cpp:203
const namespacet & ns
Definition: expr_util.h:104
Base class for all expressions.
Definition: expr.h:56
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
A class containing utility functions for havocing expressions.
Definition: havoc_utils.h:28
bool is_constant(const exprt &expr) const override
This function determines what expressions are to be propagated as "constants".
Definition: havoc_utils.h:37
havoc_utils_can_forward_propagatet(const assignst &mod, const namespacet &ns)
Definition: havoc_utils.h:30
virtual void append_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest)
Append goto instructions to havoc a single expression expr
Definition: havoc_utils.cpp:29
const havoc_utils_can_forward_propagatet is_constant
Definition: havoc_utils.h:108
virtual void append_object_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const
Append goto instructions to havoc the underlying object of expr
Definition: havoc_utils.cpp:46
const assignst & assigns
Definition: havoc_utils.h:107
havoc_utilst(const assignst &mod, const namespacet &ns)
Definition: havoc_utils.h:55
void append_full_havoc_code(const source_locationt location, goto_programt &dest)
Append goto instructions to havoc the full assigns set.
Definition: havoc_utils.cpp:21
virtual void append_scalar_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const
Append goto instructions to havoc the value of expr
Definition: havoc_utils.cpp:57
const irep_idt & id() const
Definition: irep.h:388
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
Deprecated expression utility functions.
std::set< exprt > assignst
Definition: havoc_utils.h:22