Man page - goto-harness(1)

Packages contains this manual

Package: cbmc
apt-get install cbmc

Manuals in package:

Documentations in package:

cbmc

Manual

GOTO-HARNESS

NAME
SYNOPSIS
DESCRIPTION
OPTIONS
Common generator options
Function harness generator (--harness-type call-function):
Memory snapshot harness generator (--harness-typeinitialise-from-memory-snapshot):
ENVIRONMENT
BUGS
SEE ALSO
COPYRIGHT

NAME

goto-harness - Generate environments for symbolic analysis

SYNOPSIS

goto-harness [-?] [-h] [--help]

show help

goto-harness --version

show version

goto-harness in out --harness-function-name name --harness-type
harness-type [ harness-options ]

build harness for in and write harness to out ; the harness is printed as C code, if out has a .c suffix, else a GOTO binary including the harness is generated

DESCRIPTION

goto-harness constructs functions that set up an appropriate environment before calling functions under analysis. This is most useful when trying to analyze an isolated unit of a program.

A typical sequence of tool invocations is as follows. Given a C program program.c , we generate a harness for function test_function :

# Compile the program
goto-cc program.c -o program.gb
# Run goto-harness to produce harness file
goto-harness --harness-type call-function --harness-function-name generated_harness_test_function
--function test_function program.gb harness.c
# Run the checks targeting the generated harness
cbmc --pointer-check harness.c --function generated_harness_test_function

goto-harness has two main modes of operation. First,function-call harnesses, which automatically synthesize an environment without having any information about the program state. Second, memory-snapshot harnesses, in which case goto-harness loads an existing program state as generated by memory-analyzer (1) and selectively havocs some variables.

OPTIONS

--harness-function-name name

Use name as the name of the harness function that is generated, i.e., the new entry point.

--harness-type [ call-function | initialize-with-memory-snapshot ]

Select the type of harness to generate. In addition to options applicable to both harness generators, each of them also has dedicated options that are described below.

Common generator options

--min-null-tree-depth N

Set the minimum level at which a pointer can first be NULL in a recursively non-deterministically initialized struct to N . Defaults to 1.

--max-nondet-tree-depth N

Set the maximum height of the non-deterministic object tree to N . At that level, all pointers will be set to NULL . Defaults to 2.

--min-array-size N

Set the minimum size of arrays of non-constant size allocated by the harness to N . Defaults to 1.

--max-array-size N

Set the maximum size of arrays of non-constant size allocated by the harness to N . Defaults to 2.

--nondet-globals

Set global variables to non-deterministic values in harness.

--havoc-member member-expr

Non-deterministically initialize member-expr of some global object (may be given multiple times).

--function-pointer-can-be-null function-name

Name of parameters of the target function or of global variables of function-pointer type that can non-deterministically be set to NULL .

Function harness generator (--harness-type call-function):

--function function-name

Generate an environment to call function function-name , which the harness will then call.

--treat-pointer-as-array p

Treat the (pointer-typed) function parameter with name p as an array.

--associated-array-size array_name : size_name

Set the function parameter size_name to the size of the array parameter array_name (implies --treat-pointer-as-array array_name ).

--treat-pointers-equal p , q , r [; s , t ]

Assume the pointer-typed function parameters q and r are equal to parameter p , and s equal to t , and so on.

--treat-pointers-equal-maybe

Function parameter equality is non-deterministic.

--treat-pointer-as-cstring p

Treat the function parameter with the name p as a string of characters.

Memory snapshot harness generator (--harness-typeinitialise-from-memory-snapshot):

--memory-snapshot file

Initialize memory from JSON memory snapshot stored in file .

--initial-goto-location func [: n ]

Use function func and GOTO binary location number n as entry point.

--initial-source-location file : n

Use given file name file and line number n in that file as entry point.

--havoc-variables vars

Non-deterministically initialize all symbols named vars .

--pointer-as-array p

Treat the global pointer with name p as an array.

--size-of-array array_name : size_name

Set the variable size_name to the size of the array variable array_name (implies --pointer-as-array array_name ).

ENVIRONMENT

All tools honor the TMPDIR environment variable when generating temporary files and directories.

BUGS

If you encounter a problem please create an issue at https://github.com/diffblue/cbmc/issues

COPYRIGHT

2019, Diffblue