diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-02-29 08:42:10 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-02-29 08:42:10 +0000 |
commit | c42d68fdeeef7d08b64a900f52d6b295ad31f4f0 (patch) | |
tree | be1575a8e04e814306d7fd3611071c6bc4599fe3 /cfrontend/PrintCsyntax.ml | |
parent | 55a23ce430234a40081222a213c5bb6b157b7552 (diff) | |
download | compcert-c42d68fdeeef7d08b64a900f52d6b295ad31f4f0.tar.gz compcert-c42d68fdeeef7d08b64a900f52d6b295ad31f4f0.zip |
Better printing of pointer values and of locations.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1830 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/PrintCsyntax.ml')
-rw-r--r-- | cfrontend/PrintCsyntax.ml | 26 |
1 files changed, 16 insertions, 10 deletions
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 06160498..3880188e 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -21,6 +21,7 @@ open Camlcoq open Datatypes open Values open AST +open Globalenvs open Csyntax let name_unop = function @@ -167,6 +168,17 @@ let rec precedence = function (* Expressions *) +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" f + | Vptr(b, ofs) -> fprintf p "<ptr%a>" !print_pointer_hook (b, ofs) + | Vundef -> fprintf p "<undef>" + let rec expr p (prec, e) = let (prec', assoc) = precedence e in let (prec1, prec2) = @@ -177,8 +189,8 @@ let rec expr p (prec, e) = then fprintf p "@[<hov 2>(" else fprintf p "@[<hov 2>"; begin match e with - | Eloc _ -> - fprintf p "<loc>" + | Eloc(b, ofs, _) -> + fprintf p "<loc%a>" !print_pointer_hook (b, ofs) | Evar(id, _) -> fprintf p "%s" (extern_atom id) | Ederef(a1, _) -> @@ -187,14 +199,8 @@ let rec expr p (prec, e) = fprintf p "%a.%s" expr (prec', a1) (extern_atom f) | Evalof(l, _) -> expr p (prec, l) - | Eval(Vint n, _) -> - fprintf p "%ld" (camlint_of_coqint n) - | Eval(Vfloat f, _) -> - fprintf p "%F" f - | Eval(Vptr _, _) -> - fprintf p "<ptr>" - | Eval(Vundef, _) -> - fprintf p "<undef>" + | Eval(v, _) -> + print_value p (v) | Esizeof(ty, _) -> fprintf p "sizeof(%s)" (name_type ty) | Ealignof(ty, _) -> |