1WHY3(1)                          User Commands                         WHY3(1)
2
3
4

NAME

6       why3 - check verification conditions in source code
7

SYNOPSIS

9       why3 [OPTIONS] [[FILE|-] [-T <theory> [-G <goal>] ... ] ... ]
10

DESCRIPTION

12       Verify  conditions  in source code.  If the filename is "-", then input
13       is read from stdin.
14

OPTIONS

16       -T, --theory <theory>
17              Select theory in the input file or in the library.
18
19       -G, --goal <goal>
20              Select goal in the last selected theory.
21
22       -C, --config <file>
23              Read configuration from file.
24
25       -L, --library <dir>
26              Add dir to the library search path.
27
28       -P, --prover <prover>
29              Prove or print (with -o) the selected goals using prover.
30
31       -F, --format <format>
32              Select the input format (default: "why").
33
34       -t, --timelimit <sec>
35              Set the prover's time limit in seconds, where 0 means  no  limit
36              (default: 10).
37
38       -m, --memlimit <MiB>
39              Set the prover's memory limit in megabytes (default: no limit).
40
41       -a, --apply-transform <transformation>
42              Apply a transformation to every task.
43
44       -M, --meta <metaname>=<string>
45              Add a string meta to every task.
46
47       -D, --driver <file>
48              Specify a prover's driver (conflicts with -P).
49
50       -o, --output <dir>
51              Print the selected goals to separate files in dir.
52
53       --realize
54              Realize selected theories from the library.
55
56       --bisect
57              Reduce  the  set of needed axioms which prove a goal, and output
58              the resulting task.
59
60       --print-theory
61              Print selected theories.
62
63       --print-namespace
64              Print namespaces of selected theories.
65
66       --list-transforms
67              List known transformations.
68
69       --list-printers
70              List known printers.
71
72       --list-provers
73              List known provers.
74
75       --list-formats
76              List known input formats.
77
78       --list-metas
79              List known metas.
80
81       --list-debug-flags
82              List known debug flags.
83
84       --parse-only
85              Stop after parsing (same as --debug parse_only).
86
87       --type-only
88              Stop after type checking (same as --debug type_only).
89
90       --debug-all
91              Set all debug flags except parse_only and type_only.
92
93       --debug <flag>
94              Set a debug flag.
95
96       --print-libdir
97              Print location of binary components (plugins, etc.).
98
99       --print-datadir
100              Print location of non-binary data (theories, modules, etc.).
101
102       --version
103              Print version information.
104
105       -help, --help
106              Show a list of options.
107

SEE ALSO

109       why3-cpulimit(1), why3bench(1), why3config(1), why3doc(1),  why3ide(1),
110       why3ml(1), why3realize(1), why3replayer(1)
111
112
113
114why3                                 1.4.1                             WHY3(1)
Impressum