From 76cb39f790fc3bf4d1e2fae99cda7eeae8bbbbf2 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Fri, 6 Nov 2015 13:26:11 +0100
Subject: Added printing functions for debug annotations.

Instead of printing <unknown builtin> we now print the debug
annotations.
Fix 17581.
---
 cfrontend/PrintCsyntax.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'cfrontend')

diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 4f2a8d0c..bb6576aa 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -266,6 +266,9 @@ let rec expr p (prec, e) =
       fprintf p "%s@[<hov 1>(%a)@]" (camlstring_of_coqstring id) exprlist (true, args)
   | Ebuiltin(EF_inline_asm(txt, sg, clob), _, args, _) ->
       extended_asm p txt None args clob
+  | Ebuiltin(EF_debug(kind,txt,_),_,args,_) ->
+      fprintf p "__builtin_debug@[<hov 1>(%d,%S%a)@]"
+        (P.to_int kind) (extern_atom txt) exprlist (false,args)
   | Ebuiltin(_, _, args, _) ->
       fprintf p "<unknown builtin>@[<hov 1>(%a)@]" exprlist (true, args)
   | Eparen(a1, tycast, ty) ->
-- 
cgit