From 0180f46a9f47f9611974d77844fd860ffa49d679 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 14 Jun 2011 09:35:55 +0000 Subject: Forgot to add new file git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1673 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/PrintAST.ml | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 common/PrintAST.ml (limited to 'common') diff --git a/common/PrintAST.ml b/common/PrintAST.ml new file mode 100644 index 0000000..e065976 --- /dev/null +++ b/common/PrintAST.ml @@ -0,0 +1,40 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Useful functions for pretty-printers *) + +open Printf +open Camlcoq +open AST + +let name_of_type = function Tint -> "int" | Tfloat -> "float" + +let name_of_chunk = function + | Mint8signed -> "int8signed" + | Mint8unsigned -> "int8unsigned" + | Mint16signed -> "int16signed" + | Mint16unsigned -> "int16unsigned" + | Mint32 -> "int32" + | Mfloat32 -> "float32" + | Mfloat64 -> "float64" + +let name_of_external = function + | EF_external(name, sg) -> extern_atom name + | EF_builtin(name, sg) -> extern_atom name + | EF_vload chunk -> sprintf "volatile load %s" (name_of_chunk chunk) + | EF_vstore chunk -> sprintf "volatile store %s" (name_of_chunk chunk) + | EF_malloc -> "malloc" + | EF_free -> "free" + | EF_memcpy(sz, al) -> + sprintf "memcpy size %ld align %ld " (camlint_of_z sz) (camlint_of_z al) + | EF_annot(text, targs) -> sprintf "annot %S" (extern_atom text) + | EF_annot_val(text, targ) -> sprintf "annot_val %S" (extern_atom text) -- cgit v1.2.3