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 More...
|
|
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 More...
|
|
| 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. More...
|
|
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 More...
|
|
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 More...
|
|
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 More...
|
|
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.