Data structures representing instructions in a GOTO program. More...

#include "goto_instruction_code.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/cprover_prefix.h>
#include <util/namespace.h>
#include <util/std_expr.h>
#include <util/string_constant.h>
#include <util/symbol.h>

Include dependency graph for goto_instruction_code.cpp:

Go to the source code of this file.

Functions
code_function_callt	havoc_slice_call (const exprt &p, const exprt &size, const namespacet &ns)
	Builds a code_function_callt to `__CPROVER_havoc_slice(p, size)`. More...

Detailed Description

Data structures representing instructions in a GOTO program.

Definition in file goto_instruction_code.cpp.

Function Documentation

◆ havoc_slice_call()

code_function_callt havoc_slice_call	(	const exprt &	p,
		const exprt &	size,
		const namespacet &	ns
	)

inline

Builds a code_function_callt to __CPROVER_havoc_slice(p, size).

Parameters

p	The pointer argument.
size	The size argument.
ns	Namespace where the `__CPROVER_havoc_slice symbol` can be found.

Remarks: : It is a PRECONDITION that __CPROVER_havoc_slice exists in the namespace

Returns: A code_function_callt expression nil_exprt() := __CPROVER_havoc_slice(p, size).

Definition at line 81 of file goto_instruction_code.cpp.

Functions

Detailed Description

Function Documentation

◆ havoc_slice_call()