aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Elab.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-09-22 10:58:41 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2016-09-22 10:58:41 +0200
commite237804b607c1d3bc8217d6f14a35c003f6c8fc7 (patch)
tree5f3977778104e5640afda7c79cd9fd57d23457b6 /cparser/Elab.ml
parent60402c551f309b3eb87f83f2b67906229f688625 (diff)
downloadcompcert-e237804b607c1d3bc8217d6f14a35c003f6c8fc7.tar.gz
compcert-e237804b607c1d3bc8217d6f14a35c003f6c8fc7.zip
Renamed pedantic to implicit-int.
The only case where compcert raise a pedantic warning was for implicit int parameters. This is the behavior of clang. However since not all other pedantic warnings are supported the behavior of gcc is adopted. Bug 19872.
Diffstat (limited to 'cparser/Elab.ml')
-rw-r--r--cparser/Elab.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index b6418217..8d14baf1 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -2115,7 +2115,7 @@ let elab_KR_function_parameters env params defs loc =
| [] ->
(* Parameter is not declared, defaults to "int" in ISO C90,
is an error in ISO C99. Just emit a warning. *)
- warning loc Pedantic "type of '%s' defaults to 'int'" param;
+ warning loc Implicit_int "type of '%s' defaults to 'int'" param;
TInt (IInt, [])
| (_, ty) :: rem ->
if rem <> [] then