diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2020-02-11 18:43:24 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2020-02-12 12:28:55 +0100 |
| commit | 9b881b7928ab7d21e9981133bef5b26e33b6cd9d (patch) | |
| tree | 30c0228aa0c78808d3e9cf5efd5d7e64d4c1cbf0 /cfrontend/Ctyping.v | |
| parent | 6ca9f9bfc7119f1ca4f48de3b5a37cbaee07e4fd (diff) | |
| download | compcert-kvx-9b881b7928ab7d21e9981133bef5b26e33b6cd9d.tar.gz compcert-kvx-9b881b7928ab7d21e9981133bef5b26e33b6cd9d.zip | |
Take the sign into account for int to ptr cast.
Casting from an integer constant to pointer on 64 bit
architectures did not take the signedness into account and always
interpreted the integer as unsigned which causes some
incompatibility with libc implementations.
Diffstat (limited to 'cfrontend/Ctyping.v')
| -rw-r--r-- | cfrontend/Ctyping.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index b92a9bac..29ea3bf2 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -987,6 +987,7 @@ Proof. classify_cast (Tint i s a) t2 <> cast_case_default). { unfold classify_cast. destruct t2; try congruence. destruct f; congruence. + destruct Archi.ptr64; congruence. } destruct i; auto. Qed. |