Add goto-harness man page

This was built using help2man and then manually expanded. In the process
of preparing it, several errors in existing goto-harness documentation
were found and fixed as well.

Author: tautschnig

doc/man/goto-harness.1

@@ -0,0 +1,133 @@
+.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|\fBinitialise-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\R:\fIn\fR
+Use given file name \fIfile\fR and line number \fIn\R 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

doc/man/goto-harness.1

@@ -111,7 +111,7 @@ void memory_snapshot_harness_generatort::validate_options(
   {
     throw invalid_command_line_argument_exceptiont(
       "option --memory_snapshot is required",
-      "--harness-type initialise-from-memory-snapshot");
+      "--harness-type initialise-with-memory-snapshot");
   }
 
   if(initial_source_location_line.empty() == initial_goto_location_line.empty())

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -33,7 +33,7 @@ Author: Diffblue Ltd.
 // clang-format off
 #define MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP                                 \
   "memory snapshot harness generator (--harness-type\n"                        \
-  "  initialise-from-memory-snapshot)\n\n"                                     \
+  "  initialise-with-memory-snapshot)\n\n"                                     \
   "--" MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT " <file>      initialise memory "  \
   "from JSON memory snapshot\n"                                                \
   "--" MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT " <func[:<n>]>\n"          \