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.

Author: bschommer

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

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.