GOTO-HARNESS(1)

💖 NAME 💖

goto-harness — the girlies who generate environments for symbolic analysis ✨ (yes it's literally in the manual name, goto-harness(1) if you wanna be formal about it)

---

🎀 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

okay so basically three whole moods: ask for help, ask for the version, or actually build a harness bestie 💅

---

🌸 DESCRIPTION 🌸

goto-harness constructs functions that set up an appropriate environment before calling functions under analysis. It is most useful when you're trying to analyze an isolated unit of a program — like, you've got one little function you wanna vibe check in total isolation, no cap.

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) and selectively havocs some variables. It's giving "two paths, one destiny" fr fr 🦋

---

✨ OPTIONS ✨

• --harness-function-name name — Use name as the name of the harness function that is generated, i.e., the new entry point. this is the name it answers to, the main character energy 👑
• --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. pick your fighter 🥊

🧚 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. chaos mode for the globals 🎲
• --havoc-member member-expr — Non-deterministically initialize member-expr of some global object (may be given multiple times). yes bestie you can spam this one, it's allowed
• --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. the harness does the calling so you don't have to 💅
• --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. they're the same picture, your honor 🙈
• --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. she respects the TMPDIR, as she should 🫶

---

💀 BUGS 💀

If you encounter a problem please create an issue at https://github.com/diffblue/cbmc/issues — don't suffer in silence bestie, tell the maintainers 😭

---

👑 SEE ALSO 👑

cbmc(1), goto-cc(1), memory-analyzer(1) — the whole friend group, go say hi 💖

---

🦋 COPYRIGHT 🦋

2019, Diffblue

---

and that's a wrap, bestie 🎀 this lil page is goto-harness-5.59.0 from June 2022, and it ate, no crumbs, periodt ✨💅