* *      Goto-Harness 6.11.0 (cbmc-6.11.0-dirty) 64-bit     * *
* *                    Copyright (C) 2019                   * *
* *                      Diffblue Ltd.                      * *
* *                    info@diffblue.com                    * *

Usage:                       Purpose:

 goto-harness [-?] [-h] [--help]  show this help
 goto-harness --version       show version and exit
 goto-harness in out --harness-function-name name --harness-type harness-type [harness options]

  in                          goto binary to read from
  out                         file to write the harness to; the harness is
                              printed as C code, if out has a .c suffix, else a
                              goto binary including the harness is generated
 --harness-function-name name  the name of the harness function to generate
 --harness-type type          one of the harness types listed below

function harness generator (--harness-type call-function):
 --function function_name     the function the harness should call
 --nondet-globals             set global variables to non-deterministic values
                              in harness
 --min-null-tree-depth N      minimum level at which a pointer can first be
                              NULL in a recursively nondet initialized struct
 --max-nondet-tree-depth N    limit size of nondet (e.g. input) object tree; at
                              level N pointers are set to null
 --min-array-size N           minimum size of dynamically created arrays
                              (default: 1)
 --max-array-size N           maximum size of dynamically created arrays
                              (default: 2)
 --function-pointer-can-be-null function_name  name of the function(s) pointer
                              parameters that can be NULL pointing
 --havoc-member member_expr   path to the member to be havocked
 --treat-pointer-as-array p   treat the function parameter with the name p as
                              an array
 --treat-pointers-equal p,q,r[;s,t]  treat the function parameters q,r equal to
                              parameter p; s to t and so on
 --treat-pointers-equal-maybe  function parameters equality is non-deterministic
 --associated-array-size array_name:size_name  set the parameter size_name to
                              the size of the array array_name (implies
                              -- treat-pointer-as-array array_name)
 --treat-pointer-as-cstring p  treat the function parameter with the name p as
                              a string of characters

memory snapshot harness generator (--harness-type
  initialize-with-memory-snapshot):
 --memory-snapshot file       initialize memory from JSON memory snapshot
 --initial-goto-location func[:n]  use given function and location number as
                              entry point
 --initial-source-location file:n  use given file name and line number as entry
                              point
 --havoc-variables vars       initialize variables from vars to
                              non-deterministic values
 --min-null-tree-depth N      minimum level at which a pointer can first be
                              NULL in a recursively nondet initialized struct
 --max-nondet-tree-depth N    limit size of nondet (e.g. input) object tree; at
                              level N pointers are set to null
 --min-array-size N           minimum size of dynamically created arrays
                              (default: 1)
 --max-array-size N           maximum size of dynamically created arrays
                              (default: 2)
 --function-pointer-can-be-null function_name  name of the function(s) pointer
                              parameters that can be NULL pointing
 --havoc-member member_expr   path to the member to be havocked
 --pointer-as-array p         treat the global pointer with the name p as an
                              array
 --size-of-array array_name:size_name  set the parameter size_name to the size
                              of the array array_name (implies
                              -- pointer-as-array array_name)