cprover
havoc_utils.h File Reference

Utilities for building havoc code for expressions. More...

#include <set>
#include <goto-programs/goto_program.h>
#include <util/expr_util.h>
+ Include dependency graph for havoc_utils.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  havoc_utils_is_constantt
 

Typedefs

typedef std::set< exprtmodifiest
 

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)
 

Detailed Description

Utilities for building havoc code for expressions.

Definition in file havoc_utils.h.

Typedef Documentation

◆ modifiest

typedef std::set<exprt> modifiest

Definition at line 23 of file havoc_utils.h.

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_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.