14 #ifndef CPROVER_GOTO_INSTRUMENT_HAVOC_UTILS_H
15 #define CPROVER_GOTO_INSTRUMENT_HAVOC_UTILS_H
Base class for all expressions.
A generic container class for the GOTO intermediate representation of one function.
const modifiest & modifies
bool is_constant(const exprt &expr) const override
This function determines what expressions are to be propagated as "constants".
havoc_utils_is_constantt(const modifiest &mod)
const irep_idt & id() const
Determine whether an expression is constant.
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
Deprecated expression utility functions.
void append_object_havoc_code_for_expr(const source_locationt source_location, const exprt &expr, goto_programt &dest)
std::set< exprt > modifiest
void append_havoc_code(const source_locationt source_location, const modifiest &modifies, goto_programt &dest)
void append_scalar_havoc_code_for_expr(const source_locationt source_location, const exprt &expr, goto_programt &dest)