diff --git a/src/machine_code.ml b/src/machine_code.ml index 29851744e92dd2b9ef114a007dd14da158832d79..17f91d2f6a8ad6db45821b0958b8082285e1e741 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 f843223d406664f5d7736247811e0e0c1f8056a9..82fcd9585d2ea8f9c6bfef32d78ba56f9a135dba 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 a801b8a031176238dfca8592a97cd73396d45d48..04c91085eeb7504a1783d0dd2e98242d2c375906 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 4acbc8982789dd7deb22ac2e93c5d7fb4ab05079..ebfa7ce74582a2581cbabfed85e3c286f5901975 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 e27c5b538049b9715aae197c351d5c61cc28d5de..fb7acccda959b0b501c7fee41a766ef4f172c41a 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 }