From a5ffc59246b09a389e5f8cbc2f217e323e76990f Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 13 Jun 2011 18:11:19 +0000
Subject: Revised handling of annotation statements, and more generally
 built-in functions, and more generally external functions

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/PrintLTLin.ml | 18 +++---------------
 1 file changed, 3 insertions(+), 15 deletions(-)

(limited to 'backend/PrintLTLin.ml')

diff --git a/backend/PrintLTLin.ml b/backend/PrintLTLin.ml
index e0a3204..adff483 100644
--- a/backend/PrintLTLin.ml
+++ b/backend/PrintLTLin.ml
@@ -21,21 +21,9 @@ open Integers
 open Locations
 open Machregsaux
 open LTLin
+open PrintAST
 open PrintOp
 
-let name_of_chunk = function
-  | Mint8signed -> "int8signed"
-  | Mint8unsigned -> "int8unsigned"
-  | Mint16signed -> "int16signed"
-  | Mint16unsigned -> "int16unsigned"
-  | Mint32 -> "int32"
-  | Mfloat32 -> "float32"
-  | Mfloat64 -> "float64"
-
-let name_of_type = function
-  | Tint -> "int"
-  | Tfloat -> "float"
-
 let reg pp loc =
   match loc with
   | R r ->
@@ -80,8 +68,8 @@ let print_instruction pp i =
       fprintf pp "tailcall %a(%a)@ "
         ros fn regs args
   | Lbuiltin(ef, args, res) ->
-      fprintf pp "%a = builtin \"%s\"(%a)@ "
-        reg res (extern_atom ef.ef_id) regs args
+      fprintf pp "%a = builtin %s(%a)@ "
+        reg res (name_of_external ef) regs args
   | Llabel lbl ->
       fprintf pp "%ld:@ " (camlint_of_positive lbl)
   | Lgoto lbl ->
-- 
cgit v1.2.3