goto-instrument(1) on Linux

The text e6f90361a3c4, as Debian 13 (Trixie) shipped it. The page shows this text now.

Perform analysis or instrumentation of goto binaries

Flags it lists

--accelerate
--add-library
--aggressive-slice
--aggressive-slice-call-depth
--aggressive-slice-preserve-all-direct-paths
--aggressive-slice-preserve-function
--aggressive-slice-preserve-functions-containing
--apply-loop-contracts
--assert-to-assume
--base-case
--bounds-check
--branch
--call-graph
--cav11
--cfg-kill
--check-call-sequence
--constant-propagator
--continue-as-loops
--conversion-check
--count-eloc
--custom-bitvector-analysis
--dfcc
--dfcc-debug-lib
--dfcc-simple-invalid-pointer-model
--div-by-zero-check
--document-properties-html
--document-properties-latex
--dot
--drop-unused-functions
--dump-c
--dump-c-type-header
--dump-cpp
--enforce-contract
--enforce-contract-rec
--ensure-one-backedge-per-target
--enum-range-check
--error-label
--escape-analysis
--float-div-by-zero-check
--float-overflow-check
--flush
--force-loop-duplication
--fp-reachability-slice
--full-slice
--function-enter
--function-exit
--function-inline
--function-pointer-restrictions-file
--generate-function-body
--generate-function-body-options
--harness
--havoc-loops
--hide-internals
--horn
--ignore-arrays
--inline
--insert-final-assert-false
--interpreter
--interval-analysis
--isr
--json-ui
--k-induction
--list-calls-args
--list-eloc
--list-goto-functions
--list-symbols
--list-undefined-functions
--log
--malloc-fail-assert
--malloc-fail-null
--malloc-may-fail
--max-nondet-tree-depth
--max-po-trans
--max-var
--memory-cleanup-check
--memory-leak-check
--min-null-tree-depth
--minimum-interference
--mm
--mmio
--model-argc-argv
--my-events
--nan-check
--no-assertions
--no-assumptions
--no-built-in-assertions
--no-caching
--no-dependencies
--no-loop-duplication
--no-malloc-may-fail
--no-po-rendering
--no-system-headers
--no-unwinding-assertions
--nondet-static
--nondet-static-exclude
--nondet-static-matching
--nondet-volatile
--nondet-volatile-model
--nondet-volatile-variable
--one-event-per-cycle
--partial-inline
--partial-loops
--pointer-check
--pointer-overflow-check
--pointer-primitive-check
--print-global-state-size
--print-internal-representation
--print-path-lengths
--property
--race-check
--reachability-slice
--reachability-slice-fb
--reachable-call-graph
--read-first
--remove-calls-no-body
--remove-const-function-pointers
--remove-function-body
--remove-function-pointers
--remove-pointers
--render-cluster-file
--render-cluster-function
--replace-call-with-contract
--replace-calls
--restrict-function-pointer
--restrict-function-pointer-by-name
--retain-trivial-checks
--scc
--show-call-sequences
--show-class-hierarchy
--show-custom-bitvector-analysis
--show-dependence-graph
--show-escape-analysis
--show-global-may-alias
--show-goto-functions
--show-intervals
--show-lexical-loops
--show-local-bitvector-analysis
--show-local-safe-pointers
--show-locations
--show-loops
--show-natural-loops
--show-points-to
--show-properties
--show-reaching-definitions
--show-rw-set
--show-safe-dereferences
--show-sese-regions
--show-struct-alignment
--show-symbol-table
--show-threaded
--show-uninitialized
--show-value-sets
--signed-overflow-check
--skip-loops
--slice-global-inits
--splice-call
--stack-depth
--step-case
--string-abstraction
--timestamp
--undefined-function-is-assume-false
--undefined-shift-check
--uninitialized-check
--unsigned-overflow-check
--unwind
--unwinding-assertions
--unwindset
--unwindset-file
--use-all-headers
--validate-goto-binary
--validate-goto-model
--validate-ssa-equation
--value-set-fi-fp-removal
--verbosity
--write-first
--xml
--xml-ui
--z3
-disable-loop-contracts-side-effect-check
-loop-contracts-file
-loop-contracts-no-unwind

goto-instrument(1) on Linux now