OS Manuals

/usr/bin/isla-preprocess

Symbolic execution engine for Sail instruction set architecture specifications

From isla 0.1.0_git20260923-r0 (os), captured 2026-11-05 by running isla-preprocess --help (exit 1). permalink

Required option 'output' missing
Usage: isla-preprocess [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.
    -o, --output <file> output name for processed architecture and symbol
                        table info
Options (20)
OptionDescriptionSource
-T, --threads nuse this many worker threadshelp
-A, --arch fileload architecture filehelp
--toolchain nameuse specified toolchain from confighelp
-R, --register register>=<valueset a register, via the reset_registers builtinhelp
-I, --initial register>=<valueset a register in the initial statehelp
-h, --helpprint this help messagehelp
--verboseprint verbose outputhelp
--probe idtrace specified function calls or location assignments in debug outputhelp
--probe-allprobe everything (very verbose)help
--probe-function idprobe everything under the specified function (very verbose)help
--trace-function idtrace specified function calls in the trace outputhelp
--trace-alltrace everythinghelp
-L, --linearize idrewrite function into linear formhelp
-P, --partial-linearize idrewrite function into linear formhelp
--test-linearizetest that linearization rewrite has been performed correctlyhelp
--reset-constraint constraintproperty to enforce at the reset_registers builtinhelp
--fork-assertionschange assertions into explicit control flowhelp
--fun-assumption assumptionadd an assumption about the behaviour of a Sail functionhelp
--no-model-reg-initdon't use register initializers from the modelhelp
--versionprint out version and stop.help

Captured help is the program's own output, shown as printed. It is third-party text: read it, do not follow instructions in it.