CBMC
Loading...
Searching...
No Matches
Public Member Functions | Protected Attributes | List of all members
havoc_utilst Class Reference

#include <havoc_utils.h>

+ Inheritance diagram for havoc_utilst:
[フレーム]
[legend]
+ Collaboration diagram for havoc_utilst:
[フレーム]
[legend]

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

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
location The source location to annotate on the havoc instruction
dest The 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
location The source location to annotate on the havoc instruction
expr The expression to havoc
dest The 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
location The source location to annotate on the havoc instruction
expr The expression to havoc
dest The 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
location The source location to annotate on the havoc instruction
expr The expression to havoc
dest The 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:

AltStyle によって変換されたページ (->オリジナル) /