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

goto-harness - Generate environments for symbolic analysis

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

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.

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.

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.

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.

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

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

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

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

2019, Diffblue

June 2022 goto-harness-5.59.0