cprover
|
Utilities for building havoc code for expressions. More...
Go to the source code of this file.
Classes | |
class | havoc_utils_is_constantt |
Typedefs | |
typedef std::set< exprt > | modifiest |
Functions | |
void | append_havoc_code (const source_locationt source_location, const modifiest &modifies, goto_programt &dest) |
void | append_object_havoc_code_for_expr (const source_locationt source_location, const exprt &expr, goto_programt &dest) |
void | append_scalar_havoc_code_for_expr (const source_locationt source_location, const exprt &expr, goto_programt &dest) |
Utilities for building havoc code for expressions.
Definition in file havoc_utils.h.
Definition at line 23 of file havoc_utils.h.
void append_havoc_code | ( | const source_locationt | source_location, |
const modifiest & | modifies, | ||
goto_programt & | dest | ||
) |
Definition at line 73 of file havoc_utils.cpp.
void append_object_havoc_code_for_expr | ( | const source_locationt | source_location, |
const exprt & | expr, | ||
goto_programt & | dest | ||
) |
Definition at line 47 of file havoc_utils.cpp.
void append_scalar_havoc_code_for_expr | ( | const source_locationt | source_location, |
const exprt & | expr, | ||
goto_programt & | dest | ||
) |
Definition at line 60 of file havoc_utils.cpp.