goto-harness - Generate environments for symbolic analysis

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

       2019, Diffblue

goto-harness-5.59.0                                 June 2022                                    GOTO-HARNESS(1)

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.

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

       goto-harness - Generate environments for symbolic analysis

--harness-function-namename
              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.

   Commongeneratoroptions--min-null-tree-depthN
              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-depthN
              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-sizeN
              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-membermember-expr
              Non-deterministically initialize member-expr of some global object (may be given multiple times).

       --function-pointer-can-be-nullfunction-name
              Name of parameters of the target function or of global variables of function-pointer type that can
              non-deterministically be set to NULL.

   Functionharnessgenerator(--harness-typecall-function):
       --functionfunction-name
              Generate an environment to call function function-name, which the harness will then call.

       --treat-pointer-as-arrayp
              Treat the (pointer-typed) function parameter with name p as an array.

       --associated-array-sizearray_name:size_name
              Set the function parameter size_name to the  size  of  the  array  parameter  array_name  (implies
              --treat-pointer-as-arrayarray_name).

       --treat-pointers-equalp,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-cstringp
              Treat the function parameter with the name p as a string of characters.

   Memorysnapshotharnessgenerator(--harness-typeinitialise-from-memory-snapshot):
       --memory-snapshotfile
              Initialize memory from JSON memory snapshot stored in file.

       --initial-goto-locationfunc[:n]
              Use function func and GOTO binary location number n as entry point.

       --initial-source-locationfile:n
              Use given file name file and line number n in that file as entry point.

       --havoc-variablesvars
              Non-deterministically initialize all symbols named vars.

       --pointer-as-arrayp
              Treat the global pointer with name p as an array.

       --size-of-arrayarray_name:size_name
              Set  the  variable  size_name  to  the  size   of   the   array   variable   array_name   (implies
              --pointer-as-arrayarray_name).

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

goto-harness[-?][-h][--help]
              show help

       goto-harness--version
              show version

       goto-harnessinout--harness-function-namename--harness-typeharness-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