aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2022-09-04 19:08:22 +0200
committerXavier Leroy <xavier.leroy@college-de-france.fr>2022-09-04 19:08:22 +0200
commit91f21889423c41bb46b8b25b510c71987cf6006b (patch)
tree0f39c51602d6d3947f35784c9eee8a10df3ae545
parent941c3f023f473731d5a3399d950c746d0cadf46a (diff)
downloadcompcert-91f21889423c41bb46b8b25b510c71987cf6006b.tar.gz
compcert-91f21889423c41bb46b8b25b510c71987cf6006b.zip
`_Generic` is a C11 feature, should trigger the corresponding warning if active
-rw-r--r--cparser/Elab.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 88500470..01e745c3 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1768,6 +1768,7 @@ let elab_expr ctx loc env a =
(* 6.5.1.1 Generic selection *)
| GENERIC(a1, assoc) ->
+ warning Celeven_extension "'_Generic' is a C11 extension";
let b1,env = elab env a1 in
let bssoc,env = elab_generic_association env assoc in
let ty = erase_attributes_type env (pointer_decay env b1.etyp) in