CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
havoc_utils.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Utilities for building havoc code for expressions.
4
5Author: Saswat Padhi, saspadhi@amazon.com
6
7Date: 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
22class goto_programt;
23
24typedef std::set<exprt> assignst;
25
28{
29public:
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
48protected:
50};
51
53{
54public:
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
106protected:
109};
110
111#endif // CPROVER_GOTO_INSTRUMENT_HAVOC_UTILS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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".
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.
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
const havoc_utils_can_forward_propagatet is_constant
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
const assignst & assigns
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.
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
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:91
Deprecated expression utility functions.
std::set< exprt > assignst
Definition havoc_utils.h:24