A class that overrides the low-level havocing functions in the base utility class, to havoc only when expressions point to valid memory, i.e.
More...
|
| havoc_if_validt (const assignst &mod, const namespacet &ns) |
|
void | append_object_havoc_code_for_expr (const source_locationt location, const exprt &expr, goto_programt &dest) const override |
| Append goto instructions to havoc the underlying object of expr
|
|
void | append_scalar_havoc_code_for_expr (const source_locationt location, const exprt &expr, goto_programt &dest) const override |
| Append goto instructions to havoc the value of expr
|
|
| havoc_utilst (const assignst &mod) |
|
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_havoc_code_for_expr (const source_locationt location, const exprt &expr, goto_programt &dest) const |
| Append goto instructions to havoc a single expression expr
|
|
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
|
|
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
|
|
A class that overrides the low-level havocing functions in the base utility class, to havoc only when expressions point to valid memory, i.e.
if all dereferences within an expression are valid
Definition at line 32 of file utils.h.