source: driver/exec.ml @ 2721

open Extracted.Errors

let rec run g s =
  (match Extracted.Cexec.is_final0 s with
  | Extracted.Types.None ->
    (match Extracted.Cexec.exec_step g s with
    | Extracted.IOMonad.Value x -> run g (Extracted.Types.snd x)
    | Extracted.IOMonad.Wrong m -> failwith (Error.errormsg m)
    | _ -> failwith "unexpected interaction")
  | Extracted.Types.Some r -> r)

let convBool = function
| Extracted.Bool.True -> true
| Extracted.Bool.False -> false

let bv_to_int v =
  let rec aux i v =
    match v with
    | Extracted.Vector.VEmpty -> i
    | Extracted.Vector.VCons (_,b,t) -> aux (2*i + (if convBool b then 1 else 0)) t
  in aux 0 v
;;

let cl = ClightParser.process Sys.argv.(1) in
let OK mid = Extracted.Compiler.front_end cl in
let rtlabs = Extracted.Types.snd mid in
let g = Extracted.Cexec.make_global0 cl in
let OK s0 = Extracted.Cexec.make_initial_state0 cl in
let r = run g s0 in
exit (bv_to_int r)