source: driver/cerco.ml @ 2813

Last change on this file since 2813 was 2791, checked in by campbell, 7 years ago

Remove dead code in driver.

File size: 1.5 KB
Line 
1open Extracted.Errors
2open ClightPrinter
3
4let 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)
12
13let convBool = function
14| Extracted.Bool.True -> true
15| Extracted.Bool.False -> false
16
17let 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
23;;
24
25let cl = ClightParser.process Sys.argv.(1) in
26let output = 
27  match Extracted.Compiler.compile cl with
28  | OK o -> o
29  | Error m -> failwith (Error.errormsg m)
30in
31let labelled = output.Extracted.Compiler.c_labelled_clight in
32let l_costmap = output.Extracted.Compiler.c_clight_cost_map in
33let s_costmap = output.Extracted.Compiler.c_stack_cost in
34let style =
35  match try Sys.argv.(2) with _ -> "instrumented" with
36  | "plain" -> Cost_plain
37  | "numbered" -> Cost_numbered (l_costmap,s_costmap)
38  | "instrumented" -> Cost_instrumented (l_costmap,s_costmap)
39  | x -> failwith ("I have no idea what " ^ x ^ " means")
40in
41print_endline (ClightPrinter.print_program style labelled);
42print_newline ();
43print_endline (ASMPrinter.print_program (Extracted.ASM.oc (Extracted.Compiler.c_labelled_object_code output)));
44
Note: See TracBrowser for help on using the repository browser.