.TH GOTO-HARNESS "1" "June 2022" "goto-harness-5.59.0" "User Commands"
.SH NAME
goto-harness \- Generate environments for symbolic analysis
.SH SYNOPSIS
.TP
.B goto\-harness [\-?] [\-h] [\-\-help]
show help
.TP
.B goto\-harness \fB\-\-version\fR
show version
.TP
.B goto\-harness \fIin\fB \fIout\fB \-\-harness\-function\-name\ \fIname\fB \-\-harness\-type \fIharness\-type\fR [\fBharness-options\fR]
build harness for \fIin\fR and write harness to \fIout\fR; the harness is
printed as C code, if \fIout\fR has a .c suffix, else a GOTO binary including
the harness is generated
.SH DESCRIPTION
\fBgoto\-harness\fR 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.
.PP
A typical sequence of tool invocations is
as follows. Given a C program \fIprogram.c\fR, we generate a harness for
function \fItest_function\fR:
.EX
.IP
# 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
.EE
.PP
\fBgoto\-harness\fR 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
\fBgoto\-harness\fR loads an existing program state as generated by
\fBmemory-analyzer\fR(1) and selectively havocs some variables.
.SH OPTIONS
.TP
\fB\-\-harness\-function\-name\fR \fIname\fR
Use \fIname\fR as the name of the harness function that is generated, i.e., the
new entry point.
.TP
\fB\-\-harness\-type\fR [\fBcall-function\fR|\fBinitialize-with-memory-snapshot\fR]
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.
.SS "Common generator options"
.TP
\fB\-\-min\-null\-tree\-depth\fR \fIN\fR
Set the minimum level at which a pointer can first be \fBNULL\fR
in a recursively non-deterministically initialized struct to \fIN\fR. Defaults
to 1.
.TP
\fB\-\-max\-nondet\-tree\-depth\fR \fIN\fR
Set the maximum height of the non-deterministic object tree to \fIN\fR. At that
level, all pointers will be set to \fBNULL\fR. Defaults to 2.
.TP
\fB\-\-min\-array\-size\fR \fIN\fR
Set the minimum size of arrays of non-constant size allocated by the harness to
\fIN\fR. Defaults to 1.
.TP
\fB\-\-max\-array\-size\fR N
Set the maximum size of arrays of non-constant size allocated by the harness to
\fIN\fR. Defaults to 2.
.TP
\fB\-\-nondet\-globals\fR
Set global variables to non-deterministic values in harness.
.TP
\fB\-\-havoc\-member\fR \fImember\-expr\fR
Non-deterministically initialize \fImember\-expr\fR of some global object (may
be given multiple times).
.TP
\fB\-\-function\-pointer\-can\-be\-null\fR \fIfunction\-name\fR
Name of parameters of the target function or of global variables of
function-pointer type that can non-deterministically be set to \fBNULL\fR.
.SS "Function harness generator (\fB\-\-harness\-type call-function\fR):"
.TP
\fB\-\-function\fR \fIfunction\-name\fR
Generate an environment to call function \fIfunction\-name\fR, which the harness
will then call.
.TP
\fB\-\-treat\-pointer\-as\-array\fR \fIp\fR
Treat the (pointer-typed) function parameter with name \fIp\fR as an array.
.TP
\fB\-\-associated\-array\-size\fR \fIarray_name\fR:\fIsize_name\fR
Set the function parameter \fIsize_name\fR to the size of the array parameter
\fIarray_name\fR (implies \fB\-\-treat\-pointer\-as\-array \fIarray_name\fR).
.TP
\fB\-\-treat\-pointers\-equal\fR \fIp\fR,\fIq\fR,\fIr\fR[;\fIs\fR,\fIt\fR]
Assume the pointer-typed function parameters \fIq\fR and \fIr\fR are equal to
parameter \fIp\fR, and \fIs\fR equal to \fIt\fR, and so on.
.TP
\fB\-\-treat\-pointers\-equal\-maybe\fR
Function parameter equality is non\-deterministic.
.TP
\fB\-\-treat\-pointer\-as\-cstring\fR \fIp\fR
Treat the function parameter with the name \fIp\fR as a string of characters.
.SS "Memory snapshot harness generator (\fB\-\-harness\-type initialise\-from\-memory\-snapshot\fR):"
.TP
\fB\-\-memory\-snapshot\fR \fIfile\fR
Initialize memory from JSON memory snapshot stored in \fIfile\fR.
.TP
\fB\-\-initial\-goto\-location\fR \fIfunc\fR[:\fIn\fR]
Use function \fIfunc\fR and GOTO binary location number \fIn\fR as entry point.
.TP
\fB\-\-initial\-source\-location\fR \fIfile\fR:\fIn\fR
Use given file name \fIfile\fR and line number \fIn\fR in that file as entry
point.
.TP
\fB\-\-havoc\-variables\fR \fIvars\fR
Non-deterministically initialize all symbols named \fIvars\fR.
.TP
\fB\-\-pointer\-as\-array\fR \fIp\fR
Treat the global pointer with name \fIp\fR as an array.
.TP
\fB\-\-size\-of\-array\fR \fIarray_name\fR:\fIsize_name\fR
Set the variable \fIsize_name\fR to the size of the array variable
\fIarray_name\fR (implies \fB\-\-pointer\-as\-array \fIarray_name\fR).
.SH ENVIRONMENT
All tools honor the TMPDIR environment variable when generating temporary
files and directories.
.SH BUGS
If you encounter a problem please create an issue at
.B https://github.com/diffblue/cbmc/issues
.SH SEE ALSO
.BR cbmc (1),
.BR goto-cc (1),
.BR memory-analyzer (1)
.SH COPYRIGHT
2019, Diffblue