cprover
havoc_utils.cpp File Reference

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>
+ Include dependency graph for havoc_utils.cpp:

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)
 

Detailed Description

Utilities for building havoc code for expressions.

Definition in file havoc_utils.cpp.

Function Documentation

◆ append_havoc_code()

void append_havoc_code ( const source_locationt  source_location,
const modifiest modifies,
goto_programt dest 
)

Definition at line 73 of file havoc_utils.cpp.

◆ append_object_havoc_code_for_expr()

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.

◆ append_safe_havoc_code_for_expr()

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.

◆ append_scalar_havoc_code_for_expr()

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.