CBMC
Public Member Functions | Protected Attributes | List of all members
havoc_utilst Class Reference

#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. More...
 
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 More...
 
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 More...
 
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 More...
 

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()

havoc_utilst::havoc_utilst ( const assignst &  mod,
const namespacet &  ns 
)
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
locationThe source location to annotate on the havoc instruction
destThe destination goto program to append the instructions to

Definition at line 21 of file havoc_utils.cpp.

◆ append_havoc_code_for_expr()

void havoc_utilst::append_havoc_code_for_expr ( const source_locationt  location,
const exprt &  expr,
goto_programt &  dest 
)
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
locationThe source location to annotate on the havoc instruction
exprThe expression to havoc
destThe 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()

void havoc_utilst::append_object_havoc_code_for_expr ( const source_locationt  location,
const exprt &  expr,
goto_programt &  dest 
) const
virtual

Append goto instructions to havoc the underlying object of expr

Parameters
locationThe source location to annotate on the havoc instruction
exprThe expression to havoc
destThe 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()

void havoc_utilst::append_scalar_havoc_code_for_expr ( const source_locationt  location,
const exprt &  expr,
goto_programt &  dest 
) const
virtual

Append goto instructions to havoc the value of expr

Parameters
locationThe source location to annotate on the havoc instruction
exprThe expression to havoc
destThe 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

const assignst& havoc_utilst::assigns
protected

Definition at line 107 of file havoc_utils.h.

◆ is_constant

const havoc_utils_can_forward_propagatet havoc_utilst::is_constant
protected

Definition at line 108 of file havoc_utils.h.

The documentation for this class was generated from the following files: