Usage: isla-litmus-dump [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.
--footprint-config <file>
load custom config for footprint analysis
--cache <path> A directory to cache intermediate results. The default
is TMPDIR if set, otherwise /tmp
-o, --output <file> Output file
--archsem-initial <file>
Outfile initial registers for ArchSem to file
--archsem-header <line>
Header line to include in ArchSem initial registers
output
-f, --format coq|human
Output Format
--memory <n> Add a max memory consumption (in megabytes)
Options (26)
| Option | Description | Source |
|---|
-T, --threads n | use this many worker threads | help |
-A, --arch file | load architecture file | help |
--toolchain name | use specified toolchain from config | help |
-R, --register register>=<value | set a register, via the reset_registers builtin | help |
-I, --initial register>=<value | set a register in the initial state | help |
-h, --help | print this help message | help |
--verbose | print verbose output | help |
--probe id | trace specified function calls or location assignments in debug output | help |
--probe-all | probe everything (very verbose) | help |
--probe-function id | probe everything under the specified function (very verbose) | help |
--trace-function id | trace specified function calls in the trace output | help |
--trace-all | trace everything | help |
-L, --linearize id | rewrite function into linear form | help |
-P, --partial-linearize id | rewrite function into linear form | help |
--test-linearize | test that linearization rewrite has been performed correctly | help |
--reset-constraint constraint | property to enforce at the reset_registers builtin | help |
--fork-assertions | change assertions into explicit control flow | help |
--fun-assumption assumption | add an assumption about the behaviour of a Sail function | help |
--no-model-reg-init | don't use register initializers from the model | help |
--version | print out version and stop. | help |
--footprint-config file | load custom config for footprint analysis | help |
--cache path | A directory to cache intermediate results. | help |
--archsem-initial file | Outfile initial registers for ArchSem to file | help |
--archsem-header line | Header line to include in ArchSem initial registers output | help |
-f, --format coq|human | Output Format | help |
--memory n | Add a max memory consumption (in megabytes) | 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.