From b7cba3315a613115c467b1a35aa51138edaf1c1c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=EBl=20Delaval?= Date: Wed, 8 Dec 2010 17:31:16 +0100 Subject: [PATCH] Compiler option -nocaus Added a compiler option de-activating causality analysis --- compiler/heptagon/main/hept_compiler.ml | 2 +- compiler/main/heptc.ml | 1 + compiler/utilities/global/compiler_options.ml | 2 ++ 3 files changed, 4 insertions(+), 1 deletion(-) diff --git a/compiler/heptagon/main/hept_compiler.ml b/compiler/heptagon/main/hept_compiler.ml index 11b28cc..19aa693 100644 --- a/compiler/heptagon/main/hept_compiler.ml +++ b/compiler/heptagon/main/hept_compiler.ml @@ -42,7 +42,7 @@ let compile_impl pp p = if !print_types then print_interface Format.std_formatter; (* Causality check *) - let p = silent_pass "Causality check" true Causality.program p in + let p = silent_pass "Causality check" !causality Causality.program p in (* Initialization check *) let p = silent_pass "Initialization check" !init Initialization.program p in diff --git a/compiler/main/heptc.ml b/compiler/main/heptc.ml index a31cce0..dc1f1a2 100644 --- a/compiler/main/heptc.ml +++ b/compiler/main/heptc.ml @@ -90,6 +90,7 @@ let main () = "-nopervasives", Arg.Unit set_no_pervasives, doc_no_pervasives; "-target", Arg.String add_target_language, doc_target; "-targetpath", Arg.String set_target_path, doc_target_path; + "-nocaus", Arg.Clear causality, doc_nocaus; "-noinit", Arg.Clear init, doc_noinit; "-fti", Arg.Set full_type_info, doc_full_type_info; "-itfusion", Arg.Set do_iterator_fusion, doc_itfusion; diff --git a/compiler/utilities/global/compiler_options.ml b/compiler/utilities/global/compiler_options.ml index 03c16ea..837c923 100644 --- a/compiler/utilities/global/compiler_options.ml +++ b/compiler/utilities/global/compiler_options.ml @@ -75,6 +75,7 @@ let set_target_path path = let full_type_info = ref false +let causality = ref true let init = ref true let inline : qualname list ref = ref [] @@ -111,6 +112,7 @@ and doc_full_type_info = "\t\t\tPrint full type information" and doc_target_path = "\tGenerated files will be placed in \n\t\t\t(the directory is" ^ " cleaned)" +and doc_nocaus = "\t\tDisable causality analysis" and doc_noinit = "\t\tDisable initialization analysis" and doc_assert = "\t\tInsert run-time assertions for boolean node " and doc_inline = "\t\tInline node "