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

Timestamp:

Apr 4, 2011, 5:18:15 PM (10 years ago)

Author:

ayache

Message:

New memory model and bug fixes in 8051 branch. Added primitive operations in interpreters from Clight to LIN.

File:

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

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

@@ -234 +234 @@
     [Pretty.print_program p ; ASMPrinter.print_program p]
 
-let save exact_output filename ast =
+let save exact_output filename suffix ast =
   let ext_chopped_filename =
-    if exact_output then filename
+    if exact_output then filename 
     else
       try Filename.chop_extension filename
       with Invalid_argument ("Filename.chop_extension") -> filename in
+  let ext_chopped_filename = ext_chopped_filename ^ suffix in
   let ext_filenames =
     List.map (fun ext -> ext_chopped_filename ^ "." ^ ext)
@@ -261 +262 @@
   close_out cout
 
-let interpret print_result = function
+let interpret debug = function
   | AstClight p ->
-    ClightInterpret.interpret print_result p
+    ClightInterpret.interpret debug p
   | AstCminor p ->
-    CminorInterpret.interpret print_result p  
+    CminorInterpret.interpret debug p  
   | AstRTLabs p ->
-    RTLabsInterpret.interpret print_result p
+    RTLabsInterpret.interpret debug p
   | AstRTL p ->
-    RTLInterpret.interpret print_result p
+    RTLInterpret.interpret debug p
   | AstERTL p ->
-    ERTLInterpret.interpret print_result p
+    ERTLInterpret.interpret debug p
   | AstLTL p ->
-    LTLInterpret.interpret print_result p
+    LTLInterpret.interpret debug p
   | AstLIN p ->
-    LINInterpret.interpret print_result p
+    LINInterpret.interpret debug p
   | AstASM p ->
-    ASMInterpret.interpret print_result p
+    ASMInterpret.interpret debug p