GOTO-INSTRUMENT(1)

📦
version 6.8.0 · 4 versions
, in fedora 44, nixos 26.05, nixpkgs unstable

🦋 GOTO-INSTRUMENT(1) 🦋

okay bestie, welcome to the goto-instrument page, section 1 of the User Commands manual. buckle up, she's a long one 💅

✨ NAME ✨

goto-instrument — do analysis stuff or instrumentation stuff on goto binaries 🎀

✨ SYNOPSIS ✨

goto-instrument [-?] [-h] [--help]
       show help

goto-instrument --version
       show version and exit

goto-instrument [options] in [out]
       perform analysis or instrumentation

so basically: no input file = you're just asking for help or the version. give it an in and she does the thing. 🌸

✨ DESCRIPTION ✨

goto-instrument reads a GOTO binary, does whatever program transformation you asked for, and then writes the resulting program back out to disk as a GOTO binary. that's the whole vibe. no cap. 🦋

✨ OPTIONS ✨

🌈 Dump Source 🌈

  • --dump-c — spit out C source, bestie ✨
  • --dump-c-type-header m — generate a C header for the types that are local in m
  • --dump-cpp — spit out C++ source instead
  • --no-system-headers — generate C source but expand the libc includes
  • --use-all-headers — generate C source with all the includes, go big
  • --harness — include the input generator in the output 🫶
  • --horn — print the program as constrained horn clauses

🩺 Diagnosis 🩺

  • --show-properties — show the properties but don't run the analysis, we're just looking
  • --document-properties-html — generate HTML property documentation 📄
  • --document-properties-latex — generate Latex property documentation 📄
  • --show-symbol-table — show the loaded symbol table
  • --list-symbols — list symbols with their type info
  • --show-goto-functions — show the loaded goto program
  • --list-goto-functions — list the loaded goto functions
  • --count-eloc — count effective lines of code (eloc my beloved)
  • --list-eloc — list the full path names of the lines containing code
  • --print-global-state-size — count the total number of bits of global objects
  • --print-path-lengths — print statistics about the paths in the control-flow graph
  • --show-locations — show all the source locations
  • --dot — generate the CFG graph in DOT format 🔥
  • --print-internal-representation — show the verbose internal representation of the program
  • --list-undefined-functions — list the functions that have no body
  • --list-calls-args — list every function call with its arguments
  • --call-graph — show the graph of function calls
  • --reachable-call-graph — show the graph of function calls that are potentially reachable from the main function
  • --show-class-hierarchy — show the class hierarchy 👑
  • --validate-goto-model — turn on extra well-formedness checks on the goto program
  • --validate-ssa-equation — turn on extra well-formedness checks on the SSA representation
  • --validate-goto-binary — check that the GOTO binary you passed in is well-formed, then dip
  • --interpreter — do concrete execution

🌊 Data-flow analyses 🌊

  • --show-struct-alignment — show the struct members that might be accessed concurrently
  • --show-threaded — show the instructions that may be executed by more than one thread
  • --show-local-safe-pointers — show pointer expressions that are trivially dominated by a not-null check
  • --show-safe-dereferences — show pointer expressions that are trivially dominated by a not-null check and used as a dereference operand
  • --show-value-sets — show points-to information (using value sets)
  • --show-global-may-alias — show may-alias information over globals
  • --show-local-bitvector-analysis — show the procedure-local pointer analysis
  • --escape-analysis — perform escape analysis
  • --show-escape-analysis — show the results of escape analysis
  • --custom-bitvector-analysis — perform configurable bitvector analysis
  • --show-custom-bitvector-analysis — show the results of configurable bitvector analysis
  • --interval-analysis — perform interval analysis
  • --show-intervals — show the results of interval analysis
  • --show-uninitialized — show the maybe-uninitialized variables
  • --show-points-to — show points-to information
  • --show-rw-set — show read-write sets
  • --show-call-sequences — show function call sequences
  • --show-reaching-definitions — show reaching definitions
  • --show-dependence-graph — show the program-dependence graph
  • --show-sese-regions — show single-entry-single-exit regions

