- Timestamp:
- Mar 8, 2013, 11:45:29 PM (8 years ago)
- Location:
- driver
- Files:
-
- 1 deleted
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
driver/build
r2815 r2834 12 12 ocamlc -I ../Deliverables/D2.2/8051/lib -c -g error.ml 13 13 ocamlc -I ../Deliverables/D2.2/8051/lib -c -g *.ml 14 ocamlc -custom -g -I ../Deliverables/D2.2/8051/lib extracted.cmo ../Deliverables/D2.2/8051/lib/libcparser.a ../Deliverables/D2.2/8051/lib/cparser.cma clightFromC.cmo clightParser.cmo error.cmo exec_all.cmo -o exec_all15 14 ocamlc -custom -g -I ../Deliverables/D2.2/8051/lib extracted.cmo ../Deliverables/D2.2/8051/lib/libcparser.a ../Deliverables/D2.2/8051/lib/cparser.cma clightFromC.cmo clightParser.cmo clightPrinter.cmo IntelHex.cmo ASMPrinter.cmo error.cmo cerco.cmo -o cerco -
driver/cerco.ml
r2791 r2834 2 2 open ClightPrinter 3 3 4 let rec run g s = 5 (match Extracted.RTLabs_semantics.rTLabs_is_final s with 6 | Extracted.Types.None -> 7 (match Extracted.RTLabs_semantics.eval_statement g s with 8 | Extracted.IOMonad.Value x -> run g (Extracted.Types.snd x) 9 | Extracted.IOMonad.Wrong m -> failwith (Error.errormsg m) 10 | _ -> failwith "oh dear") 11 | Extracted.Types.Some r -> r) 4 let string_of_pos n = string_of_int (Extracted.Glue.int_of_matitapos n) 12 5 13 let convBool = function 14 | Extracted.Bool.True -> true 15 | Extracted.Bool.False -> false 16 17 let bv_to_int v = 18 let rec aux i v = 19 match v with 20 | Extracted.Vector.VEmpty -> i 21 | Extracted.Vector.VCons (_,b,t) -> aux (2*i + (if convBool b then 1 else 0)) t 22 in aux 0 v 6 let string_of_intensional_event = 7 function 8 Extracted.StructuredTraces.IEVcost cl -> 9 "COST(k_" ^ string_of_pos cl ^") " 10 | Extracted.StructuredTraces.IEVcall id -> 11 "CALL(fun_" ^ string_of_pos id ^ ") " 12 | Extracted.StructuredTraces.IEVtailcall _ -> assert false 13 | Extracted.StructuredTraces.IEVret id -> 14 "RET(fun_" ^ string_of_pos id ^ ") " 23 15 ;; 24 16 25 let cl = ClightParser.process Sys.argv.(1) in 17 let string_of_pass = 18 function 19 | Extracted.Compiler.Clight_pass -> "Clight_pass" 20 | Extracted.Compiler.Clight_switch_removed_pass -> "Clight_switch_removed_pass" 21 | Extracted.Compiler.Clight_label_pass -> "Clight_label_pass" 22 | Extracted.Compiler.Clight_simplified_pass -> "Clight_simplified_pass" 23 | Extracted.Compiler.Cminor_pass -> "Cminor_pass" 24 | Extracted.Compiler.Rtlabs_pass -> "Rtlabs_pass" 25 | Extracted.Compiler.Rtl_separate_pass -> "Rtl_separate_pass" 26 | Extracted.Compiler.Rtl_uniq_pass -> "Rtl_uniq_pass" 27 | Extracted.Compiler.Ertl_pass -> "Ertl_pass" 28 | Extracted.Compiler.Ertlptr_pass -> "Ertlptr_pass" 29 | Extracted.Compiler.Ltl_pass -> "Ltl_pass" 30 | Extracted.Compiler.Lin_pass -> "Lin_pass" 31 ;; 32 33 let argv1 = Sys.argv.(1) in 34 let do_print,filename = 35 if argv1 = "-exec" then 36 true,Sys.argv.(2) 37 else 38 false,argv1 in 39 let cl = ClightParser.process filename in 40 let observe = 41 if do_print then 42 let rec infinity = Extracted.Nat.S infinity in 43 (fun pass prog -> 44 Extracted.Semantics.run_and_print pass prog infinity 45 (fun p -> print_endline ("\n" ^ string_of_pass p ^ ":"); Extracted.Types.It) 46 (fun evn -> print_string (string_of_intensional_event evn); Extracted.Types.It) 47 (fun msg -> print_endline (Error.errormsg msg); Extracted.Types.It) 48 (fun n-> print_endline (string_of_int (Extracted.Glue.int_of_bitvector n)); Extracted.Types.It)) 49 else (fun _ _ -> Extracted.Types.It) 50 in 26 51 let output = 27 match Extracted.Compiler.compile cl with52 match Extracted.Compiler.compile observe cl with 28 53 | OK o -> o 29 54 | Error m -> failwith (Error.errormsg m)
Note: See TracChangeset
for help on using the changeset viewer.