Changeset 2993 for driver/cerco.ml


Ignore:
Timestamp:
Mar 28, 2013, 9:56:26 AM (8 years ago)
Author:
sacerdot
Message:
  1. performance improved: the type inference was inferring load_code_memory ... in computational positions, duplicating the work at every step of execution of the assembly code. We now force the use of the let-in-ed variable
  2. new extraction after 1)
  3. driver/printer.ml repaired
  4. the output of the intermediate passes is now printed on file
File:
1 edited

Legend:

Unmodified
Added
Removed
  • driver/cerco.ml

    r2964 r2993  
    3434
    3535let argv1 = Sys.argv.(1) in
    36 let do_print,filename,style =
     36let do_exec,filename,style =
    3737 if argv1 = "-exec" then
    3838  true,Sys.argv.(2),(try Sys.argv.(3) with _ -> "instrumented")
     
    4141let cl = ClightParser.process filename in
    4242let observe =
    43  if do_print then
    44   let rec infinity = Extracted.Nat.S infinity in
    45   (fun pass prog ->
    46     print_string (Printer.print_program pass prog);
     43 let rec infinity = Extracted.Nat.S infinity in
     44 (fun pass prog ->
     45   if do_exec || pass = Extracted.Compiler.Clight_label_pass ||
     46      pass = Extracted.Compiler.Object_code_pass then
     47    Printer.print_program filename pass prog;
     48   if do_exec then
    4749    Extracted.Semantics.run_and_print pass prog infinity
    48      (fun p -> print_string ("\n" ^ string_of_pass p ^ ": "); Extracted.Types.It)
    49      (fun evn -> print_string (string_of_intensional_event evn); Extracted.Types.It)
    50      (fun msg -> print_endline (Error.errormsg msg); Extracted.Types.It)
    51      (fun n-> print_endline (string_of_int (Extracted.Glue.int_of_bitvector n)); Extracted.Types.It))
    52  else (fun _ _ -> Extracted.Types.It)
     50     (fun p -> print_string ("\n" ^ string_of_pass p ^ ": "); flush stdout;
     51       Extracted.Types.It)
     52     (fun evn -> print_string (string_of_intensional_event evn); flush stdout;
     53       Extracted.Types.It)
     54     (fun msg -> print_endline (Error.errormsg msg); flush stdout;
     55       Extracted.Types.It)
     56     (fun n-> print_endline (string_of_int(Extracted.Glue.int_of_bitvector n));
     57       flush stdout; Extracted.Types.It)
     58   else
     59    Extracted.Types.It)
    5360in
    5461let output =
Note: See TracChangeset for help on using the changeset viewer.