aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Elab.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bschommer@users.noreply.github.com>2018-04-20 18:02:34 +0200
committerXavier Leroy <xavierleroy@users.noreply.github.com>2018-04-20 19:02:34 +0300
commit90f83fd516f625f21533c7c8d775bf630bbacdb5 (patch)
treeed52870ef65244b2356ab17a5876914621a7723f /cparser/Elab.ml
parentcdeece5cb3f3087baa641c41cc30ec34aa635edd (diff)
downloadcompcert-kvx-90f83fd516f625f21533c7c8d775bf630bbacdb5.tar.gz
compcert-kvx-90f83fd516f625f21533c7c8d775bf630bbacdb5.zip
Better check for incomplete types in pointer subtraction (#92)
In the case of pointer subtraction both side can be pointers, for example if the difference between two array cells is calculated, so we need to check that both sides have complete types. Bug 23312
Diffstat (limited to 'cparser/Elab.ml')
-rw-r--r--cparser/Elab.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 074779ca..f203c777 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1854,6 +1854,7 @@ let elab_expr vararg loc env a =
err "%a and %a are not pointers to compatible types"
(print_typ env) b1.etyp (print_typ env) b1.etyp;
check_ptr_arith env ty1 '-';
+ check_ptr_arith env ty2 '-';
if wrap sizeof loc env ty1 = Some 0 then
err "subtraction between two pointers to zero-sized objects";
(TPtr(ty1, []), TInt(ptrdiff_t_ikind(), []))