A class that overrides the low-level havocing functions in the base utility class, to havoc only when expressions point to valid memory, i.e. More...

#include <utils.h>

Inheritance diagram for havoc_if_validt:

Collaboration diagram for havoc_if_validt:

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

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

Protected Attributes
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 overrides the low-level havocing functions in the base utility class, to havoc only when expressions point to valid memory, i.e.

if all dereferences within an expression are valid

Definition at line 67 of file utils.h.

Constructor & Destructor Documentation

havoc_if_validt::havoc_if_validt	(	const assignst &	mod,
		const namespacet &	ns
	)

inline

Definition at line 70 of file utils.h.

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

overridevirtual

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

Definition at line 88 of file utils.cpp.

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

overridevirtual

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

Definition at line 98 of file utils.cpp.

const namespacet& havoc_if_validt::ns

protected

Definition at line 86 of file utils.h.

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