GOTO-HARNESS(1) User Commands GOTO-HARNESS(1)

# [NAME](#NAME)

goto-harness - Generate environments for symbolic analysis

# [SYNOPSIS](#SYNOPSIS)

[**goto-harness \[-?\] \[-h\] \[--help\]**](#goto)

show help

[**goto-harness --version**](#goto~2)

show version

[**goto-harness *in* *out* --harness-function-name *name* --harness-type *harness-type* \[harness-options\]**](#goto~3)

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](#DESCRIPTION)

**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)](/man/os/cbmc/memory-analyzer.1) and selectively havocs some variables.

# [OPTIONS](#OPTIONS)

[**--harness-function-name** *name*](#harness)

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**\]](#harness~2)

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](#Common_generator_options)

[**--min-null-tree-depth** *N*](#min)

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-depth** *N*](#max)

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*](#min~2)

Set the minimum size of arrays of non-constant size allocated by the harness to *N*. Defaults to 1.

[**--max-array-size** N](#max~2)

Set the maximum size of arrays of non-constant size allocated by the harness to *N*. Defaults to 2.

[**--nondet-globals**](#nondet)

Set global variables to non-deterministic values in harness.

[**--havoc-member** *member-expr*](#havoc)

Non-deterministically initialize *member-expr* of some global object (may be given multiple times).

[**--function-pointer-can-be-null** *function-name*](#function)

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_harness_generator_%28)

[**--function** *function-name*](#function~2)

Generate an environment to call function *function-name*, which the harness will then call.

[**--treat-pointer-as-array** *p*](#treat)

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

[**--associated-array-size** *array\_name*:*size\_name*](#associated)

Set the function parameter *size\_name* to the size of the array parameter *array\_name* (implies **--treat-pointer-as-array array\_name**).

[**--treat-pointers-equal** *p*,*q*,*r*\[;*s*,*t*\]](#treat~2)

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**](#treat~3)

Function parameter equality is non-deterministic.

[**--treat-pointer-as-cstring** *p*](#treat~4)

Treat the function parameter with the name *p* as a string of characters.

## [Memory snapshot harness generator (**--harness-type initialise-from-memory-snapshot**):](#Memory_snapshot_harness_generator_%28)

[**--memory-snapshot** *file*](#memory)

Initialize memory from JSON memory snapshot stored in *file*.

[**--initial-goto-location** *func*\[:*n*\]](#initial)

Use function *func* and GOTO binary location number *n* as entry point.

[**--initial-source-location** *file*:*n*](#initial~2)

Use given file name *file* and line number *n* in that file as entry point.

[**--havoc-variables** *vars*](#havoc~2)

Non-deterministically initialize all symbols named *vars*.

[**--pointer-as-array** *p*](#pointer)

Treat the global pointer with name *p* as an array.

[**--size-of-array** *array\_name*:*size\_name*](#size)

Set the variable *size\_name* to the size of the array variable *array\_name* (implies **--pointer-as-array array\_name**).

# [ENVIRONMENT](#ENVIRONMENT)

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

# [BUGS](#BUGS)

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

# [SEE ALSO](#SEE_ALSO)

[**cbmc**(1)](/man/os/cbmc/cbmc.1), [**goto-cc**(1)](/man/os/cbmc/goto-cc.1), [**memory-analyzer**(1)](/man/os/cbmc/memory-analyzer.1)

# [COPYRIGHT](#COPYRIGHT)

2019, Diffblue

June 2022 goto-harness-5.59.0

---

Document: goto-harness(1) from cbmc 6.11.0-r0 (Chainguard OS)