CBMC: /home/runner/work/cbmc/cbmc/src/goto-programs/goto_instruction_code.cpp File Reference

CBMC

Loading...

Searching...

No Matches

goto_instruction_code.cpp File Reference

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

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.