---
name: "goto-harness"
section: "1"
platform: "linux"
package: "cbmc"
version: "6.6.0-4"
release: "Debian 13 (Trixie)"
platforms: ["linux"]
url: "https://new.carta.tech/goto-harness"
---

# goto-harness(1)

Generate environments for symbolic analysis

## 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 *harness-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 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)](/memory-analyzer/1.md) 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*. Defaults 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 object (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** *array\_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-memory-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 *array\_name* (implies **--pointer-as-array** *array\_name*).

## ENVIRONMENT

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

## BUGS

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

## SEE ALSO

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

## COPYRIGHT

2019, Diffblue