havoc_assigns_targetst Class Reference
A class that further overrides the "safe" havoc utilities, and adds support for havocing pointer_object expressions. More...
#include <utils.h>
Inheritance diagram for havoc_assigns_targetst: Collaboration diagram for havoc_assigns_targetst:Public Member Functions | |
| havoc_assigns_targetst (const assignst &mod, const namespacet &ns) | |
| void | append_havoc_code_for_expr (const source_locationt location, const exprt &expr, goto_programt &dest) const override |
Append goto instructions to havoc a single expression expr More... | |
| Public Member Functions inherited from havoc_if_validt | |
| 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... | |
| Public Member Functions inherited from havoc_utilst | |
| 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... | |
Additional Inherited Members | |
| Protected Attributes inherited from havoc_if_validt | |
| const namespacet & | ns |
| Protected Attributes inherited from havoc_utilst | |
| const assignst & | assigns |
| const havoc_utils_is_constantt | is_constant |
Detailed Description
A class that further overrides the "safe" havoc utilities, and adds support for havocing pointer_object expressions.
Constructor & Destructor Documentation
◆ havoc_assigns_targetst()
|
inline |
Member Function Documentation
◆ append_havoc_code_for_expr()
|
overridevirtual |
Append goto instructions to havoc a single expression expr
If expr is an array index or object dereference expression, with a non-constant offset, e.g. a[i] or *(b+i) with a non-constant i, then instructions are generated to havoc the entire underlying object. Otherwise, e.g. for a[0] or *(b+i) when i is a known constant, the instructions are generated to only havoc the scalar value of expr.
- Parameters
-
location The source location to annotate on the havoc instruction expr The expression to havoc dest The destination goto program to append the instructions to
Reimplemented from havoc_utilst.
The documentation for this class was generated from the following files:
