Changeset 2805 for driver


Ignore:
Timestamp:
Mar 7, 2013, 2:01:40 PM (7 years ago)
Author:
sacerdot
Message:

Now also prints the trace for the labelled Clight.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • driver/exec_all.ml

    r2804 r2805  
    1414;;
    1515
    16 let run_and_print pre_classified_system prog =
     16let run_and_print label pre_classified_system prog =
    1717 let prog = Obj.magic prog in
    1818 let fullexec = Extracted.Measurable.pcs_exec pre_classified_system in
     
    2525 in
    2626 let rec infinity = Extracted.Nat.S infinity in
     27 print_string label;
    2728 let {Extracted.Types.fst = trace; snd = res} =
    2829  Extracted.Measurable.observe_all_in_measurable infinity
     
    4142let mid =
    4243  match Extracted.Compiler.front_end cl with
    43   | OK o -> Extracted.Types.snd o
    44   | Error m -> failwith (Error.errormsg m)
    45 in
    46 run_and_print Extracted.Clight_classified_system.clight_pcs cl
     44  | OK o -> o
     45  | Error m -> failwith (Error.errormsg m) in
     46let acl = Extracted.Types.snd (Extracted.Types.fst mid) in
     47run_and_print "Clight:  " Extracted.Clight_classified_system.clight_pcs cl;
     48run_and_print "LClight: " Extracted.Clight_classified_system.clight_pcs cl
Note: See TracChangeset for help on using the changeset viewer.