Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
96cfbb62
Commit
96cfbb62
authored
Jul 11, 2014
by
Andrei Paskevich
Browse files
move Args inside Whyconf
parent
8ebe2032
Changes
12
Hide whitespace changes
Inline
Side-by-side
Makefile.in
View file @
96cfbb62
...
...
@@ -510,7 +510,7 @@ clean::
###############
TOOLS_BIN
=
why3execute why3extract why3prove why3realize why3replay
TOOLS_FILES
=
args
main
$(TOOLS_BIN)
TOOLS_FILES
=
main
$(TOOLS_BIN)
TOOLSMODULES
=
$(
addprefix
src/tools/,
$(TOOLS_FILES)
)
...
...
@@ -524,51 +524,51 @@ $(TOOLSCMO) $(TOOLSCMX): INCLUDES += -I src/tools
byte
:
bin/why3.byte $(TOOLS_BIN:%=bin/%.byte)
opt
:
bin/why3.opt $(TOOLS_BIN:%=bin/%.opt)
bin/why3.opt
:
lib/why3/why3.cmxa
src/tools/args.cmx
src/tools/main.cmx
bin/why3.opt
:
lib/why3/why3.cmxa src/tools/main.cmx
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
\
$(OCAMLOPT)
$(OFLAGS)
-o
$@
$(OLINKFLAGS)
$^
bin/why3.byte
:
lib/why3/why3.cma
src/tools/args.cmo
src/tools/main.cmo
bin/why3.byte
:
lib/why3/why3.cma src/tools/main.cmo
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
\
$(OCAMLC)
$(BFLAGS)
-o
$@
$(BLINKFLAGS)
$^
bin/why3execute.opt
:
lib/why3/why3.cmxa
src/tools/args.cmx
src/tools/why3execute.cmx
bin/why3execute.opt
:
lib/why3/why3.cmxa src/tools/why3execute.cmx
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
\
$(OCAMLOPT)
$(OFLAGS)
-o
$@
$(OLINKFLAGS)
$^
bin/why3execute.byte
:
lib/why3/why3.cma
src/tools/args.cmo
src/tools/why3execute.cmo
bin/why3execute.byte
:
lib/why3/why3.cma src/tools/why3execute.cmo
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
\
$(OCAMLC)
$(BFLAGS)
-o
$@
$(BLINKFLAGS)
$^
bin/why3extract.opt
:
lib/why3/why3.cmxa
src/tools/args.cmx
src/tools/why3extract.cmx
bin/why3extract.opt
:
lib/why3/why3.cmxa src/tools/why3extract.cmx
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
\
$(OCAMLOPT)
$(OFLAGS)
-o
$@
$(OLINKFLAGS)
$^
bin/why3extract.byte
:
lib/why3/why3.cma
src/tools/args.cmo
src/tools/why3extract.cmo
bin/why3extract.byte
:
lib/why3/why3.cma src/tools/why3extract.cmo
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
\
$(OCAMLC)
$(BFLAGS)
-o
$@
$(BLINKFLAGS)
$^
bin/why3prove.opt
:
lib/why3/why3.cmxa
src/tools/args.cmx
src/tools/why3prove.cmx
bin/why3prove.opt
:
lib/why3/why3.cmxa src/tools/why3prove.cmx
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
\
$(OCAMLOPT)
$(OFLAGS)
-o
$@
$(OLINKFLAGS)
$^
bin/why3prove.byte
:
lib/why3/why3.cma
src/tools/args.cmo
src/tools/why3prove.cmo
bin/why3prove.byte
:
lib/why3/why3.cma src/tools/why3prove.cmo
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
\
$(OCAMLC)
$(BFLAGS)
-o
$@
$(BLINKFLAGS)
$^
bin/why3realize.opt
:
lib/why3/why3.cmxa
src/tools/args.cmx
src/tools/why3realize.cmx
bin/why3realize.opt
:
lib/why3/why3.cmxa src/tools/why3realize.cmx
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
\
$(OCAMLOPT)
$(OFLAGS)
-o
$@
$(OLINKFLAGS)
$^
bin/why3realize.byte
:
lib/why3/why3.cma
src/tools/args.cmo
src/tools/why3realize.cmo
bin/why3realize.byte
:
lib/why3/why3.cma src/tools/why3realize.cmo
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
\
$(OCAMLC)
$(BFLAGS)
-o
$@
$(BLINKFLAGS)
$^
bin/why3replay.opt
:
lib/why3/why3.cmxa lib/why3/why3session.cmxa
src/tools/args.cmx
src/tools/why3replay.cmx
bin/why3replay.opt
:
lib/why3/why3.cmxa lib/why3/why3session.cmxa src/tools/why3replay.cmx
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
\
$(OCAMLOPT)
$(OFLAGS)
-o
$@
$(OLINKFLAGS)
$^
bin/why3replay.byte
:
lib/why3/why3.cma lib/why3/why3session.cma
src/tools/args.cmo
src/tools/why3replay.cmo
bin/why3replay.byte
:
lib/why3/why3.cma lib/why3/why3session.cma src/tools/why3replay.cmo
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
\
$(OCAMLC)
$(BFLAGS)
-o
$@
$(BLINKFLAGS)
$^
...
...
@@ -595,7 +595,6 @@ endif
depend
:
$(TOOLSDEP)
clean
::
rm
-f
src/tools/args.cm[iox] src/tools/args.annot src/tools/args.o src/tools/args.dep
rm
-f
src/tools/main.cm[iox] src/tools/main.annot src/tools/main.o src/tools/main.dep
rm
-f
src/tools/why3execute.cm[iox] src/tools/why3execute.annot src/tools/why3execute.o src/tools/why3execute.dep
rm
-f
src/tools/why3extract.cm[iox] src/tools/why3extract.annot src/tools/why3extract.o src/tools/why3extract.dep
...
...
src/driver/whyconf.ml
View file @
96cfbb62
...
...
@@ -748,3 +748,54 @@ let () = Exn_printer.register (fun fmt e -> match e with
fprintf
fmt
"Shortcut %s appears two times in the configuration file"
s
|
_
->
raise
e
)
module
Args
=
struct
let
opt_config
=
ref
None
let
opt_extra
=
ref
[]
let
opt_loadpath
=
ref
[]
let
opt_help
=
ref
false
let
common_options_head
=
[
"-C"
,
Arg
.
String
(
fun
s
->
opt_config
:=
Some
s
)
,
"<file> read configuration from <file>"
;
"--config"
,
Arg
.
String
(
fun
s
->
opt_config
:=
Some
s
)
,
" same as -C"
;
"--extra-config"
,
Arg
.
String
(
fun
s
->
opt_extra
:=
!
opt_extra
@
[
s
])
,
"<file> read additional configuration from <file>"
;
"-L"
,
Arg
.
String
(
fun
s
->
opt_loadpath
:=
s
::
!
opt_loadpath
)
,
"<dir> add <dir> to the library search path"
;
"--library"
,
Arg
.
String
(
fun
s
->
opt_loadpath
:=
s
::
!
opt_loadpath
)
,
" same as -L"
;
Debug
.
Args
.
desc_debug
;
Debug
.
Args
.
desc_debug_all
;
Debug
.
Args
.
desc_debug_list
;
]
let
common_options_tail
=
[
"-h"
,
Arg
.
Set
opt_help
,
" print this list of options"
;
"-help"
,
Arg
.
Set
opt_help
,
""
;
"--help"
,
Arg
.
Set
opt_help
,
" same as -h"
;
]
let
align_options
options
=
Arg
.
align
(
common_options_head
@
options
@
common_options_tail
)
let
initialize
?
(
extra_help
=
Format
.
pp_print_newline
)
options
default
usage
=
let
options
=
align_options
options
in
Arg
.
parse
options
default
usage
;
if
!
opt_help
then
begin
Format
.
printf
"@[%s%a@]"
(
Arg
.
usage_string
options
usage
)
extra_help
()
;
exit
0
end
;
let
config
=
read_config
!
opt_config
in
let
config
=
List
.
fold_left
merge_config
config
!
opt_extra
in
let
main
=
get_main
config
in
load_plugins
main
;
Debug
.
Args
.
set_flags_selected
()
;
if
Debug
.
Args
.
option_list
()
then
exit
0
;
let
lp
=
List
.
rev_append
!
opt_loadpath
(
loadpath
main
)
in
config
,
Env
.
create_env
lp
let
exit_with_usage
options
usage
=
Arg
.
usage
(
align_options
options
)
usage
;
exit
1
end
src/driver/whyconf.mli
View file @
96cfbb62
...
...
@@ -63,10 +63,10 @@ val get_conf_file : config -> string
(** {2 Main section} *)
type
main
val
get_main
:
config
->
main
val
get_main
:
config
->
main
(** [get_main config] get the main section stored in the Rc file *)
val
set_main
:
config
->
main
->
config
val
set_main
:
config
->
main
->
config
(** [set_main config main] replace the main section by the given one *)
val
libdir
:
main
->
string
...
...
@@ -87,11 +87,11 @@ val load_plugins : main -> unit
(** {3 Prover's identifier} *)
type
prover
=
{
prover_name
:
string
;
(* "Alt-Ergo" *)
prover_version
:
string
;
(* "2.95" *)
prover_altern
:
string
;
(* "special" *)
}
type
prover
=
{
prover_name
:
string
;
(* "Alt-Ergo" *)
prover_version
:
string
;
(* "2.95" *)
prover_altern
:
string
;
(* "special" *)
}
(** record of necessary data for a given external prover *)
val
print_prover
:
Format
.
formatter
->
prover
->
unit
...
...
@@ -107,7 +107,7 @@ module Hprover : Exthtbl.S with type key = prover
(** {3 Prover configuration} *)
type
config_prover
=
{
prover
:
prover
;
(* unique name for session *)
prover
:
prover
;
(* unique name for session *)
command
:
string
;
(* "exec why-limit %t %m alt-ergo %f" *)
driver
:
string
;
(* "/usr/local/share/why/drivers/ergo-spec.drv" *)
in_place
:
bool
;
(* verification should be performed in-place *)
...
...
@@ -120,7 +120,7 @@ type config_prover = {
val
get_complete_command
:
config_prover
->
string
(** add the extra_options to the command *)
val
get_provers
:
config
->
config_prover
Mprover
.
t
val
get_provers
:
config
->
config_prover
Mprover
.
t
(** [get_provers config] get the prover family stored in the Rc file. The
keys are the unique ids of the prover (argument of the family) *)
...
...
@@ -156,7 +156,6 @@ val editor_by_id : config -> string -> config_editor
(** return the configuration of the editor if found, otherwise return
Not_found *)
(** prover upgrade policy *)
type
prover_upgrade_policy
=
...
...
@@ -232,3 +231,15 @@ val set_section : config -> string -> Rc.section -> config
val
set_family
:
config
->
string
->
Rc
.
family
->
config
(** [set_family config name] Same as {!Rc.set_family} except name
must not be prover *)
(** Common command line options *)
module
Args
:
sig
val
initialize
:
?
extra_help
:
(
Format
.
formatter
->
unit
->
unit
)
->
(
string
*
Arg
.
spec
*
string
)
list
->
(
string
->
unit
)
->
string
->
config
*
Env
.
env
val
exit_with_usage
:
(
string
*
Arg
.
spec
*
string
)
list
->
string
->
'
a
end
src/tools/args.ml
deleted
100644 → 0
View file @
8ebe2032
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2014 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
open
Why3
let
opt_config
=
ref
None
let
opt_extra
=
ref
[]
let
opt_loadpath
=
ref
[]
let
opt_help
=
ref
false
let
common_options_head
=
[
"-C"
,
Arg
.
String
(
fun
s
->
opt_config
:=
Some
s
)
,
"<file> read configuration from <file>"
;
"--config"
,
Arg
.
String
(
fun
s
->
opt_config
:=
Some
s
)
,
" same as -C"
;
"--extra-config"
,
Arg
.
String
(
fun
s
->
opt_extra
:=
!
opt_extra
@
[
s
])
,
"<file> read additional configuration from <file>"
;
"-L"
,
Arg
.
String
(
fun
s
->
opt_loadpath
:=
s
::
!
opt_loadpath
)
,
"<dir> add <dir> to the library search path"
;
"--library"
,
Arg
.
String
(
fun
s
->
opt_loadpath
:=
s
::
!
opt_loadpath
)
,
" same as -L"
;
Debug
.
Args
.
desc_debug
;
Debug
.
Args
.
desc_debug_all
;
Debug
.
Args
.
desc_debug_list
;
]
let
common_options_tail
=
[
"-h"
,
Arg
.
Set
opt_help
,
" print this list of options"
;
"-help"
,
Arg
.
Set
opt_help
,
""
;
"--help"
,
Arg
.
Set
opt_help
,
" same as -h"
;
]
let
align_options
options
=
Arg
.
align
(
common_options_head
@
options
@
common_options_tail
)
let
initialize
?
(
extra_help
=
Format
.
pp_print_newline
)
options
default
usage
=
let
options
=
align_options
options
in
Arg
.
parse
options
default
usage
;
if
!
opt_help
then
begin
Format
.
printf
"@[%s%a@]"
(
Arg
.
usage_string
options
usage
)
extra_help
()
;
exit
0
end
;
let
config
=
Whyconf
.
read_config
!
opt_config
in
let
config
=
List
.
fold_left
Whyconf
.
merge_config
config
!
opt_extra
in
let
main
=
Whyconf
.
get_main
config
in
Whyconf
.
load_plugins
main
;
Debug
.
Args
.
set_flags_selected
()
;
if
Debug
.
Args
.
option_list
()
then
exit
0
;
let
lp
=
List
.
rev_append
!
opt_loadpath
(
Whyconf
.
loadpath
main
)
in
(
Env
.
create_env
lp
,
config
)
let
exit_with_usage
options
usage
=
Arg
.
usage
(
align_options
options
)
usage
;
exit
1
src/tools/args.mli
deleted
100644 → 0
View file @
8ebe2032
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2014 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
open
Why3
val
initialize
:
?
extra_help
:
(
Format
.
formatter
->
unit
->
unit
)
->
(
string
*
Arg
.
spec
*
string
)
list
->
(
string
->
unit
)
->
string
->
Env
.
env
*
Whyconf
.
config
val
exit_with_usage
:
(
string
*
Arg
.
spec
*
string
)
list
->
string
->
'
a
src/tools/main.ml
View file @
96cfbb62
...
...
@@ -93,7 +93,7 @@ let command sscmd =
let
()
=
try
let
extra_help
fmt
()
=
extra_help
fmt
(
available_commands
()
)
in
let
_
,
config
=
Args
.
initialize
~
extra_help
option_list
command
usage_msg
in
let
config
,_
=
Args
.
initialize
~
extra_help
option_list
command
usage_msg
in
(** listings *)
...
...
src/tools/why3execute.ml
View file @
96cfbb62
...
...
@@ -14,7 +14,7 @@ open Why3
open
Stdlib
let
usage_msg
=
sprintf
"Usage: %s [options] file module.ident..."
"Usage:
why3
%s [options] file module.ident..."
(
Filename
.
basename
Sys
.
argv
.
(
0
))
let
opt_file
=
ref
None
...
...
@@ -33,15 +33,15 @@ let opt_parser = ref None
let
option_list
=
[
"-F"
,
Arg
.
String
(
fun
s
->
opt_parser
:=
Some
s
)
,
"<format>
S
elect input format (default:
\"
why
\"
)"
;
"<format>
s
elect input format (default:
\"
why
\"
)"
;
"--format"
,
Arg
.
String
(
fun
s
->
opt_parser
:=
Some
s
)
,
" same as -F"
]
let
(
env
,
config
)
=
Args
.
initialize
option_list
add_opt
usage_msg
let
config
,
env
=
Whyconf
.
Args
.
initialize
option_list
add_opt
usage_msg
let
()
=
if
!
opt_file
=
None
then
Args
.
exit_with_usage
option_list
usage_msg
if
!
opt_file
=
None
then
Whyconf
.
Args
.
exit_with_usage
option_list
usage_msg
let
do_input
f
=
let
fname
,
cin
=
...
...
src/tools/why3extract.ml
View file @
96cfbb62
...
...
@@ -15,7 +15,7 @@ open Stdlib
open
Theory
let
usage_msg
=
sprintf
"Usage: %s [options] -D <driver> -o <dir> [[file|-] [-T <theory>]...]..."
"Usage:
why3
%s [options] -D <driver> -o <dir> [[file|-] [-T <theory>]...]..."
(
Filename
.
basename
Sys
.
argv
.
(
0
))
let
opt_queue
=
Queue
.
create
()
...
...
@@ -53,30 +53,30 @@ let opt_output = ref None
let
option_list
=
[
"-"
,
Arg
.
Unit
(
fun
()
->
add_opt_file
"-"
)
,
"
R
ead the input file from stdin"
;
"
r
ead the input file from stdin"
;
"-T"
,
Arg
.
String
add_opt_theory
,
"<theory>
S
elect <theory> in the input file or in the library"
;
"<theory>
s
elect <theory> in the input file or in the library"
;
"--theory"
,
Arg
.
String
add_opt_theory
,
" same as -T"
;
"-F"
,
Arg
.
String
(
fun
s
->
opt_parser
:=
Some
s
)
,
"<format>
S
elect input format (default:
\"
why
\"
)"
;
"<format>
s
elect input format (default:
\"
why
\"
)"
;
"--format"
,
Arg
.
String
(
fun
s
->
opt_parser
:=
Some
s
)
,
" same as -F"
;
"-D"
,
Arg
.
String
(
fun
s
->
opt_driver
:=
Some
s
)
,
"<file>
S
pecify a driver"
;
"<file>
s
pecify a driver"
;
"--driver"
,
Arg
.
String
(
fun
s
->
opt_driver
:=
Some
s
)
,
" same as -D"
;
"-o"
,
Arg
.
String
(
fun
s
->
opt_output
:=
Some
s
)
,
"<dir>
P
rint the selected goals to separate files in <dir>"
;
"<dir>
p
rint the selected goals to separate files in <dir>"
;
"--output"
,
Arg
.
String
(
fun
s
->
opt_output
:=
Some
s
)
,
" same as -o"
]
let
(
env
,
config
)
=
Args
.
initialize
option_list
add_opt_file
usage_msg
let
config
,
env
=
Whyconf
.
Args
.
initialize
option_list
add_opt_file
usage_msg
let
()
=
if
Queue
.
is_empty
opt_queue
then
Args
.
exit_with_usage
option_list
usage_msg
Whyconf
.
Args
.
exit_with_usage
option_list
usage_msg
let
opt_output
=
match
!
opt_output
with
...
...
src/tools/why3prove.ml
View file @
96cfbb62
...
...
@@ -18,7 +18,7 @@ open Task
open
Driver
let
usage_msg
=
sprintf
"Usage: %s [options] [[file|-] [-T <theory> [-G <goal>]...]...]..."
"Usage:
why3
%s [options] [[file|-] [-T <theory> [-G <goal>]...]...]..."
(
Filename
.
basename
Sys
.
argv
.
(
0
))
let
opt_queue
=
Queue
.
create
()
...
...
@@ -94,60 +94,62 @@ let opt_print_namespace = ref false
let
option_list
=
[
"-"
,
Arg
.
Unit
(
fun
()
->
add_opt_file
"-"
)
,
"
R
ead the input file from stdin"
;
"
r
ead the input file from stdin"
;
"-T"
,
Arg
.
String
add_opt_theory
,
"<theory>
S
elect <theory> in the input file or in the library"
;
"<theory>
s
elect <theory> in the input file or in the library"
;
"--theory"
,
Arg
.
String
add_opt_theory
,
" same as -T"
;
"-G"
,
Arg
.
String
add_opt_goal
,
"<goal>
S
elect <goal> in the last selected theory"
;
"<goal>
s
elect <goal> in the last selected theory"
;
"--goal"
,
Arg
.
String
add_opt_goal
,
" same as -G"
;
"-P"
,
Arg
.
String
(
fun
s
->
opt_prover
:=
Some
s
)
,
"<prover>
P
rove or print (with -o) the selected goals"
;
"<prover>
p
rove or print (with -o) the selected goals"
;
"--prover"
,
Arg
.
String
(
fun
s
->
opt_prover
:=
Some
s
)
,
" same as -P"
;
"-F"
,
Arg
.
String
(
fun
s
->
opt_parser
:=
Some
s
)
,
"<format>
S
elect input format (default:
\"
why
\"
)"
;
"<format>
s
elect input format (default:
\"
why
\"
)"
;
"--format"
,
Arg
.
String
(
fun
s
->
opt_parser
:=
Some
s
)
,
" same as -F"
;
"-t"
,
Arg
.
Int
(
fun
i
->
opt_timelimit
:=
Some
i
)
,
"<sec>
S
et the prover's time limit (default=10, no limit=0)"
;
"<sec>
s
et the prover's time limit (default=10, no limit=0)"
;
"--timelimit"
,
Arg
.
Int
(
fun
i
->
opt_timelimit
:=
Some
i
)
,
" same as -t"
;
"-m"
,
Arg
.
Int
(
fun
i
->
opt_memlimit
:=
Some
i
)
,
"<MiB>
S
et the prover's memory limit (default: no limit)"
;
"<MiB>
s
et the prover's memory limit (default: no limit)"
;
"--memlimit"
,
Arg
.
Int
(
fun
i
->
opt_timelimit
:=
Some
i
)
,
" same as -m"
;
"-a"
,
Arg
.
String
add_opt_trans
,
"<transformation>
A
pply a transformation to every task"
;
"<transformation>
a
pply a transformation to every task"
;
"--apply-transform"
,
Arg
.
String
add_opt_trans
,
" same as -a"
;
"-M"
,
Arg
.
String
add_opt_meta
,
"<meta_name>[=<string>]
A
dd a meta to every task"
;
"<meta_name>[=<string>]
a
dd a meta to every task"
;
"--meta"
,
Arg
.
String
add_opt_meta
,
" same as -M"
;
"-D"
,
Arg
.
String
(
fun
s
->
opt_driver
:=
Some
(
s
,
[]
))
,
"<file>
S
pecify a prover's driver (conflicts with -P)"
;
"<file>
s
pecify a prover's driver (conflicts with -P)"
;
"--driver"
,
Arg
.
String
(
fun
s
->
opt_driver
:=
Some
(
s
,
[]
))
,
" same as -D"
;
"-o"
,
Arg
.
String
(
fun
s
->
opt_output
:=
Some
s
)
,
"<dir>
P
rint the selected goals to separate files in <dir>"
;
"<dir>
p
rint the selected goals to separate files in <dir>"
;
"--output"
,
Arg
.
String
(
fun
s
->
opt_output
:=
Some
s
)
,
" same as -o"
;
"--print-theory"
,
Arg
.
Set
opt_print_theory
,
"
P
rint selected theories"
;
"
p
rint selected theories"
;
"--print-namespace"
,
Arg
.
Set
opt_print_namespace
,
" Print namespaces of selected theories"
;
Debug
.
Args
.
desc_shortcut
"parse_only"
"--parse-only"
" Stop after parsing"
;
" print namespaces of selected theories"
;
Debug
.
Args
.
desc_shortcut
"type_only"
"--type-only"
" Stop after type checking"
]
"parse_only"
"--parse-only"
" stop after parsing"
;
Debug
.
Args
.
desc_shortcut
"type_only"
"--type-only"
" stop after type checking"
]
let
(
env
,
config
)
=
Args
.
initialize
option_list
add_opt_file
usage_msg
let
config
,
env
=
Whyconf
.
Args
.
initialize
option_list
add_opt_file
usage_msg
let
()
=
try
if
Queue
.
is_empty
opt_queue
then
Args
.
exit_with_usage
option_list
usage_msg
;
if
Queue
.
is_empty
opt_queue
then
Whyconf
.
Args
.
exit_with_usage
option_list
usage_msg
;
if
!
opt_prover
<>
None
&&
!
opt_driver
<>
None
then
begin
eprintf
"Options '-P'/'--prover' and \
...
...
src/tools/why3realize.ml
View file @
96cfbb62
...
...
@@ -13,7 +13,7 @@ open Format
open
Why3
let
usage_msg
=
sprintf
"Usage: %s [options] -D <driver> -o <dir> -T <theory> ..."
"Usage:
why3
%s [options] -D <driver> -o <dir> -T <theory> ..."
(
Filename
.
basename
Sys
.
argv
.
(
0
))
let
opt_queue
=
Queue
.
create
()
...
...
@@ -44,27 +44,28 @@ let opt_output = ref None
let
option_list
=
[
"-T"
,
Arg
.
String
add_opt_theory
,
"<theory>
S
elect <theory> in the input file or in the library"
;
"<theory>
s
elect <theory> in the input file or in the library"
;
"--theory"
,
Arg
.
String
add_opt_theory
,
" same as -T"
;
"-F"
,
Arg
.
String
(
fun
s
->
opt_parser
:=
Some
s
)
,
"<format>
S
elect input format (default:
\"
why
\"
)"
;
"<format>
s
elect input format (default:
\"
why
\"
)"
;
"--format"
,
Arg
.
String
(
fun
s
->
opt_parser
:=
Some
s
)
,
" same as -F"
;
"-D"
,
Arg
.
String
(
fun
s
->
opt_driver
:=
Some
s
)
,
"<file>
S
pecify a realization driver"
;
"<file>
s
pecify a realization driver"
;
"--driver"
,
Arg
.
String
(
fun
s
->
opt_driver
:=
Some
s
)
,
" same as -D"
;
"-o"
,
Arg
.
String
(
fun
s
->
opt_output
:=
Some
s
)
,
"<dir>
W
rite the realizations in <dir>"
;
"<dir>
w
rite the realizations in <dir>"
;
"--output"
,
Arg
.
String
(
fun
s
->
opt_output
:=
Some
s
)
,
" same as -o"
]
let
(
env
,
config
)
=
Args
.
initialize
option_list
add_opt_file
usage_msg
let
config
,
env
=
Whyconf
.
Args
.
initialize
option_list
add_opt_file
usage_msg
let
()
=
if
Queue
.
is_empty
opt_queue
then
Args
.
exit_with_usage
option_list
usage_msg
if
Queue
.
is_empty
opt_queue
then
Whyconf
.
Args
.
exit_with_usage
option_list
usage_msg
let
opt_output
=
match
!
opt_output
with
...
...
src/tools/why3replay.ml
View file @
96cfbb62
...
...
@@ -62,31 +62,41 @@ let set_opt_smoke = function
|
_
->
assert
false
let
usage_msg
=
Format
.
sprintf
"Usage: %s [options] [<file.why>|<project directory>]"
"Usage:
why3
%s [options] [<file.why>|<project directory>]"
(
Filename
.
basename
Sys
.
argv
.
(
0
))
let
option_list
=
[
(
"-f"
,
Arg
.
Set
opt_force
,
" enforce saving the session after replay"
);
(
"--force"
,
Arg
.
Set
opt_force
,
"
enforce saving the session after replay
"
)
;
"
same as -f
"
);
(
"--obsolete-only"
,
Arg
.
Set
opt_obsolete_only
,
" replay only if session is obsolete"
)
;
(
"-P"
,
Arg
.
String
(
fun
s
->
opt_provers
:=
Whyconf
.
parse_filter_prover
s
::
!
opt_provers
)
,
"<prover> restrict replay to given prover"
);
(
"--prover"
,
Arg
.
String
(
fun
s
->
opt_provers
:=
Whyconf
.
parse_filter_prover
s
::
!
opt_provers
)
,
" same as -P"
);
(
"--smoke-detector"
,
Arg
.
Symbol
([
"none"
;
"top"
;
"deep"
]
,
set_opt_smoke
)
,
" try to detect if the context is self-contradicting"
)
;
(
"--bench"
,
Arg
.
Set
opt_bench
,
" run as bench (experimental)"
);
(
"--prover"
,
Arg
.
String
(
fun
s
->
opt_provers
:=
Whyconf
.
parse_filter_prover
s
::
!
opt_provers
)
,
"<prover> restrict replay to given prover"
);
(
"-s"
,
(
"--no-stats"
,
Arg
.
Clear
opt_stats
,
" do not print statistics"
)
;
(
"-q"
,
Arg
.
Unit
(
fun
()
->
Debug
.
unset_flag
debug
)
,
" run quietly"
)
]
" run quietly"
);
(
"--quiet"
,
Arg
.
Unit
(
fun
()
->
Debug
.
unset_flag
debug
)
,
" same as -q"
)
]
let
add_opt_file
f
=
match
!
opt_file
with
|
Some
_
->
...
...
@@ -94,8 +104,8 @@ let add_opt_file f = match !opt_file with
|
None
->
opt_file
:=
Some
f
let
(
env
,
config
)
=
Args
.
initialize
option_list
add_opt_file
usage_msg
let
config
,
env
=
Whyconf
.
Args
.
initialize
option_list
add_opt_file
usage_msg
(* let () = *)
(* if !opt_smoke <> Session.SD_None && !opt_force then begin *)
...
...
@@ -105,7 +115,7 @@ let (env, config) =
let
fname
=
match
!
opt_file
with
|
None
->
Args
.
exit_with_usage
option_list
usage_msg
|
None
->
Whyconf
.
Args
.
exit_with_usage
option_list
usage_msg
|
Some
f
->
f
let
found_upgraded_prover
=
ref
false
...
...
@@ -342,9 +352,9 @@ let add_to_check_smoke env_session sched =
let
add_to_check
config
some_merge_miss
found_obs
=
match
!
opt_smoke
with
|
SD_None
->
add_to_check_no_smoke
config
some_merge_miss
found_obs
;
|
_
->
|
_
->
assert
(
not
some_merge_miss
);
assert
(
not
found_obs
);
assert
(
not
found_obs
);
add_to_check_smoke
let
transform_smoke
env_session
=
...
...
@@ -394,7 +404,7 @@ let () =
M
.
update_session
~
allow_obsolete
:
true
session
env
config
in
Debug
.
dprintf
debug
" done.@."
;
if
!
opt_obsolete_only
&&
not
found_obs
if
!
opt_obsolete_only
&&
not
found_obs
then
begin
eprintf
"Session is not obsolete, hence not replayed@."
;
...
...
src/tools/why3wc.mll
View file @
96cfbb62
...
...
@@ -238,7 +238,7 @@ and comment n = parse
and read_header = parse
| "(*" { skip_header_comment lexbuf; skip_until_nl lexbuf;
read_header lexbuf }
read_header lexbuf }
| "\n" { () }
| space+ { read_header lexbuf }
<