cprover
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 <set>
18 
20 
21 #include <util/expr_util.h>
22 
23 typedef std::set<exprt> modifiest;
24 
26 {
27 public:
28  explicit havoc_utils_is_constantt(const modifiest &mod) : modifies(mod)
29  {
30  }
31 
32  bool is_constant(const exprt &expr) const override
33  {
34  // Besides the "usual" constants (checked in is_constantt::is_constant),
35  // we also treat unmodified symbols as constants
36  if(expr.id() == ID_symbol && modifies.find(expr) == modifies.end())
37  return true;
38 
39  return is_constantt::is_constant(expr);
40  }
41 
42 protected:
44 };
45 
47  const source_locationt source_location,
48  const modifiest &modifies,
49  goto_programt &dest);
50 
52  const source_locationt source_location,
53  const exprt &expr,
54  goto_programt &dest);
55 
57  const source_locationt source_location,
58  const exprt &expr,
59  goto_programt &dest);
60 
61 #endif // CPROVER_GOTO_INSTRUMENT_HAVOC_UTILS_H
is_constantt
Determine whether an expression is constant.
Definition: expr_util.h:85
append_scalar_havoc_code_for_expr
void append_scalar_havoc_code_for_expr(const source_locationt source_location, const exprt &expr, goto_programt &dest)
Definition: havoc_utils.cpp:60
havoc_utils_is_constantt
Definition: havoc_utils.h:26
append_havoc_code
void append_havoc_code(const source_locationt source_location, const modifiest &modifies, goto_programt &dest)
Definition: havoc_utils.cpp:73
exprt
Base class for all expressions.
Definition: expr.h:54
append_object_havoc_code_for_expr
void append_object_havoc_code_for_expr(const source_locationt source_location, const exprt &expr, goto_programt &dest)
Definition: havoc_utils.cpp:47
modifiest
std::set< exprt > modifiest
Definition: havoc_utils.h:23
is_constantt::is_constant
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
Definition: expr_util.cpp:225
havoc_utils_is_constantt::havoc_utils_is_constantt
havoc_utils_is_constantt(const modifiest &mod)
Definition: havoc_utils.h:28
havoc_utils_is_constantt::is_constant
bool is_constant(const exprt &expr) const override
This function determines what expressions are to be propagated as "constants".
Definition: havoc_utils.h:32
irept::id
const irep_idt & id() const
Definition: irep.h:407
goto_program.h
Concrete Goto Program.
source_locationt
Definition: source_location.h:19
expr_util.h
Deprecated expression utility functions.
havoc_utils_is_constantt::modifies
const modifiest & modifies
Definition: havoc_utils.h:43
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71