From af5758ac9414541a62bf08ae44373b441b8653ec Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 24 Oct 2016 14:27:35 +0200 Subject: driver/Interp: update Cherry-pick commit d1311e6 from trunk. Simplify convert_external_arg so that it works both in 32 and 64 bits. --- driver/Interp.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'driver/Interp.ml') diff --git a/driver/Interp.ml b/driver/Interp.ml index c197d004..1e328a70 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -304,7 +304,7 @@ let format_value m flags length conv arg = format_int64 (flags ^ conv) (camlint64_of_coqint i) | ('d'|'i'|'u'|'o'|'x'|'X'), ("ll"|"j"), _ -> " + | ('f'|'e'|'E'|'g'|'G'|'a'), (""|"l"), Vfloat f -> format_float (flags ^ conv) (camlfloat_of_coqfloat f) | ('f'|'e'|'E'|'g'|'G'|'a'), "", _ -> ">=) 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 -> + match v with + | Vint i -> Some (EVint i) + | Vfloat f -> Some (EVfloat f) + | Vsingle f -> Some (EVsingle f) + | Vlong n -> Some (EVlong n) + | Vptr(b, ofs) -> Senv.invert_symbol ge b >>= fun id -> Some (EVptr_global(id, ofs)) - | _, _ -> None + | _ -> None let rec convert_external_args ge vl tl = match vl, tl with -- cgit