aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Cutil.mli
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-10-04 20:36:02 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-10-04 20:36:02 +0200
commit57fceab9ba11cb98635236f31c85ca976ca7f48c (patch)
tree60c617163717c1c56df7219babdcc49a00e3d5c1 /cparser/Cutil.mli
parentb96122579c7e4dc6e38b0f1caa9bddf9997b49fa (diff)
downloadcompcert-kvx-57fceab9ba11cb98635236f31c85ca976ca7f48c.tar.gz
compcert-kvx-57fceab9ba11cb98635236f31c85ca976ca7f48c.zip
Allow redefinition of a typedef with the same name.
C11 allows a typedef redefinition if the types are the same. We now allow this also and issue a warning and an error if the types are different.
Diffstat (limited to 'cparser/Cutil.mli')
-rw-r--r--cparser/Cutil.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index b9879339..a322bfb1 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -80,6 +80,8 @@ val combine_types : attr_handling -> Env.t -> typ -> typ -> typ option
with the same meaning as for [compatible_types].
When two sets of attributes are compatible, the result of
[combine_types] carries the union of these two sets of attributes. *)
+val equal_types : Env.t -> typ -> typ -> bool
+ (* Check that the two given types are equal up to typedef use *)
(* Size and alignment *)