cprover
Loading...
Searching...
No Matches
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 <set>
18
20
21#include <util/expr_util.h>
22
23typedef std::set<exprt> assignst;
24
27{
28public:
30 {
31 }
32
33 bool is_constant(const exprt &expr) const override
34 {
35 // Besides the "usual" constants (checked in is_constantt::is_constant),
36 // we also treat unmodified symbols as constants
37 if(expr.id() == ID_symbol && assigns.find(expr) == assigns.end())
38 return true;
39
40 return is_constantt::is_constant(expr);
41 }
42
43protected:
45};
46
48{
49public:
51 {
52 }
53
62 const source_locationt location,
63 goto_programt &dest) const;
64
76 virtual void append_havoc_code_for_expr(
77 const source_locationt location,
78 const exprt &expr,
79 goto_programt &dest) const;
80
87 const source_locationt location,
88 const exprt &expr,
89 goto_programt &dest) const;
90
97 const source_locationt location,
98 const exprt &expr,
99 goto_programt &dest) const;
100
101protected:
104};
105
106#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:564
Base class for all expressions.
Definition expr.h:54
A generic container class for the GOTO intermediate representation of one function.
A class containing utility functions for havocing expressions.
Definition havoc_utils.h:27
bool is_constant(const exprt &expr) const override
This function determines what expressions are to be propagated as "constants".
Definition havoc_utils.h:33
const assignst & assigns
Definition havoc_utils.h:44
havoc_utils_is_constantt(const assignst &mod)
Definition havoc_utils.h:29
virtual void append_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const
Append goto instructions to havoc a single expression expr
const havoc_utils_is_constantt is_constant
havoc_utilst(const assignst &mod)
Definition havoc_utils.h:50
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
void append_full_havoc_code(const source_locationt location, goto_programt &dest) const
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:396
Determine whether an expression is constant.
Definition expr_util.h:89
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
Deprecated expression utility functions.
Concrete Goto Program.
std::set< exprt > assignst
Definition havoc_utils.h:23