goto-harness1
Generate environments for symbolic analysis
Usage
- goto-harness [-?] [-h] [--help]
-
goto-harness [-?] [-h] [--help] show help
- goto-harness --version
-
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
Overview
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-type initialise-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.
Releases
2 releases since Debian 11 (Bullseye); the text changed 1 time.
--associated-array-size since Debian 13 (Trixie);
--function-pointer-can-be-null since Debian 13 (Trixie);
--harness-function-name since Debian 13 (Trixie);
--harness-type since Debian 13 (Trixie);
--havoc-member since Debian 13 (Trixie);
--havoc-variables since Debian 13 (Trixie);
--initial-goto-location since Debian 13 (Trixie);
--initial-source-location since Debian 13 (Trixie);
--max-array-size since Debian 13 (Trixie);
--max-nondet-tree-depth since Debian 13 (Trixie);
--memory-snapshot since Debian 13 (Trixie);
--min-array-size since Debian 13 (Trixie);
--min-null-tree-depth since Debian 13 (Trixie);
--nondet-globals since Debian 13 (Trixie);
--pointer-as-array since Debian 13 (Trixie);
--size-of-array since Debian 13 (Trixie);
--treat-pointer-as-array since Debian 13 (Trixie);
--treat-pointer-as-cstring since Debian 13 (Trixie);
--treat-pointers-equal since Debian 13 (Trixie);
--treat-pointers-equal-maybe since Debian 13 (Trixie).
--16 until Debian 11 (Bullseye);
--32 until Debian 11 (Bullseye);
--64 until Debian 11 (Bullseye);
--ILP32 until Debian 11 (Bullseye);
--ILP64 until Debian 11 (Bullseye);
--LLP64 until Debian 11 (Bullseye);
--LP32 until Debian 11 (Bullseye);
--LP64 until Debian 11 (Bullseye);
--all-properties until Debian 11 (Bullseye);
--arch until Debian 11 (Bullseye);
--arrays-uf-always until Debian 11 (Bullseye);
--arrays-uf-never until Debian 11 (Bullseye);
--beautify-greedy until Debian 11 (Bullseye);
--big-endian until Debian 11 (Bullseye);
--boolector until Debian 11 (Bullseye);
--bounds-check until Debian 11 (Bullseye);
--cover-assertions until Debian 11 (Bullseye);
--cvc3 until Debian 11 (Bullseye);
--cvc4 until Debian 11 (Bullseye);
--depth until Debian 11 (Bullseye);
--dimacs until Debian 11 (Bullseye);
--div-by-zero-check until Debian 11 (Bullseye);
--dump-c until Debian 11 (Bullseye);
--error-label until Debian 11 (Bullseye);
--isr until Debian 11 (Bullseye);
--little-endian until Debian 11 (Bullseye);
--mathsat until Debian 11 (Bullseye);
--mmio until Debian 11 (Bullseye);
--nan-check until Debian 11 (Bullseye);
--no-arch until Debian 11 (Bullseye);
--no-assertions until Debian 11 (Bullseye);
--no-assumptions until Debian 11 (Bullseye);
--no-library until Debian 11 (Bullseye);
--no-pretty-names until Debian 11 (Bullseye);
--no-unwinding-assertions until Debian 11 (Bullseye);
--nondet-static until Debian 11 (Bullseye);
--nondet-volatile until Debian 11 (Bullseye);
--os until Debian 11 (Bullseye);
--outfile until Debian 11 (Bullseye);
--pointer-check until Debian 11 (Bullseye);
--preprocess until Debian 11 (Bullseye);
--program-only until Debian 11 (Bullseye);
--property until Debian 11 (Bullseye);
--refine until Debian 11 (Bullseye);
--round-to-minus-inf until Debian 11 (Bullseye);
--round-to-nearest until Debian 11 (Bullseye);
--round-to-plus-inf until Debian 11 (Bullseye);
--round-to-zero until Debian 11 (Bullseye);
--show-goto-functions until Debian 11 (Bullseye);
--show-loops until Debian 11 (Bullseye);
--show-properties until Debian 11 (Bullseye);
--show-symbol-table until Debian 11 (Bullseye);
--show-vcc until Debian 11 (Bullseye);
--signed-overflow-check until Debian 11 (Bullseye);
--slice-formula until Debian 11 (Bullseye);
--smt2 until Debian 11 (Bullseye);
--unsigned-char until Debian 11 (Bullseye);
--unsigned-overflow-check until Debian 11 (Bullseye);
--unwind until Debian 11 (Bullseye);
--unwindset until Debian 11 (Bullseye);
--yices until Debian 11 (Bullseye);
--z3 until Debian 11 (Bullseye);
-D until Debian 11 (Bullseye);
-I until Debian 11 (Bullseye).