14 #ifndef CPROVER_GOTO_INSTRUMENT_HAVOC_UTILS_H
15 #define CPROVER_GOTO_INSTRUMENT_HAVOC_UTILS_H
Determine whether an expression is constant.
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
Base class for all expressions.
A generic container class for the GOTO intermediate representation of one function.
A class containing utility functions for havocing expressions.
bool is_constant(const exprt &expr) const override
This function determines what expressions are to be propagated as "constants".
havoc_utils_can_forward_propagatet(const assignst &mod, const namespacet &ns)
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
havoc_utilst(const assignst &mod, const namespacet &ns)
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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Deprecated expression utility functions.
std::set< exprt > assignst