diff --git a/compiler/main/heptc.ml b/compiler/main/heptc.ml index 4763329..df6659d 100644 --- a/compiler/main/heptc.ml +++ b/compiler/main/heptc.ml @@ -157,6 +157,8 @@ let main () = "-O", Arg.Unit do_optim, doc_optim; "-mall", Arg.Set interf_all, doc_interf_all; "-time", Arg.Set time_passes, doc_time_passes; + ("-Wno-untranslatable", Arg.Clear warn_untranslatable, + doc_no_warn_untranslat); ] compile errmsg; with diff --git a/compiler/minils/ctrln/ctrlNbacGen.ml b/compiler/minils/ctrln/ctrlNbacGen.ml index f98d1d1..92a2491 100644 --- a/compiler/minils/ctrln/ctrlNbacGen.ml +++ b/compiler/minils/ctrln/ctrlNbacGen.ml @@ -413,7 +413,7 @@ let translate_contract ~pref gd mk_var_dec sink Initial.tbool Linearity.Ltop Clocks.Cbase :: locals) in - let gd = { gd with + let gd = { gd with assertion = mk_and' gd.assertion ak; invariant = mk_and' gd.invariant ok; } in @@ -548,8 +548,9 @@ let gen_ctrlf_calls ~requal_types gd node_name equs = let translate_node ~requal_types typdefs = function | ({ n_contract = None } as node) -> node, None | ({ n_name; n_params } as node) when n_params <> [] -> - warn "Unsupported@ translation@ of@ parametric@ node@ `%s'@ with@ \ - contract@ into@ Controllable-Nbac!" (Names.fullname n_name); + warn ~cond:(!Compiler_options.warn_untranslatable) + "Unsupported@ translation@ of@ parametric@ node@ `%s'@ with@ \ + contract@ into@ Controllable-Nbac!" (Names.fullname n_name); node, None | ({ n_name; n_input; n_output; n_local; n_equs; n_contract = Some contr } as node) -> diff --git a/compiler/minils/sigali/sigalimain.ml b/compiler/minils/sigali/sigalimain.ml index 8fc2f91..3b5de59 100644 --- a/compiler/minils/sigali/sigalimain.ml +++ b/compiler/minils/sigali/sigalimain.ml @@ -44,12 +44,10 @@ type mtype = Tint | Tbool | Tother exception Untranslatable let untranslatable_warn e = - if e.Minils.e_loc <> no_location then - Format.eprintf "Warning: abstracted expression:@.%a" - Location.print_location e.Minils.e_loc - else - Format.eprintf "Warning: abstracted expression: @[%a@]@." - Mls_printer.print_exp e + let warn msg = warn ~cond:(!Compiler_options.warn_untranslatable) msg in + if e.Minils.e_loc <> no_location + then warn "abstracted expression:@.%a" print_location e.Minils.e_loc + else warn "abstracted expression: @[%a@]@." Mls_printer.print_exp e let actual_ty ty = match (Modules.unalias_type ty) with @@ -539,8 +537,9 @@ let program p = | Minils.Pnode(node) as p when node.Minils.n_contract = None -> (acc_proc,p::acc_p_desc) | Minils.Pnode(node) as p when node.Minils.n_params <> [] -> - warn "Unsupported@ translation@ of@ parametric@ node@ `%s'@ with@ \ - contract@ into@ Z/3Z!" (Names.fullname node.Minils.n_name); + warn ~cond:(!Compiler_options.warn_untranslatable) + "Unsupported@ translation@ of@ parametric@ node@ `%s'@ with@ \ + contract@ into@ Z/3Z!" (Names.fullname node.Minils.n_name); (acc_proc,p::acc_p_desc) | Minils.Pnode(node) -> let (node,proc) = translate_node node in diff --git a/compiler/utilities/ctrln/ctrln_utils.ml b/compiler/utilities/ctrln/ctrln_utils.ml index b6aa5ae..1600993 100644 --- a/compiler/utilities/ctrln/ctrln_utils.ml +++ b/compiler/utilities/ctrln/ctrln_utils.ml @@ -61,6 +61,7 @@ let save_controller_modul_for modul = let cm = controller_modul modul in let epci = String.uncapitalize (Names.modul_to_string cm) ^ ".epci" in Modules.select cm; + (* XXX check for empty modules? *) let oc = open_out_bin epci in output_value oc (Modules.current_module ()); close_out oc; diff --git a/compiler/utilities/global/compiler_options.ml b/compiler/utilities/global/compiler_options.ml index e432237..8786ea5 100644 --- a/compiler/utilities/global/compiler_options.ml +++ b/compiler/utilities/global/compiler_options.ml @@ -162,6 +162,7 @@ let do_optim () = tomato := true; deadcode := true +let warn_untranslatable = ref true (* z3z | ctrln *) let check_options () = let err m = raise (Arg.Bad m) in @@ -214,3 +215,4 @@ and doc_optim = "\t\t\tOptimize with deadcode, tomato, itfusion and memalloc" and doc_interf_all = "\t\tPerform memory allocation on all types" and doc_unroll = "\t\tUnroll all loops" and doc_time_passes = "\t\tTime compilation passes" +and doc_no_warn_untranslat = "\tSuppress warnings about untranslatable constructs" diff --git a/compiler/utilities/global/compiler_utils.ml b/compiler/utilities/global/compiler_utils.ml index f0c5eef..489a6e0 100644 --- a/compiler/utilities/global/compiler_utils.ml +++ b/compiler/utilities/global/compiler_utils.ml @@ -59,20 +59,21 @@ let separateur = "\n*********************************************\ let comment ?(sep=separateur) s = if !verbose then Format.printf "%s%s@." sep s -let info: ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a = fun f -> +let info: ('a, formatter, unit, unit) format4 -> 'a = fun f -> if !verbose then - Format.kfprintf (Format.kfprintf (fun fmt -> Format.fprintf fmt "@]@.")) - Format.err_formatter "Info: @[" f - else - Format.ifprintf Format.err_formatter f + kfprintf (kfprintf (fun fmt -> fprintf fmt "@]@.")) err_formatter + "Info: @[" f + else ifprintf err_formatter f -let warn: ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a = fun f -> - Format.kfprintf (Format.kfprintf (fun fmt -> Format.fprintf fmt "@]@.")) - Format.err_formatter "Warning: @[" f +let warn ?(cond = true): ('a, formatter, unit, unit) format4 -> 'a = fun f -> + if cond then + kfprintf (kfprintf (fun fmt -> fprintf fmt "@]@.")) err_formatter + "Warning: @[" f + else ifprintf err_formatter f -let error: ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a = fun f -> - Format.kfprintf (Format.kfprintf (fun fmt -> Format.fprintf fmt "@]@.")) - Format.err_formatter "Error: @[" f +let error: ('a, formatter, unit, unit) format4 -> 'a = fun f -> + kfprintf (kfprintf (fun fmt -> fprintf fmt "@]@.")) err_formatter + "Error: @[" f let do_pass d f p pp = comment (d ^ " ...\n");