* * 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)
Options (21)
| Option | Description | Source |
|---|---|---|
--harness-function-name name | Use name as the name of the harness function that is generated, i.e., the new entry point. | help + man |
--harness-type type | one of the harness types listed below | help |
--function function_name | Generate an environment to call function function-name, which the harness will then call. | help + man |
--nondet-globals | Set global variables to non-deterministic values in harness. | help + man |
--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. | help + man |
--max-nondet-tree-depth N | Set the maximum height of the non-deterministic object tree to N. | help + man |
--min-array-size N | Set the minimum size of arrays of non-constant size allocated by the harness to N. | help + man |
--max-array-size N | Set the maximum size of arrays of non-constant size allocated by the harness to N. | help + man |
--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. | help + man |
--havoc-member member_expr | Non-deterministically initialize member-expr of some global object (may be given multiple times). | help + man |
--treat-pointer-as-array p | Treat the (pointer-typed) function parameter with name p as an array. | help + man |
--treat-pointers-equal p | treat the function parameters q,r equal to parameter p; | help |
--treat-pointers-equal-maybe | function parameters equality is non-deterministic | help + man |
--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). | help + man |
--treat-pointer-as-cstring p | Treat the function parameter with the name p as a string of characters. | help + man |
--memory-snapshot file | Initialize memory from JSON memory snapshot stored in file. | help + man |
--initial-goto-location func[:n | use given function and location number as entry point | help |
--initial-source-location file:n | Use given file name file and line number n in that file as entry point. | help + man |
--havoc-variables vars | initialize variables from vars to non-deterministic values | help + man |
--pointer-as-array p | treat the global pointer with the name p as an array | help + man |
--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). | help + man |