diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-15 15:07:47 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-15 15:07:47 +0100 |
| commit | 272a5b812b72f4c3e409ccdbeaf3476d95c4b552 (patch) | |
| tree | 6a8d5e75a11860b69522cef3b512b1ef5effb438 /cfrontend/PrintCsyntax.ml | |
| parent | 2185164c1845c30ebd4118ed5bc8d339b16663a9 (diff) | |
| download | compcert-kvx-272a5b812b72f4c3e409ccdbeaf3476d95c4b552.tar.gz compcert-kvx-272a5b812b72f4c3e409ccdbeaf3476d95c4b552.zip | |
Deactivate warning 27 and added back removed code.
The code was mostly there for documentation effort. So warning
27 is deactivated again.
Bug 18349
Diffstat (limited to 'cfrontend/PrintCsyntax.ml')
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 14 |
1 files changed, 7 insertions, 7 deletions
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@[<hov 1>(%S%a)@]" (camlstring_of_coqstring txt) exprlist (false, args) - | Ebuiltin(EF_external(id, _), _, args, _) -> + | Ebuiltin(EF_external(id, sg), _, args, _) -> fprintf p "%s@[<hov 1>(%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@[<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, _) -> + | 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)) = |