/usr/bin/isla-axiomatic

Usage: isla-axiomatic [options]

Options:
    -T, --threads <n>   use this many worker threads
    -A, --arch <file>   load architecture file
    -C, --config <file> load custom config for architecture
        --toolchain <name>
                        use specified toolchain from config
    -R, --register <register>=<value>
                        set a register, via the reset_registers builtin
    -I, --initial <register>=<value>
                        set a register in the initial state
    -h, --help          print this help message
        --verbose       print verbose output
    -D, --debug <flags> set debugging flags
        --probe <id>    trace specified function calls or location assignments
                        in debug output
        --probe-all     probe everything (very verbose)
        --probe-function <id>
                        probe everything under the specified function (very
                        verbose)
        --trace-function <id>
                        trace specified function calls in the trace output
        --trace-all     trace everything
    -L, --linearize <id>
                        rewrite function into linear form
    -P, --partial-linearize <id>
                        rewrite function into linear form
    -S, --source <path> directory containing the Sail source used to generate
                        the IR
        --test-linearize
                        test that linearization rewrite has been performed
                        correctly
        --abstract <id> make function abstract
        --debug-id <name id>
                        print the name of an interned identifier (for
                        debugging)
        --reset-constraint <constraint>
                        property to enforce at the reset_registers builtin
        --fork-assertions
                        change assertions into explicit control flow
        --fun-assumption <assumption>
                        add an assumption about the behaviour of a Sail
                        function
        --no-model-reg-init
                        don't use register initializers from the model
        --version       print out version and stop.
        --herd7         Output in a herd7-compatible way
        --isla-litmus <path>
                        Path to isla-litmus binary
        --litmus-translator <path>
                        Path to litmus-translator binary (takes precedence
                        over isla-litmus)
        --footprint-config <file>
                        load custom config for footprint analysis
        --variant <variant>
                        model variants
        --thread-groups <n>
                        number threads per group
        --only-group <n>
                        only perform jobs for one thread group
    -s, --timeout <n>   Add a timeout (in seconds)
        --pc-limit <n>  Limit the number of times each instruction can be
                        visited
        --pc-limit-mode <error|discard>
                        What to do when the pc-limit is exceeded (default
                        error)
        --memory <n>    Add a max memory consumption (in megabytes)
    -m, --model <path>  Memory model in cat format
        --ifetch        Generate ifetch events
        --armv8-page-tables
                        Automatically set up ARMv8 page tables
        --merge-translations
                        Merge consecutive translate events into a single event
        --merge-split-stages
                        Split stages when merging translations
        --remove-uninteresting all/safe
                        Remove uninteresting translate events
    -e, --exhaustive    Attempt to exhaustively enumerate all possible rf
                        combinations
        --extra-smt <file>
                        additional SMT appended to each candidate
        --check-sat-using tactic
                        Use z3 tactic for checking satisfiablity
        --latex <path>  generate latex version of input files in specified
                        directory
        --graph <ascii|dot|none>
                        Draw graphs of executions
        --dot <path>    Place generated graphviz dot files in specified
                        directory
        --temp-dot      Generate graphviz dot files in TMPDIR or /tmp
        --graph-show-forbidden
                        Try draw graph of forbidden executions too
        --graph-debug   Show everything, all trace events and full information
                        in the nodes
        --graph-shows <show,show,...>
                        Overwrite showed relations
        --graph-human-readable
                        Try generate human-readable strings instead of
                        bitvectors where possible
        --graph-padding <iw-left=4,threads-down=2,...,(iw|threads|thread|instr|event)-(up|down|left|right)=value,...>
                        Overwrite default padding
        --graph-force-show-events <ev1,ev2,...>
                        Overwrite hiding of event
        --graph-force-hide-events <ev1,ev2,...>
                        Overwrite hiding of event
        --graph-show-all-reads
                        Always show read events (including translations and
                        ifetches)
        --graph-flatten
                        Flatten the graph, algining all rows and columns
                        across all threads and instructions
        --graph-squash-translation-labels
                        Squash translation event labels from `T s1:pte3(x)`
                        into `Ts1l3` to save space in diagrams
        --view          Open graphviz dot files in default image viewer.
                        Implies --temp-dot unless --dot is set.
        --no-z3-model   do not generate a graph (DEPRECATED, use --graph=none
                        instead)
        --refs <path>   references to compare output with
        --cache <path>  A directory to cache intermediate results. The default
                        is TMPDIR if set, otherwise /tmp