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 | |
| parent | 6ca9f9bfc7119f1ca4f48de3b5a37cbaee07e4fd (diff) | |
| download | compcert-9b881b7928ab7d21e9981133bef5b26e33b6cd9d.tar.gz compcert-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')
| -rw-r--r-- | cfrontend/Cop.v | 4 | ||||
| -rw-r--r-- | cfrontend/Ctyping.v | 1 |
2 files changed, 3 insertions, 2 deletions
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index aa73abb0..143e87a3 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -140,8 +140,8 @@ Definition classify_cast (tfrom tto: type) : classify_cast_cases := | Tfloat F64 _, Tfloat F32 _ => cast_case_s2f | Tfloat F32 _, Tfloat F64 _ => cast_case_f2s (* To pointer types *) - | Tpointer _ _, Tint _ _ _ => - if Archi.ptr64 then cast_case_i2l Unsigned else cast_case_pointer + | Tpointer _ _, Tint _ si _ => + if Archi.ptr64 then cast_case_i2l si else cast_case_pointer | Tpointer _ _, Tlong _ _ => if Archi.ptr64 then cast_case_pointer else cast_case_l2i I32 Unsigned | Tpointer _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_pointer 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. |