diff options
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. |