Skip to content

GitLab

why3
why3

Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 9deea655 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files
Options

Factor option parsing for why3 commands.

parent 74e9e7b3
Hide whitespace changes
Inline Side-by-side
Showing with 113 additions and 51 deletions
Makefile.in
View file @ 9deea655
......@@ -429,11 +429,8 @@ src/tools/main.cmx: lib/why3/why3.cmxa
src/tools/why3contraption.cmo: lib/why3/why3.cma
src/tools/why3contraption.cmx: lib/why3/why3.cmxa
src/tools/why3prove.cmo: lib/why3/why3.cma
src/tools/why3prove.cmx: lib/why3/why3.cmxa
byte: bin/why3.byte bin/why3contraption.byte bin/why3prove.byte
opt: bin/why3.opt bin/why3contraption.opt bin/why3prove.opt
byte: bin/why3.byte bin/why3contraption.byte
opt: bin/why3.opt bin/why3contraption.opt
bin/why3.opt: lib/why3/why3.cmxa src/tools/main.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
......@@ -457,11 +454,52 @@ bin/why3contraption.byte: lib/why3/why3.cma src/tools/why3contraption.cmo
bin/why3contraption: bin/why3contraption.@OCAMLBEST@
ln -sf why3contraption.@OCAMLBEST@ $@
bin/why3prove.opt: lib/why3/why3.cmxa src/tools/why3prove.cmx
clean_old_install::
rm -f $(BINDIR)/why3$(EXE) $(BINDIR)/why3contraption$(EXE)
install_no_local::
cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
cp -f bin/why3contraption.@OCAMLBEST@ $(BINDIR)/why3contraption$(EXE)
install_local: bin/why3 bin/why3contraption bin/why3prove
ifneq "$(MAKECMDGOALS)" "clean"
include src/tools/main.dep
include src/tools/why3contraption.dep
include src/tools/why3prove.dep
endif
depend: src/tools/main.dep src/tools/why3contraption.dep
clean::
rm -f src/tools/main.cm[iox] src/tools/main.annot src/tools/main.o src/tools/main.dep
rm -f src/tools/why3contraption.cm[iox] src/tools/why3contraption.annot src/tools/why3contraption.o src/tools/why3contraption.dep
rm -f bin/why3.byte bin/why3.opt bin/why3
rm -f bin/why3contraption.byte bin/why3contraption.opt bin/why3contraption
###############
# Why3 commands
###############
TOOLS_FILES = args why3prove
TOOLSMODULES = $(addprefix src/tools/, $(TOOLS_FILES))
TOOLSDEP = $(addsuffix .dep, $(TOOLSMODULES))
TOOLSCMO = $(addsuffix .cmo, $(TOOLSMODULES))
TOOLSCMX = $(addsuffix .cmx, $(TOOLSMODULES))
$(TOOLSDEP): DEPFLAGS += -I src/tools
$(TOOLSCMO) $(TOOLSCMX): INCLUDES += -I src/tools
byte: bin/why3prove.byte
opt: bin/why3prove.opt
bin/why3prove.opt: lib/why3/why3.cmxa src/tools/args.cmx src/tools/why3prove.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3prove.byte: lib/why3/why3.cma src/tools/why3prove.cmo
bin/why3prove.byte: lib/why3/why3.cma src/tools/args.cmo src/tools/why3prove.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
......@@ -469,29 +507,22 @@ bin/why3prove: bin/why3prove.@OCAMLBEST@
ln -sf why3prove.@OCAMLBEST@ $@
clean_old_install::
rm -f $(BINDIR)/why3$(EXE) $(BINDIR)/why3contraption$(EXE) $(BINDIR)/why3prove$(EXE)
rm -f $(TOOLDIR)/why3prove$(EXE)
install_no_local::
cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
cp -f bin/why3contraption.@OCAMLBEST@ $(BINDIR)/why3contraption$(EXE)
cp -f bin/why3prove.@OCAMLBEST@ $(TOOLDIR)/why3prove$(EXE)
install_local: bin/why3 bin/why3contraption bin/why3prove
install_local: bin/why3prove
ifneq "$(MAKECMDGOALS)" "clean"
include src/tools/main.dep
include src/tools/why3contraption.dep
include src/tools/why3prove.dep
include $(TOOLSDEP)
endif
depend: src/tools/main.dep src/tools/why3contraption.dep src/tools/why3prove.dep
depend: $(TOOLSDEP)
clean::
rm -f src/tools/main.cm[iox] src/tools/main.annot src/tools/main.o src/tools/main.dep
rm -f src/tools/why3contraption.cm[iox] src/tools/why3contraption.annot src/tools/why3contraption.o src/tools/why3contraption.dep
rm -f src/tools/args.cm[iox] src/tools/args.annot src/tools/args.o src/tools/args.dep
rm -f src/tools/why3prove.cm[iox] src/tools/why3prove.annot src/tools/why3prove.o src/tools/why3prove.dep
rm -f bin/why3.byte bin/why3.opt bin/why3
rm -f bin/why3contraption.byte bin/why3contraption.opt bin/why3contraption
rm -f bin/why3prove.byte bin/why3prove.opt bin/why3prove
##############
......
src/tools/args.ml 0 → 100644
View file @ 9deea655
(********************************************************************)
(* *)
(* 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 common_options = [
"-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_list;
Debug.Args.desc_debug_all;
Debug.Args.desc_debug ]
let initialize options default usage =
Arg.parse (Arg.align (List.append options common_options)) default usage;
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 ();
let lp = List.rev_append !opt_loadpath (Whyconf.loadpath main) in
(Env.create_env lp, config)
src/tools/args.mli 0 → 100644
View file @ 9deea655
(********************************************************************)
(* *)
(* 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 : (string * Arg.spec * string) list ->
(string -> unit) -> string -> Env.env * Whyconf.config
src/tools/why3prove.ml
View file @ 9deea655
......@@ -80,11 +80,8 @@ let add_opt_meta meta =
in
opt_metas := (meta_name,meta_arg)::!opt_metas
let opt_config = ref None
let opt_extra = ref []
let opt_parser = ref None
let opt_prover = ref None
let opt_loadpath = ref []
let opt_driver = ref None
let opt_output = ref None
let opt_timelimit = ref None
......@@ -95,9 +92,7 @@ let opt_task = ref None
let opt_print_theory = ref false
let opt_print_namespace = ref false
let opt_version = ref false
let option_list = Arg.align [
let option_list = [
"-", Arg.Unit (fun () -> add_opt_file "-"),
" Read the input file from stdin";
"-T", Arg.String add_opt_theory,
......@@ -108,16 +103,6 @@ let option_list = Arg.align [
"<goal> Select <goal> in the last selected theory";
"--goal", Arg.String add_opt_goal,
" same as -G";
"-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";
"-P", Arg.String (fun s -> opt_prover := Some s),
"<prover> Prove or print (with -o) the selected goals";
"--prover", Arg.String (fun s -> opt_prover := Some s),
......@@ -154,24 +139,14 @@ let option_list = Arg.align [
" Print selected theories";
"--print-namespace", Arg.Set opt_print_namespace,
" Print namespaces of selected theories";
Debug.Args.desc_debug_list;
Debug.Args.desc_shortcut "parse_only" "--parse-only" " Stop after parsing";
Debug.Args.desc_shortcut
"type_only" "--type-only" " Stop after type checking";
Debug.Args.desc_debug_all;
Debug.Args.desc_debug ]
let () = try
Arg.parse option_list add_opt_file usage_msg;
"type_only" "--type-only" " Stop after type checking" ]
(** Configuration *)
let config = read_config !opt_config in
let config = List.fold_left merge_config config !opt_extra in
let main = get_main config in
Whyconf.load_plugins main;
Debug.Args.set_flags_selected ();
let (env, config) =
Args.initialize option_list add_opt_file usage_msg
let () = try
if Queue.is_empty opt_queue then begin
Arg.usage option_list usage_msg;
exit 1
......@@ -202,7 +177,8 @@ let () = try
opt_print_theory := true
end;
opt_loadpath := List.rev_append !opt_loadpath (Whyconf.loadpath main);
let main = Whyconf.get_main config in
if !opt_timelimit = None then opt_timelimit := Some (Whyconf.timelimit main);
if !opt_memlimit = None then opt_memlimit := Some (Whyconf.memlimit main);
begin match !opt_prover with
......@@ -411,7 +387,6 @@ let load_driver_extract env s =
let () =
try
let env = Env.create_env !opt_loadpath in
let drv = Opt.map (load_driver env) !opt_driver in
Queue.iter (do_input env drv) opt_queue
with e when not (Debug.test_flag Debug.stack_trace) ->
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment