diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-11-27 15:37:32 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-11-27 15:37:32 +0100 |
commit | 56690956f52349c3398b3de6f8ec3987501e9034 (patch) | |
tree | 5fc98e863bb41018084b2110f0ae950189a7b7d6 /driver/Interp.ml | |
parent | 853a40b117495ebf883593633f680cd5c92f5951 (diff) | |
parent | c3b615f875ed2cf8418453c79c4621d2dc61b0a0 (diff) | |
download | compcert-56690956f52349c3398b3de6f8ec3987501e9034.tar.gz compcert-56690956f52349c3398b3de6f8ec3987501e9034.zip |
Merge branch 'master' into dwarf
Diffstat (limited to 'driver/Interp.ml')
-rw-r--r-- | driver/Interp.ml | 25 |
1 files changed, 23 insertions, 2 deletions
diff --git a/driver/Interp.ml b/driver/Interp.ml index e277ebe0..9bb9d237 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -380,13 +380,33 @@ let do_printf m fmt args = let (>>=) opt f = match opt with None -> None | Some arg -> f arg +(* Like eventval_of_val, but accepts static globals as well *) + +let convert_external_arg ge v t = + match v, t with + | Vint i, AST.Tint -> Some (EVint i) + | Vfloat f, AST.Tfloat -> Some (EVfloat f) + | Vsingle f, AST.Tsingle -> Some (EVsingle f) + | Vlong n, AST.Tlong -> Some (EVlong n) + | Vptr(b, ofs), AST.Tint -> + Genv.invert_symbol ge b >>= fun id -> Some (EVptr_global(id, ofs)) + | _, _ -> None + +let rec convert_external_args ge vl tl = + match vl, tl with + | [], [] -> Some [] + | v1::vl, t1::tl -> + convert_external_arg ge v1 t1 >>= fun e1 -> + convert_external_args ge vl tl >>= fun el -> Some (e1 :: el) + | _, _ -> None + let do_external_function id sg ge w args m = match extern_atom id, args with | "printf", Vptr(b, ofs) :: args' -> extract_string m b ofs >>= fun fmt -> print_string (do_printf m fmt args'); flush stdout; - Cexec.list_eventval_of_val ge args sg.sig_args >>= fun eargs -> + convert_external_args ge args sg.sig_args >>= fun eargs -> Some(((w, [Event_syscall(id, eargs, EVint Int.zero)]), Vint Int.zero), m) | _ -> None @@ -612,7 +632,8 @@ let change_main_function p old_main old_main_ty = fn_params = []; fn_vars = []; fn_body = body } in let new_main_id = intern_string "___main" in { prog_main = new_main_id; - prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.prog_defs } + prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.prog_defs; + prog_public = p.prog_public } let rec find_main_function name = function | [] -> None |