From 272a5b812b72f4c3e409ccdbeaf3476d95c4b552 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 15 Mar 2016 15:07:47 +0100 Subject: Deactivate warning 27 and added back removed code. The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349 --- cfrontend/PrintCsyntax.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'cfrontend/PrintCsyntax.ml') diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index e3e04c07..d518d6bb 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -99,7 +99,7 @@ let rec name_cdecl id ty = | Tfunction _ | Tarray _ -> sprintf "(*%s%s)" (attributes_space a) id | _ -> sprintf "*%s%s" (attributes_space a) id in name_cdecl id' t - | Tarray(t, n, _) -> + | Tarray(t, n, a) -> name_cdecl (sprintf "%s[%ld]" id (camlint_of_coqint n)) t | Tfunction(args, res, cconv) -> let b = Buffer.create 20 in @@ -170,7 +170,7 @@ let rec precedence = function let print_pointer_hook : (formatter -> Values.block * Integers.Int.int -> unit) ref - = ref (fun _ _ -> ()) + = ref (fun p (b, ofs) -> ()) let print_typed_value p v ty = match v, ty with @@ -233,7 +233,7 @@ let rec expr p (prec, e) = expr (prec1, a1) (name_binop op) expr (prec2, a2) | Ecast(a1, ty) -> fprintf p "(%s) %a" (name_type ty) expr (prec', a1) - | Eassign(res, Ebuiltin(EF_inline_asm(txt, _, clob), _, args, _), _) -> + | Eassign(res, Ebuiltin(EF_inline_asm(txt, sg, clob), _, args, _), _) -> extended_asm p txt (Some res) args clob | Eassign(a1, a2, _) -> fprintf p "%a =@ %a" expr (prec1, a1) expr (prec2, a2) @@ -259,16 +259,16 @@ let rec expr p (prec, e) = | Ebuiltin(EF_annot_val(txt, _), _, args, _) -> fprintf p "__builtin_annot_val@[(%S%a)@]" (camlstring_of_coqstring txt) exprlist (false, args) - | Ebuiltin(EF_external(id, _), _, args, _) -> + | Ebuiltin(EF_external(id, sg), _, args, _) -> fprintf p "%s@[(%a)@]" (camlstring_of_coqstring id) exprlist (true, args) - | Ebuiltin(EF_inline_asm(txt, _, clob), _, 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@[(%d,%S%a)@]" (P.to_int kind) (extern_atom txt) exprlist (false,args) | Ebuiltin(_, _, args, _) -> fprintf p "@[(%a)@]" exprlist (true, args) - | Eparen(a1, tycast, _) -> + | Eparen(a1, tycast, ty) -> fprintf p "(%s) %a" (name_type tycast) expr (prec', a1) end; if prec' < prec then fprintf p ")@]" else fprintf p "@]" @@ -506,7 +506,7 @@ let print_globdef p (id, gd) = let struct_or_union = function Struct -> "struct" | Union -> "union" -let declare_composite p (Composite(id, su, _, _)) = +let declare_composite p (Composite(id, su, m, a)) = fprintf p "%s %s;@ " (struct_or_union su) (extern_atom id) let define_composite p (Composite(id, su, m, a)) = -- cgit