Changeset 2773 for driver

Timestamp:

Mar 4, 2013, 10:03:33 AM (8 years ago)

Author:

sacerdot

Message:

1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
2. new extraction after file reorganization (by James)

Location:

driver

Files:

• clightFromC.ml (modified) (1 diff)
• clightPrinter.ml (modified) (2 diffs)
• error.ml (modified) (1 diff)
• exec.ml (modified) (2 diffs)
• frontend.ml (modified) (1 diff)

driver/clightFromC.ml

@@ -388 +388 @@
         | C.Oshr -> Oshr
         | C.Oeq  -> Oeq
-        | C.One  -> One0
+        | C.One  -> One
         | C.Olt  -> Olt
         | C.Ogt  -> Ogt

driver/clightPrinter.ml

@@ -76 +76 @@
   | Oshr -> ">>"
   | Oeq  -> "=="
-  | One0  -> "!="
+  | One  -> "!="
   | Olt  -> "<"
   | Ogt  -> ">"
@@ -176 +176 @@
       begin match op with
       | Oand | Oor | Oxor -> 75
-      | Oeq | One0 | Olt | Ogt | Ole | Oge -> 70
+      | Oeq | One | Olt | Ogt | Ole | Oge -> 70
       | Oadd | Osub | Oshl | Oshr -> 60
       | Omul | Odiv | Omod -> 40

driver/error.ml

@@ -3 +3 @@
 
 let error_to_string = function
+| AssemblyTooLarge -> "AssemblyTooLarge"
 | MISSING -> "MISSING"
 | EXTERNAL -> "EXTERNAL"

driver/exec.ml

@@ -2 +2 @@
 
 let rec run g s =
-  (match Extracted.Cexec.is_final0 s with
+  (match Extracted.Cexec.is_final s with
   | Extracted.Types.None ->
     (match Extracted.Cexec.exec_step g s with
@@ -25 +25 @@
 let OK mid = Extracted.Compiler.front_end cl in
 let rtlabs = Extracted.Types.snd mid in
-let g = Extracted.Cexec.make_global0 cl in
-let OK s0 = Extracted.Cexec.make_initial_state0 cl in
+let g = Extracted.Cexec.make_global cl in
+let OK s0 = Extracted.Cexec.make_initial_state cl in
 let r = run g s0 in
 exit (bv_to_int r)

driver/frontend.ml

@@ -25 +25 @@
 let OK mid = Extracted.Compiler.front_end cl in
 let rtlabs = Extracted.Types.snd mid in
-let g = Extracted.RTLabs_semantics.make_global0 rtlabs in
-let OK s0 = Extracted.RTLabs_semantics.make_initial_state0 rtlabs in
+let g = Extracted.RTLabs_semantics.make_global rtlabs in
+let OK s0 = Extracted.RTLabs_semantics.make_initial_state rtlabs in
 let r = run g s0 in
 exit (bv_to_int r)