#include <havoc_utils.h>
Inheritance diagram for havoc_utilst: Collaboration diagram for havoc_utilst:Public Member Functions | |
| havoc_utilst (const assignst &mod, const namespacet &ns) | |
| void | append_full_havoc_code (const source_locationt location, goto_programt &dest) |
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) |
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 | |
Protected Attributes | |
| const assignst & | assigns |
| const havoc_utils_can_forward_propagatet | is_constant |
Detailed Description
Definition at line 52 of file havoc_utils.h.
Constructor & Destructor Documentation
◆ havoc_utilst()
|
inlineexplicit |
Definition at line 55 of file havoc_utils.h.
Member Function Documentation
◆ append_full_havoc_code()
| void havoc_utilst::append_full_havoc_code | ( | const source_locationt | location, |
| goto_programt & | dest | ||
| ) |
Append goto instructions to havoc the full assigns set.
This function invokes append_havoc_code_for_expr on each expression in the assigns set.
- Parameters
-
location The source location to annotate on the havoc instruction dest The destination goto program to append the instructions to
Definition at line 21 of file havoc_utils.cpp.
◆ append_havoc_code_for_expr()
|
virtual |
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 in havoc_assigns_targetst.
Definition at line 29 of file havoc_utils.cpp.
◆ append_object_havoc_code_for_expr()
|
virtual |
Append goto instructions to havoc the underlying object 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 in havoc_if_validt.
Definition at line 46 of file havoc_utils.cpp.
◆ append_scalar_havoc_code_for_expr()
|
virtual |
Append goto instructions to havoc the 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 in havoc_if_validt.
Definition at line 57 of file havoc_utils.cpp.
Member Data Documentation
◆ assigns
Definition at line 107 of file havoc_utils.h.
◆ is_constant
|
protected |
Definition at line 108 of file havoc_utils.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/goto-instrument/havoc_utils.h
- /home/runner/work/cbmc/cbmc/src/goto-instrument/havoc_utils.cpp