🛡️ Safety checks 🛡️

  • --no-assertions — ignore user assertions 🙈
  • --bounds-check — enable array bounds checks
  • --pointer-check — enable pointer checks
  • --memory-leak-check — enable memory leak checks
  • --memory-cleanup-check — enable memory cleanup checks: assert that all dynamically allocated memory is explicitly freed before the program terminates 🧹
  • --div-by-zero-check — enable division by zero checks for integer division
  • --float-div-by-zero-check — enable division by zero checks for floating-point division
  • --signed-overflow-check — enable signed arithmetic over- and underflow checks
  • --unsigned-overflow-check — enable arithmetic over- and underflow checks
  • --pointer-overflow-check — enable pointer arithmetic over- and underflow checks
  • --conversion-check — check whether values can still be represented after a type cast
  • --undefined-shift-check — check for a shift greater than the bit-width
  • --float-overflow-check — check floating-point for +/-Inf
  • --nan-check — check floating-point for NaN
  • --enum-range-check — check that all enum type expressions have values inside the enum range
  • --pointer-primitive-check — check that all pointers in pointer primitives are valid or null
  • --retain-trivial-checks — include the checks that are trivially true
  • --error-label label — check that label is unreachable
  • --no-built-in-assertions — ignore assertions in the built-in library
  • --no-assertions — ignore user assertions (yes bestie, she's listed twice in the original, i'm not making the rules 💀)
  • --no-assumptions — ignore user assumptions
  • --assert-to-assume — convert user assertions into assumptions
  • --uninitialized-check — add checks for uninitialized locals (experimental, so like, be aware ⚠️)
  • --stack-depth n — add a check that the call stack size of non-inlined functions never exceeds n
  • --race-check — add floating-point data race checks

🔮 Semantic transformations 🔮

  • --nondet-volatile
  • --nondet-volatile-variable variable

so here's the tea 🍵: by default, cbmc(1) treats volatile variables exactly the same as non-volatile variables. meaning it assumes a volatile variable does not change between subsequent reads, unless the program itself wrote to it. with the options above, you can tell goto-instrument to instrument the given goto program so that either (1) reads from all volatile expressions become non-deterministic (--nondet-volatile), (2) reads from specific variables become non-deterministic (--nondet-volatile-variable), or (3) reads from specific variables get modelled by given models (--nondet-volatile-model).

and now, two usage examples, because she ate and left no crumbs ✨ consider the following test, for the function get_celsius and with the harness test_get_celsius:

#include <assert.h>
#include <limits.h>
#include <stdint.h>

// hardware sensor for temperature in kelvin
extern volatile uint16_t temperature;

int get_celsius() {
  if (temperature > (1000 + 273)) {
    return INT_MIN; // value indicating error
  }
  return temperature - 273;
}

void test_get_celsius() {
  int t = get_celsius();
  assert(t == INT_MIN || t <= 1000);
  assert(t == INT_MIN || t >= -273);
}

here the variable temperature is basically a hardware sensor 📡 it returns the current temperature on each read. get_celsius converts the value from Kelvin into degrees Celsius, assuming the value is in the expected range. but — and this is the plot twist — it has a bug where it reads temperature a second time after the check, which may yield a value for which the check would not succeed 😭 verifying this program as-is with cbmc(1) would give you a verification success, which is a lie. so we use goto-instrument to make reads from temperature non-deterministic:

goto-cc -o get_celsius_test.gb get_celsius_test.c
goto-instrument --nondet-volatile-variable temperature \
  get_celsius_test.gb get_celsius_test-mod.gb
cbmc --function test_get_celsius get_celsius_test-mod.gb

and now the final invocation of cbmc(1) correctly reports a verification failure. slay. caught the bug. 🔥

  • --nondet-volatile-model variable:model

ngl, simply treating volatile variables as non-deterministic can be too inaccurate for some use cases. so consider this next test, for the function get_message and with the harness test_get_message:

#include <assert.h>
#include <stdint.h>

extern volatile uint32_t clock;

typedef struct message {
  uint32_t timestamp;
  void *data;
} message_t;

void *read_data();

message_t get_message() {
  message_t msg;
  msg.timestamp = clock;
  msg.data = read_data();
  return msg;
}

void test_get_message() {
  message_t msg1 = get_message();
  message_t msg2 = get_message();
  assert(msg1.timestamp <= msg2.timestamp);
}

the harness verifies that get_message assigns non-decreasing timestamps to the returned messages ⏰ but just treating clock as non-deterministic would not be enough to prove this property. so instead, we can supply a model for reads from clock:

// model for reads of the variable clock
uint32_t clock_read_model() {
  static uint32_t clock_value = 0;
  uint32_t increment;
  __CPROVER_assume(increment <= 100);
  clock_value += increment;
  return clock_value;
}

