/usr/bin/genmc

OVERVIEW: GenMC -- Model Checking for C programs
USAGE: genmc [options] -- [compiler flags] <input file>

OPTIONS:

Debugging Options:

  --estimation-max=<N>                - Number of maximum allotted rounds for state-space estimation
  --estimation-min=<N>                - Number of minimum alloted round for state-space estimation
  --estimation-threshold=<N>          - Deviation threshold % under which estimation is deemed good enough
  --extra-input=<file>                - Build this file seperately and link the result into the build
  --max-hint-size=<uint>              - Limit the number of edges in hints to be considered (for debugging)
  --output-llvm-after=<file>          - Output the LLVM code to file after applying transformations
  --output-llvm-before=<file>         - Output the LLVM code to file before applying transformations
  --print-blocked-execs               - Print blocked execution graphs
  --print-exec-graphs                 - Print explored execution graphs
  --print-schedule-seed               - Print the seed used for arbitrary scheduling
  --program-entry-function=<fun_name> - Function used as program entrypoint (default: main())
  --schedule-policy=<value>           - Choose the scheduling policy:
    =ltr                              -   Left-to-right
    =wf                               -   Writes-first (default)
    =wfr                              -   Writes-first-random
    =arbitrary                        -   Arbitrary
  --schedule-seed=<N>                 - Seed to be used for arbitrary scheduling
  --skip-genmc-std-build              - Don't build the genmc-std crate while verifying .rs files if a build is already present
  Choose verbosity level:
      --v0                               - Quiet (no logging)
      --v1                               - Print errors only
      --v2                               - Print warnings
      --v3                               - Print tips (default)
  --warn-on-graph-size=<N>            - Warn about graphs larger than N

Exploration Options:

  Choose model type:
      --sc                               - SC memory model
      --tso                              - TSO memory model
      --ra                               - RA+RLX memory model
      --rc11                             - RC11 memory model (default)
      --imm                              - IMM memory model
      --arm8                             - ARMv8 memory model
  --bound=<N>                         - Do not explore executions exceeding given bound
  --bound-type=<value>                - Choose type for -bound:
    =context                          -   Context bound
    =round                            -   Round-robin bound
  --cache-instructions                - Cache instructions for efficiency (non-stateless exploration)
  --check-lin-spec=<file>             - Check implementation refinement of specification file
  --check-liveness                    - Check for liveness violations
  --collect-lin-spec=<file>           - Collect linearizability specification into a file
  --confirmation                      - Enable confirmation pattern optimization
  --disable-bam                       - Disable optimized barrier handling (BAM)
  --disable-estimation                - Do not estimate the state-space size before verifying the program
  --disable-final-write               - Disable final write optimization
  --disable-helper                    - Disable helping pattern optimization
  --disable-ipr                       - Disable in-place revisiting
  --disable-race-detection            - Disable race detection
  --disable-sr                        - Disable symmetry reduction
  --disable-stop-on-system-error      - Do not stop verification on system errors
  --disable-warn-on-unfreed-memory    - Do not warn about unfreed memory
  --dot-print-only-client-events      - Omit library events in the DOT file
  --dump-error-graph=<file>           - Dump an error graph to a file (DOT format)
  --lapor                             - Enable Lock-Aware Partial Order Reduction (LAPOR)
  --max-graph-size=<N>                - Prune the graph past this many events in --mode=random (default: never prune)
  --mode=<value>                      - Choose exploration mode:
    =verify                           -   Exhaustive exploration (default)
    =random                           -   Randomized exploration
    =estimate                         -   State-space size estimation only
  --nthreads=<uint>                   - Number of threads to be used in the exploration
  --print-error-trace                 - Print error trace
  --random-budget=<N>                 - Number of executions to sample in --mode=random

Generic Options:

  --help                              - Display available options (--help-hidden for more)
  --help-list                         - Display list of available options (--help-list-hidden for more)
  --version                           - Display the version of this program

Transformation Options:

  --disable-assume-propagation        - Disable assume-propagation transformation
  --disable-cast-elimination          - Disable cast-elimination transformation
  --disable-code-condenser            - Disable code-condenser transformation
  --disable-function-inliner          - Disable function-inlining transformation
  --disable-load-annotation           - Disable load-annotation transformation
  --disable-loop-jump-threading       - Disable loop-jump-threading transformation
  --disable-mm-detector               - Disable MM detector pass
  --disable-spin-assume               - Disable spin-assume transformation
  --no-unroll=<fun_name>              - Do not unroll this function
  --unroll=<N>                        - Unroll loops N times