source: driver/exec.ml @ 2789

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

Some changes to the driver to aid debugging.

File size: 890 bytes
Line 
1open Extracted.Errors
2
3let rec run g s =
4  (match Extracted.Cexec.is_final s with
5  | Extracted.Types.None ->
6    (match Extracted.Cexec.exec_step g s with
7    | Extracted.IOMonad.Value x -> run g (Extracted.Types.snd x)
8    | Extracted.IOMonad.Wrong m -> failwith (Error.errormsg m)
9    | _ -> failwith "unexpected interaction")
10  | Extracted.Types.Some r -> r)
11
12let convBool = function
13| Extracted.Bool.True -> true
14| Extracted.Bool.False -> false
15
16let bv_to_int v =
17  let rec aux i v =
18    match v with
19    | Extracted.Vector.VEmpty -> i
20    | Extracted.Vector.VCons (_,b,t) -> aux (2*i + (if convBool b then 1 else 0)) t
21  in aux 0 v
22;;
23
24let cl = ClightParser.process Sys.argv.(1) in
25let g = Extracted.Cexec.make_global cl in
26let s0 = 
27  match Extracted.Cexec.make_initial_state cl with
28  | OK o -> o
29  | Error m -> failwith (Error.errormsg m)
30in
31let r = run g s0 in
32exit (bv_to_int r)
Note: See TracBrowser for help on using the repository browser.