From 7eac66b1e983d8cafd2fc0cfada42d011a8b1a7b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lelio.brun@isae-supaero.fr>
Date: Fri, 4 Mar 2022 16:43:59 +0100
Subject: [PATCH] flag for contracts compilation
---
src/machine_code.ml | 2 +-
src/options.ml | 3 +++
src/options.mli | 2 ++
src/options_management.ml | 5 ++++-
src/parsers/lexer_lustre.mll | 32 ++++++++++++++++++--------------
5 files changed, 28 insertions(+), 16 deletions(-)
diff --git a/src/machine_code.ml b/src/machine_code.ml
index 29851744..17f91d2f 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -440,7 +440,7 @@ let translate_eq env ctx nd mems inputs locals outputs i eq =
let instr, spec = translate_act (var_x, eq.eq_rhs) in
control_on_clock eq.eq_rhs.expr_clock instr false None spec ctx
with Not_found ->
- Format.eprintf "ERROR: node %s, eq %a@." id Printers.pp_node_eq eq;
+ Format.eprintf "ERROR: node %s, eq %a : unknown variable %s@." id Printers.pp_node_eq eq x;
raise Not_found)
| _ ->
Format.eprintf
diff --git a/src/options.ml b/src/options.ml
index f843223d..82fcd958 100644
--- a/src/options.ml
+++ b/src/options.ml
@@ -118,6 +118,9 @@ let kind2_print = ref false
(* C main options *)
let c_main_options = ref false
+(* compile contracts into acsl *)
+let compile_contracts = ref false
+
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
diff --git a/src/options.mli b/src/options.mli
index a801b8a0..04c91085 100644
--- a/src/options.mli
+++ b/src/options.mli
@@ -86,3 +86,5 @@ val compile_header : bool ref
val track_exceptions : bool ref
val c_main_options : bool ref
+
+val compile_contracts : bool ref
diff --git a/src/options_management.ml b/src/options_management.ml
index 4acbc898..ebfa7ce7 100644
--- a/src/options_management.ml
+++ b/src/options_management.ml
@@ -222,9 +222,12 @@ let lustrec_options =
cpp := true;
static_mem := false),
"generates the mauve code" );
- ( "-c_main_options",
+ ( "-c-main-options",
Arg.Set c_main_options,
"instrument the main C code with command line options" );
+ ( "-compile-contracts",
+ Arg.Set compile_contracts,
+ "compile Lustre contracts" );
]
let lustret_options =
diff --git a/src/parsers/lexer_lustre.mll b/src/parsers/lexer_lustre.mll
index e27c5b53..fb7acccd 100644
--- a/src/parsers/lexer_lustre.mll
+++ b/src/parsers/lexer_lustre.mll
@@ -118,17 +118,21 @@ let newline token lexbuf =
Lex.newline lexbuf;
token lexbuf
-let make_annot orig_loc s =
- let lexbuf = Lexing.from_string s in
- let f = Location.filename_of orig_loc in
- ANNOT (Parse.parse (module LexerLustreSpec) ~orig_loc f s lexbuf
- Parser_lustre.lustre_annot Parse.Inc.lustre_annot)
+let make_annot token orig_lexbuf orig_loc s =
+ if !Options.compile_contracts then
+ let lexbuf = Lexing.from_string s in
+ let f = Location.filename_of orig_loc in
+ ANNOT (Parse.parse (module LexerLustreSpec) ~orig_loc f s lexbuf
+ Parser_lustre.lustre_annot Parse.Inc.lustre_annot)
+ else token orig_lexbuf
-let make_spec orig_loc s =
- let lexbuf = Lexing.from_string s in
- let f = Location.filename_of orig_loc in
- NODESPEC (Parse.parse (module LexerLustreSpec) ~orig_loc f s lexbuf
- Parser_lustre.lustre_spec Parse.Inc.lustre_spec)
+let make_spec token orig_lexbuf orig_loc s =
+ if !Options.compile_contracts then
+ let lexbuf = Lexing.from_string s in
+ let f = Location.filename_of orig_loc in
+ NODESPEC (Parse.parse (module LexerLustreSpec) ~orig_loc f s lexbuf
+ Parser_lustre.lustre_spec Parse.Inc.lustre_spec)
+ else token orig_lexbuf
}
let newline = ('\010' | '\013' | "\013\010")
@@ -138,16 +142,16 @@ let blank = [' ' '\009' '\012']
rule token = parse
| "--@" { Buffer.clear buf;
let loc = Location.curr lexbuf in
- extra_singleline (make_spec loc) lexbuf }
+ extra_singleline (make_spec token lexbuf loc) lexbuf }
| "(*@" { Buffer.clear buf;
let loc = Location.curr lexbuf in
- extra_multiline (make_spec loc) Unfinished_node_spec 0 lexbuf }
+ extra_multiline (make_spec token lexbuf loc) Unfinished_node_spec 0 lexbuf }
| "--!" { Buffer.clear buf;
let loc = Location.curr lexbuf in
- extra_singleline (make_annot loc) lexbuf }
+ extra_singleline (make_annot token lexbuf loc) lexbuf }
| "(*!" { Buffer.clear buf;
let loc = Location.curr lexbuf in
- extra_multiline (make_annot loc) Unfinished_annot 0 lexbuf }
+ extra_multiline (make_annot token lexbuf loc) Unfinished_annot 0 lexbuf }
| "(*" { comment 0 lexbuf }
| "--" [^ '!' '@'] notnewline* (newline|eof)
{ newline token lexbuf }
--
GitLab