diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-04-27 15:38:16 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bschommer@users.noreply.github.com> | 2018-05-07 17:05:40 +0200 |
| commit | 6657ff7f757d22ad70fe13458f8e7eb76698ac6b (patch) | |
| tree | 6e4572e6216bd11a3d3b6959cde95d2870c9cbdb | |
| parent | f0857720ae2be7f73c43f462a4a0f47ad20b5750 (diff) | |
| download | compcert-kvx-6657ff7f757d22ad70fe13458f8e7eb76698ac6b.tar.gz compcert-kvx-6657ff7f757d22ad70fe13458f8e7eb76698ac6b.zip | |
Warning for comparison of incomplete pointers.
The C standards says that either both types must be pointer to
complete compatible or incomplete compatible types.
Bug 23631
| -rw-r--r-- | cparser/Elab.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 4decc105..a155c893 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2101,6 +2101,10 @@ let elab_expr vararg loc env a = if not (compatible_types AttrIgnoreAll env ty1 ty2) then warning Compare_distinct_pointer_types "comparison of distinct pointer types (%a and %a)" (print_typ env) b1.etyp (print_typ env) b2.etyp; + let incomp_ty1 = wrap incomplete_type loc env ty1 + and incomp_ty2 = wrap incomplete_type loc env ty2 in + if incomp_ty1 <> incomp_ty2 then + warning Unnamed "comparison of complete and incomplete pointers"; EBinop(op, b1, b2, TPtr(ty1, [])) | TPtr _, (TInt _ | TEnum _) | (TInt _ | TEnum _), TPtr _ -> |