Scroll to navigation

GOTO-HARNESS(1) User Commands GOTO-HARNESS(1)

NAME

goto-harness - Generate environments for symbolic analysis

SYNOPSIS

show help
show version
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

Use name as the name of the harness function that is generated, i.e., the new entry point.
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

Set the minimum level at which a pointer can first be NULL in a recursively non-deterministically initialized struct to N. Defaults to 1.
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.
Set the minimum size of arrays of non-constant size allocated by the harness to N. Defaults to 1.
Set the maximum size of arrays of non-constant size allocated by the harness to N. Defaults to 2.
Set global variables to non-deterministic values in harness.
Non-deterministically initialize member-expr of some global object (may be given multiple times).
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):

Generate an environment to call function function-name, which the harness will then call.
Treat the (pointer-typed) function parameter with name p as an array.
Set the function parameter size_name to the size of the array parameter array_name (implies --treat-pointer-as-array array_name).
Assume the pointer-typed function parameters q and r are equal to parameter p, and s equal to t, and so on.
Function parameter equality is non-deterministic.
Treat the function parameter with the name p as a string of characters.

Memory snapshot harness generator (--harness-type initialise-from-memory-snapshot):

Initialize memory from JSON memory snapshot stored in file.
Use function func and GOTO binary location number n as entry point.
Use given file name file and line number n in that file as entry point.
Non-deterministically initialize all symbols named vars.
Treat the global pointer with name p as an array.
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

SEE ALSO

cbmc(1), goto-cc(1), memory-analyzer(1)

COPYRIGHT

2019, Diffblue

June 2022 goto-harness-5.59.0