why3 - Man Page
check verification conditions in source code
Synopsis
why3 [Options] [[FILE|-] [-T <theory> [-G <goal>] ... ] ... ]
Description
Verify conditions in source code. If the filename is "-", then input is read from stdin.
Options
- -T, --theory <theory>
Select theory in the input file or in the library.
- -G, --goal <goal>
Select goal in the last selected theory.
- -C, --config <file>
Read configuration from file.
- -L, --library <dir>
Add dir to the library search path.
- -P, --prover <prover>
Prove or print (with -o) the selected goals using prover.
- -F, --format <format>
Select the input format (default: "why").
- -t, --timelimit <sec>
Set the prover's time limit in seconds, where 0 means no limit (default: 10).
- -m, --memlimit <MiB>
Set the prover's memory limit in megabytes (default: no limit).
- -a, --apply-transform <transformation>
Apply a transformation to every task.
- -M, --meta <metaname>=<string>
Add a string meta to every task.
- -D, --driver <file>
Specify a prover's driver (conflicts with -P).
- -o, --output <dir>
Print the selected goals to separate files in dir.
- --realize
Realize selected theories from the library.
- --bisect
Reduce the set of needed axioms which prove a goal, and output the resulting task.
- --print-theory
Print selected theories.
- --print-namespace
Print namespaces of selected theories.
- --list-transforms
List known transformations.
- --list-printers
List known printers.
- --list-provers
List known provers.
- --list-formats
List known input formats.
- --list-metas
List known metas.
- --list-debug-flags
List known debug flags.
- --parse-only
Stop after parsing (same as --debug parse_only).
- --type-only
Stop after type checking (same as --debug type_only).
- --debug-all
Set all debug flags except parse_only and type_only.
- --debug <flag>
Set a debug flag.
- --print-libdir
Print location of binary components (plugins, etc.).
- --print-datadir
Print location of non-binary data (theories, modules, etc.).
- --version
Print version information.
- -help, --help
Show a list of options.
See Also
why3-cpulimit(1), why3bench(1), why3config(1), why3doc(1), why3ide(1), why3ml(1), why3realize(1), why3replayer(1)
Referenced By
why3bench(1), why3-cpulimit(1), why3doc(1), why3ide(1), why3ml(1), why3realize(1), why3replayer(1).