diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-24 14:27:35 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-24 14:34:59 +0200 |
commit | af5758ac9414541a62bf08ae44373b441b8653ec (patch) | |
tree | 36549b68ae207e282dde80b60d375bb139afd743 | |
parent | 03ab00aec5d10f4a2d048fab7f16489cf33fcc1d (diff) | |
download | compcert-af5758ac9414541a62bf08ae44373b441b8653ec.tar.gz compcert-af5758ac9414541a62bf08ae44373b441b8653ec.zip |
driver/Interp: update
Cherry-pick commit d1311e6 from trunk.
Simplify convert_external_arg so that it works both in 32 and 64 bits.
-rw-r--r-- | driver/Interp.ml | 16 |
1 files changed, 8 insertions, 8 deletions
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"), _ -> "<long long argument expected" - | ('f'|'e'|'E'|'g'|'G'|'a'), "l", Vfloat f -> + | ('f'|'e'|'E'|'g'|'G'|'a'), (""|"l"), Vfloat f -> format_float (flags ^ conv) (camlfloat_of_coqfloat f) | ('f'|'e'|'E'|'g'|'G'|'a'), "", _ -> "<float argument expected" @@ -366,14 +366,14 @@ 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 -> + 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 |