Changeset 2805

Timestamp:

Mar 7, 2013, 2:01:40 PM (7 years ago)

Author:

sacerdot

Message:

Now also prints the trace for the labelled Clight.

File:

• driver/exec_all.ml (modified) (3 diffs)

driver/exec_all.ml

@@ -14 +14 @@
 ;;
 
-let run_and_print pre_classified_system prog =
+let run_and_print label pre_classified_system prog =
  let prog = Obj.magic prog in
  let fullexec = Extracted.Measurable.pcs_exec pre_classified_system in
@@ -25 +25 @@
  in
  let rec infinity = Extracted.Nat.S infinity in
+ print_string label;
  let {Extracted.Types.fst = trace; snd = res} =
   Extracted.Measurable.observe_all_in_measurable infinity
@@ -41 +42 @@
 let mid =
   match Extracted.Compiler.front_end cl with
-  | OK o -> Extracted.Types.snd o
-  | Error m -> failwith (Error.errormsg m)
-in
-run_and_print Extracted.Clight_classified_system.clight_pcs cl
+  | OK o -> o
+  | Error m -> failwith (Error.errormsg m) in
+let acl = Extracted.Types.snd (Extracted.Types.fst mid) in
+run_and_print "Clight:  " Extracted.Clight_classified_system.clight_pcs cl;
+run_and_print "LClight: " Extracted.Clight_classified_system.clight_pcs cl