Changeset 1462 for Deliverables/D2.2/8051/src/languages.ml

Timestamp:

Oct 25, 2011, 4:11:11 PM (9 years ago)

Author:

ayache

Message:

Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been updated accordingly.

File:

• Deliverables/D2.2/8051/src/languages.ml (modified) (8 diffs)

Deliverables/D2.2/8051/src/languages.ml

@@ -51 +51 @@
   | language -> [to_string language]
 
-let parse = function
+let parse ?is_lustre_file ?remove_lustre_externals = function
   | Clight -> 
-    fun filename -> AstClight (ClightParser.process filename)
+    fun filename ->
+      AstClight
+        (ClightParser.process ?is_lustre_file ?remove_lustre_externals filename)
 
 (*
@@ -111 +113 @@
 
 let ltl_to_lin = function
-  | AstLTL p -> 
+  | AstLTL p ->
     AstLIN (LTLToLIN.translate p)
   | _ -> assert false
 
 let lin_to_asm = function
-  | AstLIN p -> 
+  | AstLIN p ->
     AstASM (LINToASM.translate p)
   | _ -> assert false
@@ -210 +212 @@
 let instrument costs_mapping = function
   | AstClight p ->
-    let (p', cost_id, cost_incr) = ClightAnnotator.instrument p costs_mapping in
-    (AstClight p', cost_id, cost_incr)
+    let (p', cost_id, cost_incr, extern_cost_variables) =
+      ClightAnnotator.instrument p costs_mapping in
+    (AstClight p', cost_id, cost_incr, extern_cost_variables)
 (*
   | AstCminor p ->
@@ -222 +225 @@
          "Instrumentation is not implemented for source language `%s'."
          (to_string (language_of_ast p)));
-    (p, "", "")
-
-let annotate input_ast final = 
+    (p, "", "", StringTools.Map.empty)
+
+let annotate input_ast final =
   let costs_mapping = compute_costs final in 
   instrument costs_mapping input_ast
 
-let string_output = function
+let string_output asm_pretty = function
   | AstClight p -> 
     [ClightPrinter.print_program p]
@@ -244 +247 @@
     [LINPrinter.print_program p]
   | AstASM p ->
-    [Pretty.print_program p ; ASMPrinter.print_program p]
-
-let save exact_output filename suffix ast =
+    (if asm_pretty then [Pretty.print_program p]
+     else ["Pretty print not requested"]) @
+    [ASMPrinter.print_program p]
+
+let save asm_pretty exact_output filename suffix ast =
   let ext_chopped_filename =
     if exact_output then filename 
@@ -259 +264 @@
     if exact_output then ext_filenames
     else List.map Misc.SysExt.alternative ext_filenames in
-  let output_strings = string_output ast in
+  let output_strings = string_output asm_pretty ast in
   let f filename s =
     let cout = open_out filename in
@@ -267 +272 @@
   List.iter2 f output_filenames output_strings
 
-let save_cost filename cost_id cost_incr =
+let save_cost exact_name filename cost_id cost_incr extern_cost_variables =
+  let filename =
+    if exact_name then filename
+    else
+      try Filename.chop_extension filename
+      with Invalid_argument ("Filename.chop_extension") -> filename in
   let cout = open_out (filename ^ ".cerco") in
+  let f fun_name cost_var =
+    output_string cout (fun_name ^ " " ^ cost_var ^ "\n") in
   output_string cout (cost_id ^ "\n");
   output_string cout (cost_incr ^ "\n");
+  StringTools.Map.iter f extern_cost_variables;
   flush cout;
   close_out cout
@@ -291 +304 @@
   | AstASM p ->
     ASMInterpret.interpret debug p
+
+let add_lustre_main
+    lustre_test lustre_test_cases lustre_test_cycles
+    lustre_test_min_int lustre_test_max_int = function
+  | AstClight p ->
+    AstClight
+      (ClightLustreMain.add lustre_test lustre_test_cases lustre_test_cycles
+         lustre_test_min_int lustre_test_max_int p)
+  | _ ->
+    Error.global_error "during main generation"
+      "Lustre testing is only available with C programs."