why3 man page

why3 — 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).

0.87.2 why3 User Commands