diff options
| -rw-r--r-- | cfrontend/PrintClight.ml | 4 | ||||
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 31 | ||||
| -rw-r--r-- | driver/Interp.ml | 2 |
3 files changed, 27 insertions, 10 deletions
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index 376707a..49705c4 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -76,10 +76,14 @@ let rec expr p (prec, e) = fprintf p "*%a" expr (prec', a1) | Efield(a1, f, _) -> fprintf p "%a.%s" expr (prec', a1) (extern_atom f) + | Econst_int(n, Tint(I32, Unsigned, _)) -> + fprintf p "%luU" (camlint_of_coqint n) | Econst_int(n, _) -> fprintf p "%ld" (camlint_of_coqint n) | Econst_float(f, _) -> fprintf p "%F" (camlfloat_of_coqfloat f) + | Econst_long(n, Tlong(Unsigned, _)) -> + fprintf p "%LuLLU" (camlint64_of_coqint n) | Econst_long(n, _) -> fprintf p "%LdLL" (camlint64_of_coqint n) | Eunop(Oabsfloat, a1, _) -> diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 758323e..a233c1f 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -179,13 +179,24 @@ let print_pointer_hook : (formatter -> Values.block * Integers.Int.int -> unit) ref = ref (fun p (b, ofs) -> ()) -let print_value p v = - match v with - | Vint n -> fprintf p "%ld" (camlint_of_coqint n) - | Vfloat f -> fprintf p "%F" (camlfloat_of_coqfloat f) - | Vlong n -> fprintf p "%Ld" (camlint64_of_coqint n) - | Vptr(b, ofs) -> fprintf p "<ptr%a>" !print_pointer_hook (b, ofs) - | Vundef -> fprintf p "<undef>" +let print_typed_value p v ty = + match v, ty with + | Vint n, Tint(I32, Unsigned, _) -> + fprintf p "%luU" (camlint_of_coqint n) + | Vint n, _ -> + fprintf p "%ld" (camlint_of_coqint n) + | Vfloat f, _ -> + fprintf p "%F" (camlfloat_of_coqfloat f) + | Vlong n, Tlong(Unsigned, _) -> + fprintf p "%LuLLU" (camlint64_of_coqint n) + | Vlong n, _ -> + fprintf p "%LdLL" (camlint64_of_coqint n) + | Vptr(b, ofs), _ -> + fprintf p "<ptr%a>" !print_pointer_hook (b, ofs) + | Vundef, _ -> + fprintf p "<undef>" + +let print_value p v = print_typed_value p v Tvoid let rec expr p (prec, e) = let (prec', assoc) = precedence e in @@ -207,8 +218,8 @@ let rec expr p (prec, e) = fprintf p "%a.%s" expr (prec', a1) (extern_atom f) | Evalof(l, _) -> expr p (prec, l) - | Eval(v, _) -> - print_value p (v) + | Eval(v, ty) -> + print_typed_value p v ty | Esizeof(ty, _) -> fprintf p "sizeof(%s)" (name_type ty) | Ealignof(ty, _) -> @@ -251,6 +262,8 @@ let rec expr p (prec, e) = | Ebuiltin(EF_annot_val(txt, _), _, args, _) -> fprintf p "__builtin_annot_val@[<hov 1>(%S%a)@]" (extern_atom txt) exprlist (false, args) + | Ebuiltin(EF_external(id, sg), _, args, _) -> + fprintf p "%s@[<hov 1>(%a)@]" (extern_atom id) exprlist (true, args) | Ebuiltin(_, _, args, _) -> fprintf p "<unknown builtin>@[<hov 1>(%a)@]" exprlist (true, args) | Eparen(a1, ty) -> diff --git a/driver/Interp.ml b/driver/Interp.ml index 4f9debd..99f9f4f 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -47,7 +47,7 @@ let print_eventval p = function | EVint n -> fprintf p "%ld" (camlint_of_coqint n) | EVfloat f -> fprintf p "%F" (camlfloat_of_coqfloat f) | EVfloatsingle f -> fprintf p "%F" (camlfloat_of_coqfloat f) - | EVlong n -> fprintf p "%Ld" (camlint64_of_coqint n) + | EVlong n -> fprintf p "%LdLL" (camlint64_of_coqint n) | EVptr_global(id, ofs) -> fprintf p "&%a" print_id_ofs (id, ofs) let print_eventval_list p = function |