this model is stateful — it keeps the current clock value between invocations in the variable clock_value. on each invocation it increments the clock by a non-deterministic value in the range 0 to 100. and we can tell goto-instrument to use the model clock_read_model for reads from the variable clock as follows:

goto-cc -o get_message_test.gb get_message_test.c
goto-instrument --nondet-volatile-model clock:clock_read_model \
  get_message_test.gb get_message_test-mod.gb
cbmc --function get_message_test get_message_test-mod.gb

and boom — that final cbmc(1) run now reports verification success 🎉 like it's supposed to.

  • --isr function — instruments an interrupt service routine ✨
  • --mmio — instruments memory-mapped I/O 💅
  • --nondet-static — adds nondeterministic initialization for variables with static lifetime (yes bestie, the static ones get the ✨nondet✨ treatment)
  • --nondet-static-exclude e — exactly the same as nondet-static except it skips the variable e (use it multiple times if you need to, she's flexible 💖)
  • --nondet-static-matching r — adds nondeterministic initialization for variables with static lifetime that match the regex r
  • --function-enter f, --function-exit f, --branch f — instruments a call to f at the beginning, at the exit, or at a branch point, respectively 🎀
  • --splice-call caller,callee — prepends a call to callee inside the body of caller
  • --check-call-sequence seq — instruments checks that assert every call sequence matches seq 👑
  • --undefined-function-is-assume-false — converts each call to an undefined function into assume(false)
  • --insert-final-assert-false function — generates assert(false) at the end of function 🫶
  • --generate-function-body regex — this transformation inserts implementations of functions that don't have a definition, i.e. it gives them a body. What that generated body actually does is chosen with the --generate-function-body-options option:
  • --generate-function-body-options option — one of assert-false, assume-false, nondet-return, assert-false-assume-false and havoc[,params:regex][,globals:regex][,params:p_n1;p_n2;..] (default: nondet-return)
    • assert-false: the body is a single command: assert(0).
    • assume-false: the body is a single command: assume(0).
    • assert-false-assume-false: two commands, exactly as above.
    • nondet-return: the generated function returns a non-deterministic value of its return type.
    • havoc[,params:p-regex][,globals:g-regex]: assigns non-deterministic values to the targets of pointer-to-non-constant parameters matching the regular expression p-regex, and to non-constant globals matching g-regex, and then (if it's a non-void function) returns like nondet-return does. Here's an example showing it off:
// main.c
int global;
const int c_global;
int function(int *param, const int *c_param);

okay so a lot of the time we want to not overwrite internal symbols, i.e. the ones with an __ prefix, and that's what the pattern (?!__) is for 😌

goto-cc main.c -o main.gb
goto-instrument main.gb main-out.gb \
  --generate-function-body-options 'havoc,params:(?!__).*,globals:(?!__).*' \
  --generate-funtion-body function

This gives you a GOTO binary equivalent to the following C code:

// main-mod.c
int function(int *param, const int *c_param) {
  *param = nondet_int();
  global = nondet_int();
  return nondet_int();
}

The parameters that should get non-deterministically updated can be picked either with a regular expression (like above) or with a semicolon-separated list of their numbers. For example havoc,params:0;3;4 assigns non-deterministic values to the first, fourth, and fifth parameter 💫

Heads up bestie: only parameters of pointer type can be havoced, and goto-instrument will produce an error report if you hand it a parameter number that belongs to a non-pointer parameter. Asking to havoc a parameter whose number is higher than the number of parameters that function takes will also give you an error report. No cap 🚨
  • --generate-havocing-body option fun_name,params:p_n1;p_n2;..
  • --generate-havocing-body option fun_name[,call-site-id,params:p_n1;p_n2;..>]+ — requests a different implementation for a bunch of call-sites of a single function. The --generate-havocing-body option inserts brand new functions for the selected call-sites and swaps the calls to the original function out for calls to the respective new functions 🌈
// main.c
int function(int *first, int *second, int *third);

int main() {
  int a = 10;
  int b = 10;
  int c = 10;
  function(&a, &b, &c);
  function(&a, &b, &c);
}

You can specify different behaviour for each call-site like this:

goto-cc main.c -o main.gb
goto-instrument main.gb  main-mod.gb \
  --generate-havocing-body 'function,1,params:0;2,2,params:1'

which results in a GOTO binary equivalent to:

// main-mod.c
int function_1(int *first, int *second, int *third) {
  *first = nondet_int();
  *third = nondet_int();
}

int function_2(int *first, int *second, int *third) { *second = nondet_int(); }

int main() {
  int a = 10;
  int b = 10;
  int c = 10;
  function_1(&a, &b, &c);
  function_2(&a, &b, &c);
}
  • --restrict-function-pointer *pointer_name/target[,targets]** — replaces function pointers with a user-defined set of targets. You might need this when --remove-function-pointers creates too large a set of direct calls. Think about the example that was presented for --remove-function-pointers. Say that call will always receive pointers to either f or g during actual executions of the program, and symbolic execution for h is just way too expensive to simply ignore the cost of its branch 💸

To make this controlled replacement possible, we label the places in each function where function pointers get called, using this pattern:

function-name.function_pointer_call.N

where N refers to the N-th function call via a function pointer inside function-name, i.e. the first call to a function pointer in a function has N=1, the fifth has N=5, etc. Alternatively, if the calls carry labels in the source code, we can also refer to a function pointer as

function-name.label

So to implement the assumption that the first call to a function pointer in call can only ever be a call to f or g, use:

goto-instrument --restrict-function-pointer \
  call.function_pointer_call.1/f,g in.gb out.gb

The resulting output (written to the GOTO binary out.gb) looks similar to the original example, except now there won't be a call to h:

void call(fptr_t fptr) {
  int r;
  if (fptr == &f) {
    r = f(10);
  } else if (fptr == &g) {
    r = g(10);
  } else {
    // sanity check
    assert(false);
    assume(false);
  }
  return r;
}

okay another example — imagine we have a simple virtual filesystem API and implementation like this:

typedef struct filesystem_t filesystem_t;
struct filesystem_t {
  int (*open)(filesystem_t *filesystem, const char *file_name);
};

int fs_open(filesystem_t *filesystem, const char *file_name) {
  filesystem->open(filesystem, file_name);
}

int nullfs_open(filesystem_t *filesystem, const char *file_name) { return -1; }

filesystem_t nullfs_val = {.open = nullfs_open};
filesystem *const nullfs = &nullfs_val;

filesystem_t *get_fs_impl() {
  // some fancy logic to determine
  // which filesystem we're getting -
  // in-memory, backed by a database, OS file system
  // - but in our case, we know that
  // it always ends up being nullfs
  // for the cases we care about
  return nullfs;
}
int main(void) {
  filesystem_t *fs = get_fs_impl();
  assert(fs_open(fs, "hello.txt") != -1);
}

In this case the assumption is that inside function main, fs can be nothing other than nullfs. But maybe the logic is too complicated and symbolic execution just can't figure that out, so in the call to fs_open we end up branching on every function matching the signature of filesystem_t::open — which could be quite a few functions across the program 😭 And worst of all: if its address is ever taken anywhere in the program, then as far as function pointer removal via --remove-function-pointers is concerned, it could be fs_open itself, since it has a matching signature. That forces symbolic execution to follow a potentially infinite recursion until its unwind limit 💀

So in this case we can once again restrict the function pointer to the value we know it will have:

goto-instrument --restrict-function-pointer \
  fs_open.function_pointer_call.1/nullfs_open in.gb out.gb
  • --function-pointer-restrictions-file file_name — if you've got a lot of places where you want to restrict function pointers, typing them all out on the command line would be such a nuisance 🙈 In those cases you can pass a file to load the restrictions from instead, and you can hand it the name of a JSON file in this format:
{
  "function_call_site_name": ["function1", "function2", ...],
   ...
}

If you pass in multiple files, or a mix of files and command line restrictions, the final restrictions will be the set union of every restriction you specified 🫶

Note that if something goes wrong during type checking (i.e. making sure that all function pointer replacements refer to functions in the symbol table that have the correct type), the error message will refer to the command line option --restrict-function-pointer regardless of whether the restriction in question actually came from the command line or from a file. Slightly confusing, but that's the vibe ✨
  • --restrict-function-pointer-by-name symbol_name/target[,targets]* — okay so you literally just tell it which function pointers to keep, by unmangled name, and it does the restricting before it goes labeling function pointers. Very demure, very mindful. 💅
  • --remove-calls-no-body — if a function has no body, the calls to it just ✨vanish✨. No body, no calls, no problem.
  • --add-library — sprinkles in models of C library functions so your analysis isn't out here guessing what printf does. 🎀
  • --malloc-may-fail — lets malloc calls return a null pointer. Yes bestie, it can just fail on you. Character development.
  • --malloc-fail-assert — sets malloc failure mode to assert-then-assume. It's giving "assert it, then assume it."
  • --malloc-fail-null — sets malloc failure mode to return null. Straight up, no chaser.
  • --no-malloc-may-fail — do not let malloc calls fail by default. The paranoid setting, lowkey.
  • --string-abstraction — tracks C string lengths and zero-termination. She's keeping receipts on your strings, fr fr. 🧵
  • --dfcc-debug-lib — turns on debug assertions in the cprover contracts library. Debug girlies rise up. 🐛
  • --dfcc-simple-invalid-pointer-model — uses the simplified invalid pointer model in the cprover contracts library. It's faster but unsound, so like... be aware, bestie. Speed vs. correctness is the eternal vibe check.
  • --model-argc-argv n — creates up to n non-deterministic C strings as entries to argv and sets argc accordingly. If you don't model this, argv is just left uninitialized except for a terminating NULL pointer, which is not the moment. Consider this lil example:
// needs_argv.c
#include <assert.h>

int main(int argc, char *argv[]) {
  if (argc >= 2)
    assert(argv[1] != 0);

  return 0;
}

If cbmc(1) is run directly on this example, it'll report a failing assertion because nobody modeled argv. Rude. To make the assertion succeed, as expected, you do:

goto-cc needs_argv.c
goto-instrument --model-argc-argv 2 a.out a.out
cbmc a.out

Slay. ✨

  • --remove-function-body f — removes the implementation of function f. (may be repeated, so go off, remove as many as you want)
  • --remove-function-body-regex regex — removes the implementation of every function matching the regular expression regex. Regex girlies, this one's for you. 🦋
  • --replace-calls f:g — replaces calls to f with calls to g. Swapping out the whole personality.
  • --max-nondet-tree-depth N — limits the size of the nondet (like, input) object tree. At level N, pointers get set to null. Draws the line.
  • --min-null-tree-depth N — sets the minimum level at which a pointer can first be NULL in a recursively nondet initialized struct. So it can't be null before level N, no cap.

✨ Semantics-preserving transformations: ✨

These ones keep the meaning but change the shape. Glow-up, not rewrite. 💖

  • --ensure-one-backedge-per-target — transforms loop bodies so there's a single edge back to the loop head. One backedge. That's it. That's the whole vibe.
  • --drop-unused-functions — drops functions that are trivially unreachable from the main function. If nobody can get to you, you're out. 👋
  • --remove-pointers — converts pointer arithmetic into base+offset expressions. Pointers hate to see her coming.
  • --constant-propagator — propagates constants and simplifies expressions. She's simplifying. She's streamlining. She's iconic. 👑
  • --inline — performs full inlining. Go big or go home.
  • --partial-inline — performs partial inlining. The ✨curated✨ version.
  • --function-inline function — transitively inlines all calls function makes. It's giving full commitment.
  • --no-caching — disables caching of intermediate results during transitive function inlining. Yes it's slower, no we don't care.
  • --log file — logs, in JSON format, which code segments were inlined. Use it with --function-inline. Receipts, but make them machine-readable. 📝
  • --remove-function-pointers — resolves calls through function pointers into direct function calls. Candidate functions get chosen based on their signature and whether or not their address is taken somewhere in the program. Here's the approach in action: say you've got these signatures available in the program:
int f(int x);
int g(int x);
int h(int x);

And you have a call site like this:

typedef int (*fptr_t)(int x);
void call(fptr_t fptr) {
  int r = fptr(10);
  assert(r > 0);
}

Function pointer removal will turn that into code similar to this:

void call(fptr_t fptr) {
  int r;
  if (fptr == &f) {
    r = f(10);
  } else if (fptr == &g) {
    r = g(10);
  } else if (fptr == &h) {
    r = h(10);
  } else {
    // sanity check
    assert(false);
    assume(false);
  }
  return r;
}
Beware bestie!! There may be many functions matching a particular signature, and some of them may be costly for a later analysis to deal with. Consider using --restrict-function-pointer to manually specify the set of functions, or --value-set-fi-fp-removal. Protect your runtime. 🫶
  • --remove-const-function-pointers — removes function pointers that are constant, or a constant part of an array. Constants get the ✂️.
  • --value-set-fi-fp-removal — builds a flow-insensitive value set and swaps function pointers for a case statement over the possible assignments. If that set of possible assignments is empty, the function pointer gets removed using the standard --remove-function-pointers pass. No assignments, no pointer, periodt.

🌈 Loop information and transformations: 🌈

  • --show-loops — shows the loops in the program. Just... shows them. Look at them. 👀
  • --unwind nr — unwinds all loops nr times. All of them. Every last one.
  • --unwindset [T:]L:B,... — unwinds loop L with a bound of B, optionally restricted to thread T. Use --show-loops to get the loop IDs, iykyk.
  • --unwindset-file file — reads the unwindset from file. Because typing it all out is a lot. 🫠
  • --partial-loops — permits paths that execute loops only partially (up to the given unwinding bound) and then continue past the loop even when the loop condition would still hold. > Heads up: such paths may be spurious, which results in false alarms. She's a little chaotic. 😭
  • --no-unwinding-assertions — do not generate unwinding assertions. Simple as.
  • --unwinding-assertions — generate unwinding assertions. These are enabled by default, and this overrides --no-unwinding-assertions when both of these are given. She wins the argument. 💅
  • --continue-as-loops — adds a loop for the remaining iterations after the unwound part. Finishing what the unwind started.
  • --k-induction k — checks loops with k-induction. Math girlies, this one's yours.
  • --step-case — k-induction: do step-case.
  • --base-case — k-induction: do base-case. (Yes, they come as a set. Iconic duo.)
  • --havoc-loops — over-approximates all loops. Chaos mode, but make it sound.
  • --accelerate — adds loop accelerators. Vroom vroom, we're going faster than iteration. 🏎️
  • --z3 — use Z3 when computing loop accelerators. Shoutout to Z3. 💜
  • --skip-loops loop-ids — adds gotos to skip selected loops during execution. Yeet those loops.
  • --show-lexical-loops — shows lexical loops. So a lexical loop is a block of goto program instructions with a single entry edge at the top and a single backedge leading from bottom to top, where "top" and "bottom" refer to program order. The loop may have holes: instructions that sit between top and bottom in program order but can't reach the loop backedge. Lexical loops are a subset of the natural loops, which are cheaper to compute and include most natural loops generated from typical C code. Basically the low-effort, high-reward loop detection. ✨
  • --show-natural-loops — shows natural loop heads. A natural loop is when the nodes and edges of a graph make one self-encapsulating circle with no incoming edges from external nodes. For example, A -> B -> C -> D -> A is a natural loop, but if B has an incoming edge from X, then it isn't a natural loop, because X is an external node. Outgoing edges don't affect the natural-ness of a loop. Outgoing? Don't care. Incoming? Now we have beef. 🚫

🧚 Memory model instrumentations: 🧚

  • --mm [tso|pso|rmo|power] — instruments the program so it can be verified against different weak memory models, using a model-checker that verifies sequentially consistent programs. Weak memory models are the plot twist. 🌀
  • --scc — detects critical cycles per SCC (one thread per SCC). Every thread gets its own little SCC kingdom. 👑
  • --one-event-per-cycle — only instruments one event per cycle. Minimalism, but make it technical.
  • --minimum-interference — instruments an optimal number of events. Optimal. She's efficient.
  • --my-events — only instruments events whose ids appear in inst.evt. Picky, and honestly valid.
  • --read-first, --write-first — only instrument cycles where a read or a write occurs as the first event, respectively. Choose your fighter. ⚔️
  • --max-var N — limits cycles to N variables read/written. Draws the boundary.
  • --max-po-trans N — limits cycles to N program-order edges. Same energy, different metric.
  • --ignore-arrays — instruments arrays as a single object. Whole array = one thing. Efficient. 🌸
  • --cav11 — always instruments shared variables, even when they're not part of any cycle. It's giving "I don't care if it's not in a cycle, I'm instrumenting it anyway." 💅
  • --force-loop-duplication, --no-loop-duplication — optional program transformation to construct cycles in program loops. Pick a side, bestie.
  • --cfg-kill — enables symbolic execution used to reduce spurious cycles. Killing the fake ones, keeping the real ones. 🔥
  • --no-dependencies — no dependency analysis. Skip it.
  • --no-po-rendering — no representation of the threads in the dot. The dot stays quiet about threads.
  • --hide-internals — does not include thread-internal (Rfi) events in the dot output. Privacy settings: on. 🙈
  • --render-cluster-file — clusterises the dot by files. Clusters, but file-shaped.
  • --render-cluster-function — clusterises the dot by functions. Clusters, but function-shaped.

🎀 Slicing: 🎀

  • --fp-reachability-slice f — removes instructions that can't appear on a trace that visits all the given functions. The list of functions has to be given as a comma separated list f. Nothing survives unless it's on the guest list. 📋
  • --reachability-slice — removes instructions that can't appear on a trace from entry point to a property. Cut.
  • --reachability-slice-fb — removes instructions that can't appear on a trace from entry point through a property. Same energy, but it goes through.
  • --full-slice — slices away instructions that don't affect assertions. If it doesn't matter to the assert, it's gone. ✂️
  • --property id — slice with respect to a specific property id only. One property. Just that one.
  • --slice-global-inits — slices away initializations of unused global variables. Unused? Uninitialized. Bye. 👋
  • --aggressive-slice — removes the bodies of any functions not on the shortest path between the start function and the function containing the property(s). She's not just slicing, she's aggressively slicing. 💀
  • --aggressive-slice-call-depth n — used with --aggressive-slice, preserves all functions within n function calls of the functions on the shortest path. A little mercy, as a treat.
  • --aggressive-slice-preserve-function f — forces the aggressive slicer to preserve function f. She's on the do-not-touch list. 🫶
  • --aggressive-slice-preserve-functions-containing f — forces the aggressive slicer to preserve all functions with names containing f. Any function with that name-vibe survives.
  • --aggressive-slice-preserve-all-direct-paths — forces the aggressive slicer to preserve all direct paths. Every direct path lives. Periodt.

💜 Code contracts: 💜

  • --apply-loop-contracts
  • -disable-loop-contracts-side-effect-check — UNSOUND OPTION, bestie, I'm not even joking 💀 this turns off the check that makes sure there are no side effects hiding in your loop contract clauses. With that check gone, your loop contract clauses will happily accept way more expressions — think pure functions, statement expressions, the whole chaotic little buffet. But then you have to personally guarantee the loop contracts are side-effect free yourself, or your results are not sound. Like, you're on your own with this one. 🙈
  • -loop-contracts-no-unwind — do not unwind transformed loops. Just... leave them un-unwound, okay?
  • -loop-contracts-file file — annotate loop contracts from file onto the goto program. Feeding it the good stuff from a file. 🍓
  • --replace-call-with-contract fun — swap out calls to fun with fun's own contract. Trading the call for the receipts, iconic.
  • --enforce-contract fun — wrap fun up with an assertion of its contract. Like putting a lil bow on it but the bow is an assertion. 🎀
  • --enforce-contract-rec fun — same energy as above but the assertion can actually handle recursive calls, which is lowkey a flex.
  • --dfcc fun — instrument dynamic frame condition checks, using fun as the entry point.

👑 User-interface options (the glow-up section) ✨

  • --flush — flush every single line of output. No buffering, no secrets, we're being transparent.
  • --xml — output files in XML, wherever that's supported. XML girlies rise
  • --xml-ui — use XML-formatted output for the interface. Same vibe, different wrapper.
  • --json-ui — use JSON-formatted output for the interface. For when your parser is a JSON simp 🫶
  • --verbosity n — set the verbosity level to n. Pick your volume. 🔊
  • --timestamp [monotonic|wall] — print microsecond-precision timestamps. So extra, so precise. Two flavors:
    • monotonic — the stamps increase monotonically, always moving forward, never looking back, main character energy fr fr.
    • wall — ISO-8601 wall clock timestamps. Actual real-world time, clocking you in. ⏰

🌍 ENVIRONMENT (the vibes around us)

Every single one of these tools honors the TMPDIR environment variable when it's generating temporary files and directories. So if you want your temp stuff to live somewhere specific, set TMPDIR and it'll respect that. 💅

🐛 BUGS (not me...)

If you hit a problem, please make an issue over at https://github.com/diffblue/cbmc/issues — the devs genuinely want to know, no cap. 🙏

👀 SEE ALSO (the friend group)

Go say hi, they're all part of the same little family. 🦋

2008-2013, Daniel Kroening

And that's the whole page, bestie — you made it to the end, which is honestly iconic of you. 🥳 This was goto-instrument-5.59.0, dated June 2022, living in GOTO-INSTRUMENT(1). Now go forth and instrument some gotos. You've got this. 💖✨

📦 where this page comes from