cprover
|
Utilities for building havoc code for expressions. More...
#include "havoc_utils.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/pointer_expr.h>
Go to the source code of this file.
Functions | |
void | append_safe_havoc_code_for_expr (const source_locationt source_location, const exprt &expr, goto_programt &dest, const std::function< void()> &havoc_code_impl) |
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) |
void | append_havoc_code (const source_locationt source_location, const modifiest &modifies, goto_programt &dest) |
Utilities for building havoc code for expressions.
Definition in file havoc_utils.cpp.
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_safe_havoc_code_for_expr | ( | const source_locationt | source_location, |
const exprt & | expr, | ||
goto_programt & | dest, | ||
const std::function< void()> & | havoc_code_impl | ||
) |
Definition at line 20 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.