FreeBSD Manual Pages
GOTO-HARNESS(1) User Commands GOTO-HARNESS(1) NAME goto-harness - Generate environments for symbolic analysis SYNOPSIS goto-harness [-?] [-h] [--help] show help goto-harness --version show version goto-harness in out --harness-function-name name --harness-type har- ness-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 DESCRIPTION goto-harness constructs functions that set up an appropriate environ- ment 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 har- nesses, which automatically synthesize an environment without having any information about the program state. Second, memory-snapshot har- nesses, in which case goto-harness loads an existing program state as generated by memory-analyzer(1) and selectively havocs some variables. OPTIONS --harness-function-name name 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. Common generator options --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. De- faults to 1. --max-nondet-tree-depth N 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-size N 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-member member-expr Non-deterministically initialize member-expr of some global ob- ject (may be given multiple times). --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. Function harness generator (--harness-type call-function): --function function-name Generate an environment to call function function-name, which the harness will then call. --treat-pointer-as-array p Treat the (pointer-typed) function parameter with name p as an array. --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 ar- ray_name). --treat-pointers-equal p,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-cstring p Treat the function parameter with the name p as a string of characters. Memory snapshot harness generator (--harness-type initialise-from-mem- ory-snapshot): --memory-snapshot file Initialize memory from JSON memory snapshot stored in file. --initial-goto-location func[:n] Use function func and GOTO binary location number n as entry point. --initial-source-location file:n Use given file name file and line number n in that file as entry point. --havoc-variables vars Non-deterministically initialize all symbols named vars. --pointer-as-array p Treat the global pointer with name p as an array. --size-of-array array_name:size_name Set the variable size_name to the size of the array variable ar- ray_name (implies --pointer-as-array array_name). ENVIRONMENT All tools honor the TMPDIR environment variable when generating tempo- rary files and directories. BUGS If you encounter a problem please create an issue at https://github.com/diffblue/cbmc/issues SEE ALSO cbmc(1), goto-cc(1), memory-analyzer(1) COPYRIGHT 2019, Diffblue goto-harness-5.59.0 June 2022 GOTO-HARNESS(1)
NAME | SYNOPSIS | DESCRIPTION | OPTIONS | ENVIRONMENT | BUGS | SEE ALSO | COPYRIGHT
Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=goto-harness&sektion=1&manpath=FreeBSD+Ports+15.0>