Revision ad4774b0
Makefile.in | ||
---|---|---|
8 | 8 |
LUSI_MPFR_LIB=include/mpfr_lustre.lusi |
9 | 9 |
LOCAL_BINDIR=bin |
10 | 10 |
LOCAL_DOCDIR=doc/manual |
11 |
BIN_TARGETS = lustrec lustret @lustresf_target@ |
|
11 |
BIN_TARGETS = lustrec lustret lustrev @lustresf_target@
|
|
12 | 12 |
|
13 | 13 |
DEFAULT_TEST_TARGET=COMPIL_LUS\|MAKE\|BIN\|DIFF |
14 | 14 |
DEFAULT_EXCLUDE_TEST=LUSTRET |
... | ... | |
23 | 23 |
@echo Compiling binary lustret |
24 | 24 |
@make -C src lustret |
25 | 25 |
|
26 |
lustrev: |
|
27 |
@echo Compiling binary lustrev |
|
28 |
@make -C src lustrev |
|
29 |
|
|
26 | 30 |
@lustresf@ |
27 | 31 |
|
28 | 32 |
configure: configure.ac |
configure.ac | ||
---|---|---|
55 | 55 |
|
56 | 56 |
# Checks for libraries. |
57 | 57 |
# OCamlgraph |
58 |
AC_MSG_CHECKING(ocaml libraries required)
|
|
58 |
AC_MSG_CHECKING(ocaml libraries required (ocamlgraph cmdliner fmt logs num))
|
|
59 | 59 |
AS_IF([ocamlfind query ocamlgraph cmdliner fmt logs num >/dev/null 2>&1], |
60 | 60 |
[],[AC_MSG_ERROR(A few ocaml library required. opam install ocamlgraph cmdliner fmt logs num should solve the issue)], |
61 | 61 |
) |
... | ... | |
67 | 67 |
[yojson=yes; AC_MSG_RESULT(yes)],[yojson=no; AC_MSG_WARN(Yojson required for lustresf. opam install yojson should solve the issue)], |
68 | 68 |
) |
69 | 69 |
|
70 |
# Seal |
|
71 |
AC_MSG_CHECKING(seal library (optional)) |
|
72 |
AS_IF([ocamlfind query seal >/dev/null 2>&1], |
|
73 |
[seal=yes; AC_MSG_RESULT(yes)],[seal=no; AC_MSG_RESULT(no)], |
|
74 |
) |
|
75 |
AS_IF([test "x$seal" = "xyes"], [ |
|
76 |
AC_SUBST(LUSTREV_SEAL, "(module Seal_verifier.Verifier : VerifierType.S);") |
|
77 |
AC_SUBST(LUSTREV_SEAL_TAG, "<**/*>: package(seal)") |
|
78 |
]) |
|
79 |
|
|
80 |
# z3 |
|
81 |
AC_MSG_CHECKING(z3 library (optional)) |
|
82 |
AS_IF([ocamlfind query z3 >/dev/null 2>&1], |
|
83 |
[z3=yes; AC_MSG_RESULT(yes)],[seal=no; AC_MSG_RESULT(no)], |
|
84 |
) |
|
85 |
AS_IF([test "x$z3" = "xyes"], [ |
|
86 |
AC_SUBST(LUSTREV_ZUSTRE, "(module Zustre_verifier.Verifier : VerifierType.S);") |
|
87 |
AC_SUBST(LUSTREV_Z3_TAG, "<**/*>: package(z3)") |
|
88 |
]) |
|
89 |
|
|
90 |
# Tiny |
|
91 |
AC_MSG_CHECKING(tiny library (optional)) |
|
92 |
AS_IF([ocamlfind query tiny >/dev/null 2>&1], |
|
93 |
[tiny=yes; AC_MSG_RESULT(yes)],[tiny=no; AC_MSG_RESULT(no)], |
|
94 |
) |
|
95 |
AS_IF([test "x$tiny" = "xyes"], [ |
|
96 |
AC_SUBST(LUSTREV_TINY, "(module Tiny_verifier.Verifier : VerifierType.S);") |
|
97 |
AC_SUBST(LUSTREV_TINY_TAG, "<**/*>: package(tiny)") |
|
98 |
]) |
|
99 |
|
|
70 | 100 |
# Salsa |
71 | 101 |
AC_ARG_ENABLE(salsa, [AS_HELP_STRING([--disable-salsa], |
72 | 102 |
[disable Salsa plugin. Enabled by default if available.])]) |
... | ... | |
79 | 109 |
|
80 | 110 |
AS_IF([test "x$enable_salsa" != "xno"], [ |
81 | 111 |
if (test "x$salsa" = xyes ); then |
82 |
AC_SUBST(SALSA, "(module Salsa_plugin.Plugin : PluginType.PluginType);")
|
|
112 |
AC_SUBST(SALSA, "(module Salsa_plugin.Plugin : PluginType.S);")
|
|
83 | 113 |
AC_SUBST(SALSA_TAG, "<**/*.native> or <plugins/salsa/*.cm?> : package(salsa)") |
84 | 114 |
fi |
85 | 115 |
]) |
... | ... | |
156 | 186 |
src/Makefile |
157 | 187 |
src/version.ml |
158 | 188 |
src/pluginList.ml |
189 |
src/verifierList.ml |
|
159 | 190 |
src/_tags |
160 | 191 |
src/ocaml_utils.ml |
161 | 192 |
]) |
... | ... | |
190 | 221 |
AC_MSG_NOTICE([lustresf not available]) |
191 | 222 |
fi |
192 | 223 |
fi |
224 |
AC_MSG_NOTICE(******** Verifiers ********) |
|
225 |
|
|
226 |
if (test "x$seal" = "xyes"); then |
|
227 |
AC_MSG_NOTICE([Seal enabled]) |
|
228 |
else |
|
229 |
AC_MSG_NOTICE([Seal disabled. Require Seal library]) |
|
230 |
fi |
|
231 |
|
|
232 |
if (test "x$z3" = xyes); then |
|
233 |
AC_MSG_NOTICE([Zustre enabled]) |
|
234 |
else |
|
235 |
AC_MSG_NOTICE([Zustre disabled. Require Z3 ocaml library]) |
|
236 |
fi |
|
237 |
|
|
238 |
if (test "x$tiny" = xyes); then |
|
239 |
AC_MSG_NOTICE([Tiny enabled]) |
|
240 |
else |
|
241 |
AC_MSG_NOTICE([Tiny disabled. Require Tiny library]) |
|
242 |
fi |
|
193 | 243 |
|
194 | 244 |
AC_MSG_NOTICE(****** Regression Tests ******) |
195 | 245 |
if (test "x$valid_test_path" = xfalse); then |
src/Makefile.in | ||
---|---|---|
10 | 10 |
LOCAL_BINDIR=../bin |
11 | 11 |
LOCAL_DOCDIR=../doc/manual |
12 | 12 |
|
13 |
all: lustrec lustret |
|
13 |
all: lustrec lustret lustrev
|
|
14 | 14 |
|
15 | 15 |
lustrec: |
16 | 16 |
@echo Compiling binary lustrec |
... | ... | |
24 | 24 |
@mkdir -p $(LOCAL_BINDIR) |
25 | 25 |
@mv _build/main_lustre_testgen.native $(LOCAL_BINDIR)/lustret |
26 | 26 |
|
27 |
lustrev: |
|
28 |
@echo Compiling binary lustrev |
|
29 |
@$(OCAMLBUILD) main_lustre_verifier.native |
|
30 |
@mkdir -p $(LOCAL_BINDIR) |
|
31 |
@mv _build/main_lustre_verifier.native $(LOCAL_BINDIR)/lustrev |
|
32 |
|
|
27 | 33 |
@lustresf_src@ |
28 | 34 |
|
29 | 35 |
doc: |
... | ... | |
47 | 53 |
install: |
48 | 54 |
make -C .. install |
49 | 55 |
|
50 |
.PHONY: compile-lusi doc dot lustrec lustret lustrec.odocl clean install dist-clean tests |
|
56 |
.PHONY: compile-lusi doc dot lustrec lustret lustrev lustrec.odocl clean install dist-clean tests |
src/_tags.in | ||
---|---|---|
10 | 10 |
"plugins/scopes": include |
11 | 11 |
"plugins/mpfr": include |
12 | 12 |
"features/machine_types": include |
13 |
"tools": include |
|
13 | 14 |
"tools/stateflow": include |
14 | 15 |
"tools/stateflow/common": include |
15 | 16 |
"tools/stateflow/semantics": include |
... | ... | |
23 | 24 |
# packages |
24 | 25 |
<**/*.native> : package(ocamlgraph) |
25 | 26 |
<**/*.native> : use_str |
26 |
<**/main_lustre_compiler.native>: use_unix |
|
27 |
<**/main_lustre_testgen.native> : use_unix |
|
28 |
<**/sf_sem.native> : use_unix |
|
27 |
<**/*.native> : use_unix |
|
29 | 28 |
<**/*.native> : package(num) |
30 | 29 |
<**/*.ml> : package(logs) |
31 | 30 |
<**/*.native> : package(logs) |
... | ... | |
45 | 44 |
# Plugin dependencies |
46 | 45 |
@SALSA_TAG@ |
47 | 46 |
|
47 |
# Available solvers |
|
48 |
@LUSTREV_SEAL_TAG@ |
|
49 |
@LUSTREV_TINY_TAG@ |
|
50 |
@LUSTREV_Z3_TAG@ |
|
51 |
|
|
48 | 52 |
# Local Variables: |
49 | 53 |
# mode: conf |
50 | 54 |
# End: |
src/algebraicLoop.ml | ||
---|---|---|
157 | 157 |
(* Clock calculus *) |
158 | 158 |
let _ (*computed_clocks_env*) = Compiler_common.clock_decls clock_env prog in |
159 | 159 |
(* Normalization *) |
160 |
let prog = Normalization.normalize_prog ~backend:!Options.output prog in |
|
160 |
let params = Backends.get_normalization_params () in |
|
161 |
let prog = Normalization.normalize_prog params prog in |
|
161 | 162 |
(* Mini stage 2 : Scheduling *) |
162 | 163 |
let res = Scheduling.schedule_prog prog in |
163 | 164 |
Options.verbose_level := !Options.verbose_level + 2; |
... | ... | |
272 | 273 |
Alarms contain the list of inlining performed or advised for each node. |
273 | 274 |
This could be provided as a feedback to the user. |
274 | 275 |
*) |
275 |
let clean_al prog : program * bool * report = |
|
276 |
let clean_al prog : program_t * bool * report =
|
|
276 | 277 |
let max_inlines = !Options.al_nb_max in |
277 | 278 |
(* We iterate over each node *) |
278 | 279 |
let _, prog, al_list = |
src/backends/backends.ml | ||
---|---|---|
16 | 16 |
| "horn" | "lustre" | "acsl" | "emf" -> true |
17 | 17 |
| _ -> false |
18 | 18 |
|
19 |
|
|
20 |
(* Special treatment of arrows in lustre backend. We want to keep them *) |
|
21 |
let unfold_arrow () = |
|
22 |
match !Options.output with |
|
23 |
| "lustre" -> false |
|
24 |
| _ -> true |
|
25 |
|
|
26 |
(* Forcing ite normalization *) |
|
27 |
let alias_ite () = |
|
28 |
match !Options.output with |
|
29 |
| "emf" -> true |
|
30 |
| _ -> false |
|
31 |
|
|
32 |
(* Forcing basic functions normalization *) |
|
33 |
let alias_internal_fun () = |
|
34 |
match !Options.output with |
|
35 |
| "emf" -> true |
|
36 |
| _ -> false |
|
37 |
|
|
38 |
let get_normalization_params () = { |
|
39 |
Normalization.unfold_arrow_active = unfold_arrow (); |
|
40 |
force_alias_ite = alias_ite (); |
|
41 |
force_alias_internal_fun = alias_internal_fun (); |
|
42 |
} |
|
43 |
|
|
19 | 44 |
|
20 | 45 |
(* Local Variables: *) |
21 | 46 |
(* compile-command: "make -k -C .." *) |
src/compiler_stages.ml | ||
---|---|---|
3 | 3 |
open Compiler_common |
4 | 4 |
open LustreSpec |
5 | 5 |
|
6 |
exception StopPhase1 of program |
|
6 |
exception StopPhase1 of program_t
|
|
7 | 7 |
|
8 | 8 |
let dynamic_checks () = |
9 | 9 |
match !Options.output, !Options.spec with |
... | ... | |
22 | 22 |
begin |
23 | 23 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name); |
24 | 24 |
Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext; |
25 |
Lusic.print_lusic_to_h destname lusic_ext |
|
25 |
if !Options.output = "C" then Lusic.print_lusic_to_h destname lusic_ext
|
|
26 | 26 |
end |
27 | 27 |
else |
28 | 28 |
let lusic = Lusic.read_lusic destname lusic_ext in |
... | ... | |
31 | 31 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name); |
32 | 32 |
Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext; |
33 | 33 |
(*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*) |
34 |
Lusic.print_lusic_to_h destname lusic_ext |
|
34 |
if !Options.output = "C" then Lusic.print_lusic_to_h destname lusic_ext
|
|
35 | 35 |
end |
36 | 36 |
else |
37 | 37 |
begin |
... | ... | |
47 | 47 |
|
48 | 48 |
|
49 | 49 |
(* From prog to prog *) |
50 |
let stage1 prog dirname basename = |
|
50 |
let stage1 params prog dirname basename =
|
|
51 | 51 |
(* Updating parent node information for variables *) |
52 | 52 |
Compiler_common.update_vdecl_parents_prog prog; |
53 | 53 |
|
... | ... | |
175 | 175 |
|
176 | 176 |
(* Normalization phase *) |
177 | 177 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,"); |
178 |
let prog = Normalization.normalize_prog ~backend:!Options.output prog in
|
|
178 |
let prog = Normalization.normalize_prog params prog in
|
|
179 | 179 |
Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog); |
180 | 180 |
|
181 | 181 |
let prog = |
src/corelang.mli | ||
---|---|---|
110 | 110 |
|
111 | 111 |
val add_internal_funs: unit -> unit |
112 | 112 |
|
113 |
val pp_prog_type : Format.formatter -> program -> unit |
|
113 |
val pp_prog_type : Format.formatter -> program_t -> unit
|
|
114 | 114 |
|
115 |
val pp_prog_clock : Format.formatter -> program -> unit |
|
115 |
val pp_prog_clock : Format.formatter -> program_t -> unit
|
|
116 | 116 |
|
117 | 117 |
val const_of_top: top_decl -> const_desc |
118 | 118 |
val node_of_top: top_decl -> node_desc |
... | ... | |
120 | 120 |
val typedef_of_top: top_decl -> typedef_desc |
121 | 121 |
val dependency_of_top: top_decl -> (bool * ident) |
122 | 122 |
|
123 |
val get_nodes : program -> top_decl list |
|
124 |
val get_imported_nodes : program -> top_decl list |
|
125 |
val get_consts : program -> top_decl list |
|
126 |
val get_typedefs: program -> top_decl list |
|
127 |
val get_dependencies : program -> top_decl list |
|
128 |
(* val prog_unfold_consts: program -> program *)
|
|
123 |
val get_nodes : program_t -> top_decl list
|
|
124 |
val get_imported_nodes : program_t -> top_decl list
|
|
125 |
val get_consts : program_t -> top_decl list
|
|
126 |
val get_typedefs: program_t -> top_decl list
|
|
127 |
val get_dependencies : program_t -> top_decl list
|
|
128 |
(* val prog_unfold_consts: program_t -> program_t *)
|
|
129 | 129 |
|
130 | 130 |
val rename_static: (ident -> Dimension.dim_expr) -> type_dec_desc -> type_dec_desc |
131 | 131 |
val rename_carrier: (ident -> ident) -> clock_dec_desc -> clock_dec_desc |
... | ... | |
142 | 142 |
(** val rename_aut f_node f_var aut *) |
143 | 143 |
val rename_aut : (ident -> ident) -> (ident -> ident) -> automata_desc -> automata_desc |
144 | 144 |
(** rename_prog f_node f_var prog *) |
145 |
val rename_prog: (ident -> ident) -> (ident -> ident) -> (ident -> ident) -> program -> program
|
|
145 |
val rename_prog: (ident -> ident) -> (ident -> ident) -> (ident -> ident) -> program_t -> program_t
|
|
146 | 146 |
|
147 | 147 |
val substitute_expr: var_decl list -> eq list -> expr -> expr |
148 | 148 |
|
src/lustreSpec.ml | ||
---|---|---|
211 | 211 |
top_decl_itf: bool; (* header or source file ? *) |
212 | 212 |
top_decl_loc: Location.t} (* the location where it is defined *) |
213 | 213 |
|
214 |
type program = top_decl list |
|
214 |
type program_t = top_decl list
|
|
215 | 215 |
|
216 | 216 |
type dep_t = Dep of |
217 | 217 |
bool |
src/main_lustre_compiler.ml | ||
---|---|---|
71 | 71 |
else |
72 | 72 |
prog |
73 | 73 |
in |
74 |
let params = Backends.get_normalization_params () in |
|
75 |
|
|
74 | 76 |
let prog, dependencies = |
75 | 77 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 1 : Normalisation@,"); |
76 | 78 |
try |
77 |
Compiler_stages.stage1 prog dirname basename |
|
79 |
Compiler_stages.stage1 params prog dirname basename
|
|
78 | 80 |
with Compiler_stages.StopPhase1 prog -> ( |
79 | 81 |
if !Options.lusi then |
80 | 82 |
begin |
src/main_lustre_testgen.ml | ||
---|---|---|
45 | 45 |
|
46 | 46 |
(* Parsing source *) |
47 | 47 |
let prog = parse_source source_name in |
48 |
let prog, dependencies = Compiler_stages.stage1 prog dirname basename in |
|
48 |
let params = Backends.get_normalization_params () in |
|
49 |
let prog, dependencies = Compiler_stages.stage1 params prog dirname basename in |
|
49 | 50 |
|
50 | 51 |
(* Two cases |
51 | 52 |
- generation of coverage conditions |
... | ... | |
73 | 74 |
(2) produced as EMF |
74 | 75 |
*) |
75 | 76 |
Options.output := "emf"; |
76 |
let prog_mcdc = Normalization.normalize_prog ~backend:"emf" prog_mcdc in |
|
77 |
let params = Backends.get_normalization_params () in |
|
78 |
let prog_mcdc = Normalization.normalize_prog params prog_mcdc in |
|
77 | 79 |
let machine_code = Compiler_stages.stage2 prog_mcdc in |
78 | 80 |
let source_emf = source_file ^ ".emf" in |
79 | 81 |
let source_out = open_out source_emf in |
src/main_lustre_verifier.ml | ||
---|---|---|
1 |
(********************************************************************) |
|
2 |
(* *) |
|
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
|
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
|
5 |
(* *) |
|
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
|
7 |
(* under the terms of the GNU Lesser General Public License *) |
|
8 |
(* version 2.1. *) |
|
9 |
(* *) |
|
10 |
(********************************************************************) |
|
11 |
|
|
12 |
open Format |
|
13 |
open Log |
|
14 |
open Compiler_common |
|
15 |
|
|
16 |
open Utils |
|
17 |
open LustreSpec |
|
18 |
|
|
19 |
|
|
20 |
let usage = "Usage: lustrev [options] \x1b[4msource file\x1b[0m" |
|
21 |
|
|
22 |
let extensions = [".ec"; ".lus"; ".lusi"] |
|
23 |
|
|
24 |
|
|
25 |
(* verify a .lus source file |
|
26 |
|
|
27 |
we have multiple "backends" |
|
28 |
- zustre: linked to z3/spacer. Shall preserve the structure and rely on contracts. Produces both a lustre model with new properties, maybe as a lusi with lustre contract, and a JSON summarizing the results and providing tests cases or counter examples if any |
|
29 |
|
|
30 |
- seal: linked to seal. Require global inline and main node |
|
31 |
focuses only on the selected node (the main) |
|
32 |
map the machine code into SEAL datastructure and compute invariants |
|
33 |
- provides the node and its information (typical point of interest for taylor expansion, range for inputs, existing invariants, computation error for the node content) |
|
34 |
- simplification of program through taylor expansion |
|
35 |
- scaling when provided with typical ranges (not required to be sound for the moment) |
|
36 |
- computation of lyapunov invariants |
|
37 |
- returns an annotated node with invariants and a JSON to explain computation |
|
38 |
- could also returns plots |
|
39 |
|
|
40 |
- tiny: linked to tiny library to perform floating point analyses |
|
41 |
shall be provided with ranges for inputs or local variables (memories) |
|
42 |
|
|
43 |
*) |
|
44 |
let rec verify dirname basename extension = |
|
45 |
let source_name = dirname ^ "/" ^ basename ^ extension in |
|
46 |
|
|
47 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 0>"); |
|
48 |
|
|
49 |
(* Parsing source *) |
|
50 |
let prog = parse_source source_name in |
|
51 |
|
|
52 |
(* Checking which solver is active *) |
|
53 |
let verifier = Verifiers.get_active () in |
|
54 |
let module Verifier = (val verifier : VerifierType.S) in |
|
55 |
|
|
56 |
|
|
57 |
(* Normalizing it *) |
|
58 |
let prog, dependencies = |
|
59 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 1 : Normalisation@,"); |
|
60 |
try |
|
61 |
let params = Verifier.get_normalization_params () in |
|
62 |
Compiler_stages.stage1 params prog dirname basename |
|
63 |
with Compiler_stages.StopPhase1 prog -> ( |
|
64 |
assert false |
|
65 |
) |
|
66 |
in |
|
67 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@]@,"); |
|
68 |
Log.report ~level:3 (fun fmt -> fprintf fmt ".. Normalized program:@ %a@ "Printers.pp_prog prog); |
|
69 |
|
|
70 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 2 : Machines generation@,"); |
|
71 |
|
|
72 |
let machine_code = |
|
73 |
Compiler_stages.stage2 prog |
|
74 |
in |
|
75 |
|
|
76 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ "); |
|
77 |
Log.report ~level:3 (fun fmt -> fprintf fmt ".. Generated machines:@ %a@ "Machine_code.pp_machines machine_code); |
|
78 |
|
|
79 |
if Scopes.Plugin.show_scopes () then |
|
80 |
begin |
|
81 |
let all_scopes = Scopes.compute_scopes prog !Options.main_node in |
|
82 |
(* Printing scopes *) |
|
83 |
if !Options.verbose_level >= 1 then |
|
84 |
Format.printf "Possible scopes are:@ "; |
|
85 |
Format.printf "@[<v>%a@ @]@ @?" Scopes.print_scopes all_scopes; |
|
86 |
exit 0 |
|
87 |
|
|
88 |
end; |
|
89 |
|
|
90 |
let machine_code = Plugins.refine_machine_code prog machine_code in |
|
91 |
|
|
92 |
assert (dependencies = []); (* Do not handle deps yet *) |
|
93 |
Verifier.run basename prog machine_code; |
|
94 |
begin |
|
95 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@."); |
|
96 |
(* We stop the process here *) |
|
97 |
exit 0 |
|
98 |
end |
|
99 |
|
|
100 |
|
|
101 |
let anonymous filename = |
|
102 |
let ok_ext, ext = List.fold_left |
|
103 |
(fun (ok, ext) ext' -> |
|
104 |
if not ok && Filename.check_suffix filename ext' then |
|
105 |
true, ext' |
|
106 |
else |
|
107 |
ok, ext) |
|
108 |
(false, "") extensions in |
|
109 |
if ok_ext then |
|
110 |
let dirname = Filename.dirname filename in |
|
111 |
let basename = Filename.chop_suffix (Filename.basename filename) ext in |
|
112 |
verify dirname basename ext |
|
113 |
else |
|
114 |
raise (Arg.Bad ("Can only compile *.lusi, *.lus or *.ec files")) |
|
115 |
|
|
116 |
let _ = |
|
117 |
Global.initialize (); |
|
118 |
Corelang.add_internal_funs (); |
|
119 |
try |
|
120 |
Printexc.record_backtrace true; |
|
121 |
|
|
122 |
let options = Options_management.lustrev_options @ (Verifiers.options ()) in |
|
123 |
|
|
124 |
Arg.parse options anonymous usage |
|
125 |
with |
|
126 |
| Parse.Error _ |
|
127 |
| Types.Error (_,_) | Clocks.Error (_,_) -> exit 1 |
|
128 |
| Corelang.Error (_ (* loc *), kind) (*| Task_set.Error _*) -> exit (Error.return_code kind) |
|
129 |
(* | Causality.Error _ -> exit (Error.return_code Error.AlgebraicLoop) *) |
|
130 |
| Sys_error msg -> (eprintf "Failure: %s@." msg); exit 1 |
|
131 |
| exc -> (track_exception (); raise exc) |
|
132 |
|
|
133 |
(* Local Variables: *) |
|
134 |
(* compile-command:"make -C .." *) |
|
135 |
(* End: *) |
src/normalization.ml | ||
---|---|---|
29 | 29 |
definitions. |
30 | 30 |
*) |
31 | 31 |
|
32 |
(* Two global variables *) |
|
33 |
let unfold_arrow_active = ref true |
|
34 |
let force_alias_ite = ref false |
|
35 |
let force_alias_internal_fun = ref false |
|
32 |
type param_t = |
|
33 |
{ |
|
34 |
unfold_arrow_active: bool; |
|
35 |
force_alias_ite: bool; |
|
36 |
force_alias_internal_fun: bool; |
|
37 |
} |
|
38 |
|
|
39 |
let params = ref |
|
40 |
{ |
|
41 |
unfold_arrow_active = false; |
|
42 |
force_alias_ite = false; |
|
43 |
force_alias_internal_fun =false; |
|
44 |
} |
|
36 | 45 |
|
37 | 46 |
|
38 | 47 |
let expr_true loc ck = |
... | ... | |
230 | 239 |
in |
231 | 240 |
defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) |
232 | 241 |
| Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr |
233 |
&& not (!force_alias_internal_fun || alias_basic) -> |
|
242 |
&& not (!params.force_alias_internal_fun || alias_basic) ->
|
|
234 | 243 |
let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in |
235 | 244 |
defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None)) |
236 | 245 |
| Expr_appl (id, args, r) -> |
... | ... | |
248 | 257 |
let defvars, norm_expr = normalize_expr node [] defvars norm_expr in |
249 | 258 |
normalize_expr ~alias:alias node offsets defvars norm_expr |
250 | 259 |
else |
251 |
mk_expr_alias_opt (alias && (!force_alias_internal_fun || alias_basic |
|
260 |
mk_expr_alias_opt (alias && (!params.force_alias_internal_fun || alias_basic
|
|
252 | 261 |
|| not (Basic_library.is_expr_internal_fun expr))) |
253 | 262 |
node defvars norm_expr |
254 |
| Expr_arrow (e1,e2) when !unfold_arrow_active && not (is_expr_once expr) -> |
|
263 |
| Expr_arrow (e1,e2) when !params.unfold_arrow_active && not (is_expr_once expr) ->
|
|
255 | 264 |
(* Here we differ from Colaco paper: arrows are pushed to the top *) |
256 | 265 |
normalize_expr ~alias:alias node offsets defvars (unfold_arrow expr) |
257 | 266 |
| Expr_arrow (e1,e2) -> |
... | ... | |
328 | 337 |
| Expr_merge (c, hl) -> |
329 | 338 |
let defvars, norm_hl = normalize_branches node offsets defvars hl in |
330 | 339 |
defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) |
331 |
| _ when !force_alias_ite -> |
|
340 |
| _ when !params.force_alias_ite ->
|
|
332 | 341 |
(* Forcing alias creation for then/else expressions *) |
333 | 342 |
let defvars, norm_expr = |
334 | 343 |
normalize_expr ~alias:alias node offsets defvars expr |
... | ... | |
506 | 515 |
decl' |
507 | 516 |
| Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl |
508 | 517 |
|
509 |
let normalize_prog ?(backend="C") decls = |
|
510 |
let old_unfold_arrow_active = !unfold_arrow_active in |
|
511 |
let old_force_alias_ite = !force_alias_ite in |
|
512 |
let old_force_alias_internal_fun = !force_alias_internal_fun in |
|
513 |
|
|
518 |
let normalize_prog p decls = |
|
514 | 519 |
(* Backend specific configurations for normalization *) |
515 |
let _ = |
|
516 |
match backend with |
|
517 |
| "lustre" -> |
|
518 |
(* Special treatment of arrows in lustre backend. We want to keep them *) |
|
519 |
unfold_arrow_active := false; |
|
520 |
| "emf" -> ( |
|
521 |
(* Forcing ite normalization *) |
|
522 |
force_alias_ite := true; |
|
523 |
force_alias_internal_fun := true; |
|
524 |
) |
|
525 |
| _ -> () (* No fancy options for other backends *) |
|
526 |
in |
|
520 |
params := p; |
|
527 | 521 |
|
528 | 522 |
(* Main algorithm: iterates over nodes *) |
529 |
let res = List.map normalize_decl decls in |
|
530 |
|
|
531 |
(* Restoring previous settings *) |
|
532 |
unfold_arrow_active := old_unfold_arrow_active; |
|
533 |
force_alias_ite := old_force_alias_ite; |
|
534 |
force_alias_internal_fun := old_force_alias_internal_fun; |
|
535 |
res |
|
536 |
|
|
537 |
(* Local Variables: *) |
|
538 |
(* compile-command:"make -C .." *) |
|
539 |
(* End: *) |
|
523 |
List.map normalize_decl decls |
|
524 |
|
|
525 |
|
|
526 |
(* Local Variables: *) |
|
527 |
(* compile-command:"make -C .." *) |
|
528 |
(* End: *) |
|
529 |
|
src/options_management.ml | ||
---|---|---|
135 | 135 |
"-no-mutation-suffix", Arg.Set no_mutation_suffix, "does not rename node with the _mutant suffix" |
136 | 136 |
] |
137 | 137 |
|
138 |
let lustrev_options = |
|
139 |
common_options @ |
|
140 |
[ |
|
141 |
"-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inlines all node calls (require a main node). Implies constant unfolding"; |
|
142 |
"-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>"; |
|
143 |
] |
|
144 |
|
|
145 |
|
|
138 | 146 |
let plugin_opt (name, activate, options) = |
139 | 147 |
( "-" ^ name , Arg.Unit activate, "activate plugin " ^ name ) :: |
140 | 148 |
(List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options) |
141 | 149 |
|
150 |
let verifier_opt (name, activate, options) = |
|
151 |
( "-" ^ name , Arg.Unit activate, "run verifier " ^ name ) :: |
|
152 |
(List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options) |
|
142 | 153 |
|
143 | 154 |
let get_witness_dir filename = |
144 | 155 |
(* Make sure the directory exists *) |
src/pluginList.ml.in | ||
---|---|---|
1 | 1 |
let plugins = |
2 | 2 |
[ |
3 |
(module Scopes.Plugin : PluginType.PluginType);
|
|
3 |
(module Scopes.Plugin : PluginType.S);
|
|
4 | 4 |
@SALSA@ |
5 | 5 |
] |
src/pluginType.ml | ||
---|---|---|
1 |
module type PluginType =
|
|
1 |
module type S =
|
|
2 | 2 |
sig |
3 | 3 |
val name: string |
4 | 4 |
val activate: unit -> unit |
src/plugins.ml | ||
---|---|---|
7 | 7 |
List.flatten ( |
8 | 8 |
List.map Options_management.plugin_opt ( |
9 | 9 |
List.map (fun m -> |
10 |
let module M = (val m : PluginType.PluginType) in
|
|
10 |
let module M = (val m : PluginType.S) in
|
|
11 | 11 |
(M.name, M.activate, M.options) |
12 | 12 |
) plugins |
13 | 13 |
)) |
14 | 14 |
|
15 | 15 |
let check_force_stateful () = |
16 | 16 |
List.exists (fun m -> |
17 |
let module M = (val m : PluginType.PluginType) in
|
|
17 |
let module M = (val m : PluginType.S) in
|
|
18 | 18 |
M.check_force_stateful () |
19 | 19 |
) plugins |
20 | 20 |
|
21 | 21 |
let refine_machine_code prog machine_code = |
22 | 22 |
List.fold_left (fun accu m -> |
23 |
let module M = (val m : PluginType.PluginType) in
|
|
23 |
let module M = (val m : PluginType.S) in
|
|
24 | 24 |
M.refine_machine_code prog accu |
25 | 25 |
) machine_code plugins |
26 | 26 |
|
27 | 27 |
|
28 | 28 |
let c_backend_main_loop_body_prefix basename mname fmt () = |
29 |
List.iter (fun (m: (module PluginType.PluginType)) ->
|
|
30 |
let module M = (val m : PluginType.PluginType) in
|
|
29 |
List.iter (fun (m: (module PluginType.S)) ->
|
|
30 |
let module M = (val m : PluginType.S) in
|
|
31 | 31 |
M.c_backend_main_loop_body_prefix basename mname fmt ()) plugins |
32 | 32 |
|
33 | 33 |
let c_backend_main_loop_body_suffix fmt () = |
34 |
List.iter (fun (m: (module PluginType.PluginType)) ->
|
|
35 |
let module M = (val m : PluginType.PluginType) in
|
|
34 |
List.iter (fun (m: (module PluginType.S)) ->
|
|
35 |
let module M = (val m : PluginType.S) in
|
|
36 | 36 |
M.c_backend_main_loop_body_suffix fmt ()) plugins |
37 | 37 |
|
38 | 38 |
(* Specific treatment of annotations when inlining, specific of declared plugins *) |
src/plugins/salsa/salsa_plugin.ml | ||
---|---|---|
39 | 39 |
machine_code |
40 | 40 |
|
41 | 41 |
|
42 |
end: PluginType.PluginType) |
|
42 |
end: PluginType.S) |
src/plugins/scopes/scopes.ml | ||
---|---|---|
239 | 239 |
|
240 | 240 |
module Plugin : ( |
241 | 241 |
sig |
242 |
include PluginType.PluginType
|
|
242 |
include PluginType.S
|
|
243 | 243 |
val show_scopes: unit -> bool |
244 | 244 |
end) = |
245 | 245 |
struct |
src/tools/seal_verifier.ml | ||
---|---|---|
1 |
let active = ref false |
|
2 |
|
|
3 |
module Verifier = |
|
4 |
(struct |
|
5 |
include VerifierType.Default |
|
6 |
let name = "seal" |
|
7 |
let options = [] |
|
8 |
let activate () = active := true |
|
9 |
let is_active () = !active |
|
10 |
let run basename prog machines = () |
|
11 |
|
|
12 |
end: VerifierType.S) |
|
13 |
|
src/tools/stateflow/semantics/cPS_lustre_generator.ml | ||
---|---|---|
321 | 321 |
in tr |
322 | 322 |
|
323 | 323 |
let mkcomponent : |
324 |
type c. c call_t -> c -> t -> LustreSpec.program = |
|
324 |
type c. c call_t -> c -> t -> LustreSpec.program_t =
|
|
325 | 325 |
fun call args -> |
326 | 326 |
fun tr -> |
327 | 327 |
reset_loc (); |
src/tools/stateflow/semantics/cPS_transformer.ml | ||
---|---|---|
78 | 78 |
val eval_act : (module ThetaType with type t = t) -> act_t -> t |
79 | 79 |
val eval_cond : cond_t -> t -> t -> t |
80 | 80 |
(* val mktransformer : t -> unit *) |
81 |
val mkprincipal : t -> LustreSpec.program |
|
82 |
val mkcomponent : 'c call_t -> 'c -> t -> LustreSpec.program |
|
81 |
val mkprincipal : t -> LustreSpec.program_t
|
|
82 |
val mkcomponent : 'c call_t -> 'c -> t -> LustreSpec.program_t
|
|
83 | 83 |
end |
84 | 84 |
|
85 | 85 |
module type ComparableTransformerType = |
src/tools/stateflow/sf_sem.ml | ||
---|---|---|
80 | 80 |
let auto_out = open_out auto_file in |
81 | 81 |
let auto_fmt = Format.formatter_of_out_channel auto_out in |
82 | 82 |
Format.fprintf auto_fmt "%a@." Printers.pp_prog prog; |
83 |
|
|
84 |
let prog, deps = Compiler_stages.stage1 prog "" "" in |
|
83 |
|
|
84 |
let params = Backends.get_normalization_params () in |
|
85 |
let prog, deps = Compiler_stages.stage1 params prog "" "" in |
|
85 | 86 |
|
86 | 87 |
Format.printf "%a@." Printers.pp_prog prog; |
87 | 88 |
let noauto_file = "sf_gen_test_noauto.lus" in (* Could be changed *) |
src/tools/zustre_verifier.ml | ||
---|---|---|
1 |
open LustreSpec |
|
2 |
open Machine_code |
|
3 |
open Format |
|
4 |
open Horn_backend_common |
|
5 |
open Horn_backend |
|
6 |
|
|
7 |
let active = ref false |
|
8 |
let ctx = ref (Z3.mk_context []) |
|
9 |
|
|
10 |
let bool_sort = Z3.Boolean.mk_sort !ctx |
|
11 |
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx |
|
12 |
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx |
|
13 |
|
|
14 |
let const_sorts = Hashtbl.create 13 |
|
15 |
let get_const_sort ty_name = |
|
16 |
Hashtbl.find const_sorts ty_name |
|
17 |
|
|
18 |
let decl_sorts () = |
|
19 |
Hashtbl.iter (fun typ decl -> |
|
20 |
match typ with |
|
21 |
| Tydec_const var -> |
|
22 |
(match decl.top_decl_desc with |
|
23 |
| TypeDef tdef -> ( |
|
24 |
match tdef.tydef_desc with |
|
25 |
| Tydec_enum tl -> |
|
26 |
let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in |
|
27 |
Hashtbl.add const_sorts var new_sort |
|
28 |
| _ -> assert false |
|
29 |
) |
|
30 |
| _ -> assert false |
|
31 |
) |
|
32 |
| _ -> ()) Corelang.type_table |
|
33 |
|
|
34 |
|
|
35 |
let rec type_to_sort t = |
|
36 |
if Types.is_bool_type t then bool_sort else |
|
37 |
if Types.is_int_type t then int_sort else |
|
38 |
if Types.is_real_type t then real_sort else |
|
39 |
match (Types.repr t).Types.tdesc with |
|
40 |
| Types.Tconst ty -> get_const_sort ty |
|
41 |
| Types.Tclock t -> type_to_sort t |
|
42 |
| Types.Tarray(dim,ty) -> Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty) |
|
43 |
| Types.Tstatic(d, ty)-> type_to_sort ty |
|
44 |
| Types.Tarrow _ |
|
45 |
| _ -> Format.eprintf "internal error: pp_type %a@." |
|
46 |
Types.print_ty t; assert false |
|
47 |
|
|
48 |
|
|
49 |
let decl_var id = |
|
50 |
Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) |
|
51 |
|
|
52 |
let decl_machine machines m = |
|
53 |
if m.Machine_code.mname.node_id = Machine_code.arrow_id then |
|
54 |
(* We don't print arrow function *) |
|
55 |
() |
|
56 |
else |
|
57 |
begin |
|
58 |
let _ = List.map decl_var |
|
59 |
( |
|
60 |
(inout_vars machines m)@ |
|
61 |
(rename_current_list (full_memory_vars machines m)) @ |
|
62 |
(rename_mid_list (full_memory_vars machines m)) @ |
|
63 |
(rename_next_list (full_memory_vars machines m)) @ |
|
64 |
(rename_machine_list m.mname.node_id m.mstep.step_locals) |
|
65 |
) |
|
66 |
in |
|
67 |
() |
|
68 |
(* |
|
69 |
if is_stateless m then |
|
70 |
begin |
|
71 |
(* Declaring single predicate *) |
|
72 |
fprintf fmt "(declare-rel %a (%a))@." |
|
73 |
pp_machine_stateless_name m.mname.node_id |
|
74 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
75 |
(List.map (fun v -> v.var_type) (inout_vars machines m)); |
|
76 |
|
|
77 |
match m.mstep.step_asserts with |
|
78 |
| [] -> |
|
79 |
begin |
|
80 |
|
|
81 |
(* Rule for single predicate *) |
|
82 |
fprintf fmt "; Stateless step rule @."; |
|
83 |
fprintf fmt "@[<v 2>(rule (=> @ "; |
|
84 |
ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) ) m fmt m.mstep.step_instrs); |
|
85 |
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." |
|
86 |
pp_machine_stateless_name m.mname.node_id |
|
87 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_vars machines m); |
|
88 |
end |
|
89 |
| assertsl -> |
|
90 |
begin |
|
91 |
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in |
|
92 |
|
|
93 |
fprintf fmt "; Stateless step rule with Assertions @."; |
|
94 |
(*Rule for step*) |
|
95 |
fprintf fmt "@[<v 2>(rule (=> @ (and @ "; |
|
96 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
|
97 |
fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl |
|
98 |
pp_machine_stateless_name m.mname.node_id |
|
99 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m); |
|
100 |
|
|
101 |
end |
|
102 |
|
|
103 |
end |
|
104 |
else |
|
105 |
begin |
|
106 |
(* Declaring predicate *) |
|
107 |
fprintf fmt "(declare-rel %a (%a))@." |
|
108 |
pp_machine_reset_name m.mname.node_id |
|
109 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
110 |
(List.map (fun v -> v.var_type) (reset_vars machines m)); |
|
111 |
|
|
112 |
fprintf fmt "(declare-rel %a (%a))@." |
|
113 |
pp_machine_step_name m.mname.node_id |
|
114 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
115 |
(List.map (fun v -> v.var_type) (step_vars machines m)); |
|
116 |
|
|
117 |
pp_print_newline fmt (); |
|
118 |
|
|
119 |
(* Rule for reset *) |
|
120 |
fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@." |
|
121 |
(pp_machine_reset machines) m |
|
122 |
pp_machine_reset_name m.mname.node_id |
|
123 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m); |
|
124 |
|
|
125 |
match m.mstep.step_asserts with |
|
126 |
| [] -> |
|
127 |
begin |
|
128 |
fprintf fmt "; Step rule @."; |
|
129 |
(* Rule for step*) |
|
130 |
fprintf fmt "@[<v 2>(rule (=> @ "; |
|
131 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
|
132 |
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." |
|
133 |
pp_machine_step_name m.mname.node_id |
|
134 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m); |
|
135 |
end |
|
136 |
| assertsl -> |
|
137 |
begin |
|
138 |
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in |
|
139 |
(* print_string pp_val; *) |
|
140 |
fprintf fmt "; Step rule with Assertions @."; |
|
141 |
|
|
142 |
(*Rule for step*) |
|
143 |
fprintf fmt "@[<v 2>(rule (=> @ (and @ "; |
|
144 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
|
145 |
fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl |
|
146 |
pp_machine_step_name m.mname.node_id |
|
147 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m); |
|
148 |
end |
|
149 |
|
|
150 |
|
|
151 |
end |
|
152 |
*) end |
|
153 |
|
|
154 |
|
|
155 |
module Verifier = |
|
156 |
(struct |
|
157 |
include VerifierType.Default |
|
158 |
let name = "zustre" |
|
159 |
let options = [] |
|
160 |
let activate () = ( |
|
161 |
active := true; |
|
162 |
Options.output := "horn"; |
|
163 |
) |
|
164 |
let is_active () = !active |
|
165 |
|
|
166 |
let get_normalization_params () = |
|
167 |
(* make sure the output is "Horn" *) |
|
168 |
assert(!Options.output = "horn"); |
|
169 |
Backends.get_normalization_params () |
|
170 |
|
|
171 |
let run basename prog machines = |
|
172 |
let machines = Machine_code.arrow_machine::machines in |
|
173 |
let machines = preprocess machines in |
|
174 |
decl_sorts (); |
|
175 |
List.iter (decl_machine machines) (List.rev machines); |
|
176 |
|
|
177 |
|
|
178 |
() |
|
179 |
|
|
180 |
end: VerifierType.S) |
|
181 |
|
src/verifierList.ml.in | ||
---|---|---|
1 |
let verifiers = |
|
2 |
[ |
|
3 |
@LUSTREV_SEAL@ |
|
4 |
@LUSTREV_ZUSTRE@ |
|
5 |
@LUSTREV_TINY@ |
|
6 |
] |
src/verifierType.ml | ||
---|---|---|
1 |
module type S = |
|
2 |
sig |
|
3 |
val name: string |
|
4 |
val activate: unit -> unit |
|
5 |
val is_active: unit -> bool |
|
6 |
val options: (string * Arg.spec * string) list |
|
7 |
val get_normalization_params: unit -> Normalization.param_t |
|
8 |
val run: string -> LustreSpec.program_t -> Machine_code.machine_t list -> unit |
|
9 |
end |
|
10 |
|
|
11 |
module Default = |
|
12 |
struct |
|
13 |
|
|
14 |
let get_normalization_params () = { |
|
15 |
Normalization.unfold_arrow_active = true; |
|
16 |
force_alias_ite = false; |
|
17 |
force_alias_internal_fun = false; |
|
18 |
} |
|
19 |
|
|
20 |
end |
src/verifiers.ml | ||
---|---|---|
1 |
open LustreSpec |
|
2 |
|
|
3 |
open VerifierList |
|
4 |
|
|
5 |
let active = ref None |
|
6 |
|
|
7 |
let options () = |
|
8 |
List.flatten ( |
|
9 |
List.map Options_management.verifier_opt ( |
|
10 |
List.map (fun m -> |
|
11 |
let module M = (val m : VerifierType.S) in |
|
12 |
(M.name, M.activate, M.options) |
|
13 |
) verifiers |
|
14 |
)) |
|
15 |
|
|
16 |
let verifier_list verifiers = |
|
17 |
List.fold_left (fun acc m -> |
|
18 |
let module M = (val m : VerifierType.S) in |
|
19 |
(if acc = "" then "" else acc ^ ", ") ^ M.name |
|
20 |
) "" verifiers |
|
21 |
|
|
22 |
let get_active () = |
|
23 |
match !active with |
|
24 |
| None -> |
|
25 |
begin |
|
26 |
(* check that a single one is active and register it *) |
|
27 |
let found = |
|
28 |
List.fold_left (fun found m -> |
|
29 |
let module M = (val m : VerifierType.S) in |
|
30 |
if M.is_active () then |
|
31 |
m::found |
|
32 |
else |
|
33 |
found |
|
34 |
) [] verifiers |
|
35 |
in |
|
36 |
match found with |
|
37 |
| [] -> raise (Sys_error ("Please select one verifier in " ^ verifier_list verifiers)) |
|
38 |
| [m] -> active := Some m; m |
|
39 |
| _ -> raise (Sys_error ("Too many selected verifiers: " ^ verifier_list found)) |
|
40 |
end |
|
41 |
|
|
42 |
| Some m -> m |
|
43 |
|
|
44 |
|
|
45 |
|
|
46 |
(* Local Variables: *) |
|
47 |
(* compile-command:"make -C .." *) |
|
48 |
(* End: *) |
Also available in: Unified diff