A class that further overrides the "safe" havoc utilities, and adds support for havocing pointer_object expressions. More...

#include <utils.h>

Inheritance diagram for havoc_assigns_targetst:

Collaboration diagram for havoc_assigns_targetst:

Public Member Functions
	havoc_assigns_targetst (const assignst &mod, symbol_tablet &st, message_handlert &message_handler, const irep_idt &mode)

void	append_havoc_pointer_code (const source_locationt location, const exprt &ptr_to_ptr, goto_programt &dest)

void	append_havoc_slice_code (const source_locationt location, const exprt &ptr, const exprt &size, goto_programt &dest)

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

Public Member Functions inherited from havoc_if_validt
	havoc_if_validt (const assignst &mod, const namespacet &ns)

void	append_object_havoc_code_for_expr (const source_locationt location, const exprt &expr, goto_programt &dest) const override
	Append goto instructions to havoc the underlying object of `expr` More...

void	append_scalar_havoc_code_for_expr (const source_locationt location, const exprt &expr, goto_programt &dest) const override
	Append goto instructions to havoc the value of `expr` More...

Public Member Functions inherited from havoc_utilst
	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...

Public Attributes
namespacet	ns

cleanert	cleaner

messaget	log

const irep_idt &	mode

Additional Inherited Members
Protected Attributes inherited from havoc_if_validt
const namespacet &	ns

Protected Attributes inherited from havoc_utilst
const assignst &	assigns

const havoc_utils_can_forward_propagatet	is_constant

Detailed Description

A class that further overrides the "safe" havoc utilities, and adds support for havocing pointer_object expressions.

Definition at line 91 of file utils.h.

Constructor & Destructor Documentation

◆ havoc_assigns_targetst()

havoc_assigns_targetst::havoc_assigns_targetst	(	const assignst &	mod,
		symbol_tablet &	st,
		message_handlert &	message_handler,
		const irep_idt &	mode
	)

inline

Definition at line 94 of file utils.h.

Member Function Documentation

◆ append_havoc_code_for_expr()

void havoc_assigns_targetst::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 from havoc_utilst.

Definition at line 108 of file utils.cpp.

◆ append_havoc_pointer_code()

void havoc_assigns_targetst::append_havoc_pointer_code	(	const source_locationt	location,
		const exprt &	ptr_to_ptr,
		goto_programt &	dest
	)

Definition at line 76 of file utils.cpp.

◆ append_havoc_slice_code()

void havoc_assigns_targetst::append_havoc_slice_code	(	const source_locationt	location,
		const exprt &	ptr,
		const exprt &	size,
		goto_programt &	dest
	)

Definition at line 54 of file utils.cpp.

Member Data Documentation

◆ cleaner

cleanert havoc_assigns_targetst::cleaner

Definition at line 124 of file utils.h.

◆ log

messaget havoc_assigns_targetst::log

Definition at line 125 of file utils.h.

◆ mode

const irep_idt& havoc_assigns_targetst::mode

Definition at line 126 of file utils.h.

◆ ns

namespacet havoc_assigns_targetst::ns

Definition at line 123 of file utils.h.

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

/home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/utils.h
/home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/utils.cpp

Public Member Functions

Public Attributes

Additional Inherited Members