Merge branch 'feature/kernel/cast-pointer-to-integer' into 'master'

[Kernel] Warns when converting a pointer into an integer without an explicit cast.

Closes #548

See merge request frama-c/frama-c!2172

src/kernel_internals/typing/cabs2cil.ml

@@ -2737,7 +2737,6 @@ let rec castTo ?(fromsource=false)
     (* Taking numerical address or calling an absolute location. Also
        accepted by gcc albeit with a warning. *)
     | TInt _, TPtr (TFun _, _) -> result
-    | TPtr (TFun _, _), TInt _ -> result
 
     (* pointer to potential function type. Note that we do not
        use unrollTypeDeep above in order to avoid needless divergence with
@@ -2770,7 +2769,14 @@ let rec castTo ?(fromsource=false)
 
     | TInt _, TPtr _ -> result
 
-    | TPtr _, TInt _ -> result
+    | TPtr _, TInt _ ->
+      if not fromsource
+      then
+        Kernel.warning
+          ~wkey:Kernel.wkey_int_conversion
+          ~current:true
+          "Conversion from a pointer to an integer without an explicit cast";
+      result
 
     | TArray _, TPtr _ -> result
 

src/kernel_services/plugin_entry_points/kernel.ml

@@ -145,6 +145,9 @@ let wkey_incompatible_types_call =
 let wkey_incompatible_pointer_types =
   register_warn_category "typing:incompatible-pointer-types"
 
+let wkey_int_conversion =
+  register_warn_category "typing:int-conversion"
+
 let wkey_cert_exp_46 = register_warn_category "CERT:EXP:46"
 
 let wkey_cert_msc_38 = register_warn_category "CERT:MSC:38"

src/kernel_services/plugin_entry_points/kernel.mli

@@ -138,6 +138,8 @@ val wkey_incompatible_types_call: warn_category
 
 val wkey_incompatible_pointer_types: warn_category
 
+val wkey_int_conversion: warn_category
+
 val wkey_cert_exp_46: warn_category
 
 val wkey_cert_msc_38: warn_category

src/plugins/wp/tests/wp_acsl/pointer.i

@@ -83,4 +83,4 @@ void absurd (int * q) { return; }
     ensures qed_ok: NotNull: p != \null ==> \result != 0 ;
     ensures qed_ok: IsNull:  p == \null ==> \result == 0 ;
 */
-int null (int *p) { return p; }
+int null (int *p) { return (int) p; }

src/plugins/wp/tests/wp_plugin/frame.i

@@ -32,7 +32,7 @@ int localref(int *p)
 //@ensures KO: \result == r ;
 int alias(int r)
 {
-  int p = &r ;
+  int p = (int) &r ;
   f();
   return r ;
 }

src/plugins/wp/tests/wp_usage/code_spec.i

@@ -37,7 +37,7 @@ void by_value_in_code(int x) {
 }
 
 void by_reference_in_code(int *p, int **qq) {
-  *p=(int *) 0;
+  *p=0;
   **qq=*p1;
 
 }

tests/builtins/alloc.c

@@ -51,7 +51,7 @@ void main_abs(int c)
   r = - (int) q;
 
   *(int*)0x104=0;
-  *r = r;
+  *r = (int) r;
 
   (*q)++;
   a = *q; /* it is incorrect to find 1 here */

tests/builtins/imprecise-malloc-free.c

@@ -9,7 +9,7 @@ extern int i;
 
 void main() {
   int size1, size2;
-  size1 = &size1 + i;
+  size1 = (int) (&size1 + i);
   size2 = i + ((int)&size2 >> 1);
   int *p = malloc((unsigned long)&i+(int)&i);
   int *q = malloc(size1);
@@ -18,9 +18,9 @@ void main() {
   Frama_C_show_each(p, q, r);
   Frama_C_show_each(p+(int)p);
 
-  *p = p+1;
-  *q = q+2;
-  *r = r+3;
+  *p = (int) (p+1);
+  *q = (int) (q+2);
+  *r = (int) (r+3);
 
   free(p+(int)p);
   free(q+(int)r);

tests/builtins/imprecise.c

@@ -19,7 +19,7 @@ void write_garbled() { // Write through a garbled mix
   int *p = (&j + (int) &k) - (int) &k; // creates a garbled mix
   *p = 1;
   Frama_C_dump_each();
-  *p = p;
+  *p = (int) p;
 }
 
 volatile int v, addr;
@@ -50,7 +50,7 @@ void abstract_structs() {
 //  v2 = v1;
   memset(&v3, -5, sizeof(v3)); // Also illegal, rejected by gcc
   int *p2 = ((int*)&v2)+1;
-  *p2 = &addr;
+  *p2 = (int) &addr;
 //  *t[5] = v2; // assigning incomplete type
   char *p4 = ((char*)&v5) + (short)v;
   *p4 = 18;
@@ -63,7 +63,7 @@ void abstract_structs() {
 void cast_address() {
   int x;
   int *p = &x;
-  char c1 = p;
+  char c1 = (char) p;
   char c2 = *((char*)&p);
   char c3 = *((char*)&p)+0;
 }

tests/builtins/long_init.c

@@ -31,7 +31,7 @@ double analyze(int *a, unsigned long *b, double *c) {
   return res;
 }
 
-char garbled_mix = "abc";
+char garbled_mix = (char) "abc";
 char *s = "abc";
 //int another_global = 42; // from init_global2.c
 //int yet_another_global = 43; // from init_global3.c
@@ -71,7 +71,7 @@ void init_inner(int n, char const *tea) {
   pr2 = &r2;
   pr_escaping = &r2;
   alloc1 = malloc(sizeof(int*));
-  *alloc1 = alloc1;
+  *alloc1 = (int) alloc1;
   alloc2 = malloc(2*sizeof(int));
   *alloc2 = 37;
   free(alloc2);

tests/builtins/long_init2.c

@@ -31,7 +31,7 @@ double analyze(int *a, unsigned long *b, double *c) {
   return res;
 }
 
-char garbled_mix = "abc";
+char garbled_mix = (char) "abc";
 char *s = "abc";
 int another_global = 42;
 //int yet_another_global = 43; // from init_global3.c
@@ -71,7 +71,7 @@ void init_inner(int n, char const *tea) {
   pr2 = &r2;
   pr_escaping = &r2;
   alloc1 = malloc(sizeof(int*));
-  *alloc1 = alloc1;
+  *alloc1 = (int) alloc1;
   alloc2 = malloc(2*sizeof(int));
   *alloc2 = 37;
   free(alloc2);

tests/builtins/long_init3.c

@@ -31,7 +31,7 @@ double analyze(int *a, unsigned long *b, double *c) {
   return res;
 }
 
-char garbled_mix = "abc";
+char garbled_mix = (char) "abc";
 char *s = "abc";
 int another_global = 42;
 int yet_another_global = 43;
@@ -71,7 +71,7 @@ void init_inner(int n, char const *tea) {
   pr2 = &r2;
   pr_escaping = &r2;
   alloc1 = malloc(sizeof(int*));
-  *alloc1 = alloc1;
+  *alloc1 = (int) alloc1;
   alloc2 = malloc(2*sizeof(int));
   *alloc2 = 37;
   free(alloc2);

tests/builtins/memchr.c

@@ -261,7 +261,7 @@ void memchr_escaping() {
   CHAR_ARRAY(s,4);
   {
     int x;
-    *((int *)s) = &x;
+    *((int *)s) = (int) &x;
   }
   IF_NONDET(s[0], 0);
   MEMCHR(RES, z1, s, 0, c, 4); // alarm

tests/builtins/memcpy.c

@@ -87,7 +87,7 @@ void main (int a, int b){
   memcpy(&v3, t+(int)t, sizeof(v1));
 
   memcpy(&v4 + (int)&v4, &v1, sizeof(v1)-20);
-  v4.y = &t[0];
+  v4.y = (int) &t[0];
   memcpy(&v5 + (int)&v5, &v4, sizeof(v4)-20);
 
   if (maybe) {

tests/builtins/oracle/alloc_weak.res.oracle

 [kernel] Parsing tests/builtins/alloc_weak.c (with preprocessing)
+[kernel:typing:int-conversion] tests/builtins/alloc_weak.c:37: Warning: 
+  Conversion from a pointer to an integer without an explicit cast
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed

tests/builtins/strchr.c

@@ -255,7 +255,7 @@ void strchr_escaping() {
   CHAR_ARRAY(s,4);
   {
     int x;
-    *((int *)s) = &x;
+    *((int *)s) = (int) &x;
   }
   IF_NONDET(s[0], 0);
   STRCHR(RES, z1, s, 0, c); // alarm

tests/builtins/strlen.c

@@ -219,7 +219,7 @@ void escaping() {
   char s[4];
   {
     int x;
-    *((int *)s) = &x;
+    *((int *)s) = (int) &x;
   }
   if (nondet) s[0] = 0;
   int z1 = strlen(s); // alarm

tests/builtins/strnlen2.c

@@ -193,7 +193,7 @@ void escaping() {
   CHAR_ARRAY(s,4);
   {
     int x;
-    *((int *)s) = &x;
+    *((int *)s) = (int) &x;
   }
   IF_NONDET(s[0], 0);
   RES z1 = strnlen(s, 4); // alarm

tests/builtins/wcslen.c

@@ -219,7 +219,7 @@ void escaping() {
   wchar_t s[4];
   {
     int x;
-    *((int *)s) = &x; *((int *)&s[1]) = &x; *((int *)&s[2]) = &x; *((int *)&s[3]) = &x;
+    *((int *)s) = (int)&x; *((int *)&s[1]) = (int)&x; *((int *)&s[2]) = (int)&x; *((int *)&s[3]) = (int)&x;
   }
   if (nondet) s[0] = 0;
   int z1 = wcslen(s); // alarm

tests/slicing/slice_no_body.i

@@ -24,5 +24,5 @@ int h (void) {
   G = f (4);
   if (G > 0)
     G = g (c);
-  return g;
+  return (int)g;
 }