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