diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-13 22:22:14 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-13 22:22:14 +0100 |
| commit | bc5b28ec16590c52da2772b1cc296247ccf528c1 (patch) | |
| tree | d74f1725b8bc7b2017c13ffc80ad667bff11917e /cfrontend | |
| parent | 117a26880e27ae7d8efcb26d194c5ded3be642d6 (diff) | |
| parent | 9b881b7928ab7d21e9981133bef5b26e33b6cd9d (diff) | |
| download | compcert-kvx-bc5b28ec16590c52da2772b1cc296247ccf528c1.tar.gz compcert-kvx-bc5b28ec16590c52da2772b1cc296247ccf528c1.zip | |
Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge
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. |