[alias] no warning for the NULL pointer

src/plugins/alias/simplified.ml

@@ -49,7 +49,8 @@ exception Explicit_pointer_address of location
 
 let check_cast_compatibility e typ =
   let type_of_e = Cil.typeOf e in
-  if Cil.need_cast typ type_of_e then
+  (* emit a warning for unsafe cast, but not for the NULL pointer *)
+  if Cil.need_cast typ type_of_e && not (Cil.isZero e) then
     Options.warning
       ~once:true
       ~source:(fst @@ e.eloc)

src/plugins/alias/tests/basic/oracle/assignment1.res.oracle

 [kernel] Parsing assignment1.c (with preprocessing)
 [alias] analysing function: main
 [alias] analysing instruction: int *a = (int *)0;
-[alias:unsafe-cast] assignment1.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *a = (int *)0;  are  <none>
 [alias] analysing instruction: int *b = (int *)0;
-[alias:unsafe-cast] assignment1.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *b = (int *)0;  are  <none>
 [alias] analysing instruction: int *c = (int *)0;
-[alias:unsafe-cast] assignment1.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *c = (int *)0;  are  <none>
 [alias] analysing instruction: int *d = (int *)0;
-[alias:unsafe-cast] assignment1.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *d = (int *)0;  are  <none>
 [alias] analysing instruction: a = b;
 [alias] May-aliases after instruction  a = b;  are  {a, b}

src/plugins/alias/tests/basic/oracle/assignment2.res.oracle

 [kernel] Parsing assignment2.c (with preprocessing)
 [alias] analysing function: main
 [alias] analysing instruction: int **a = (int **)0;
-[alias:unsafe-cast] assignment2.c:8: Warning: unsafe cast from int to int **
 [alias] May-aliases after instruction  int **a = (int **)0;  are  <none>
 [alias] analysing instruction: int *b = (int *)0;
-[alias:unsafe-cast] assignment2.c:8: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *b = (int *)0;  are  <none>
 [alias] analysing instruction: int **c = (int **)0;
-[alias:unsafe-cast] assignment2.c:8: Warning: unsafe cast from int to int **
 [alias] May-aliases after instruction  int **c = (int **)0;  are  <none>
 [alias] analysing instruction: int *d = (int *)0;
-[alias:unsafe-cast] assignment2.c:8: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *d = (int *)0;  are  <none>
 [alias] analysing instruction: *a = b;
 [alias] May-aliases after instruction  *a = b;  are  {*a, b}

src/plugins/alias/tests/basic/oracle/assignment3.res.oracle

 [kernel] Parsing assignment3.c (with preprocessing)
 [alias] analysing function: main
 [alias] analysing instruction: int *a = (int *)0;
-[alias:unsafe-cast] assignment3.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *a = (int *)0;  are  <none>
 [alias] analysing instruction: int b = 0;
 [alias] May-aliases after instruction  int b = 0;  are  <none>
 [alias] analysing instruction: int *c = (int *)0;
-[alias:unsafe-cast] assignment3.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *c = (int *)0;  are  <none>
 [alias] analysing instruction: a = & b;
 [alias] May-aliases after instruction  a = & b;  are  <none>

src/plugins/alias/tests/basic/oracle/assignment4.res.oracle

 [kernel] Parsing assignment4.c (with preprocessing)
 [alias] analysing function: main
 [alias] analysing instruction: int **a = (int **)0;
-[alias:unsafe-cast] assignment4.c:8: Warning: unsafe cast from int to int **
 [alias] May-aliases after instruction  int **a = (int **)0;  are  <none>
 [alias] analysing instruction: int *b = (int *)0;
-[alias:unsafe-cast] assignment4.c:8: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *b = (int *)0;  are  <none>
 [alias] analysing instruction: int **c = (int **)0;
-[alias:unsafe-cast] assignment4.c:8: Warning: unsafe cast from int to int **
 [alias] May-aliases after instruction  int **c = (int **)0;  are  <none>
 [alias] analysing instruction: int *d = (int *)0;
-[alias:unsafe-cast] assignment4.c:8: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *d = (int *)0;  are  <none>
 [alias] analysing instruction: *a = b;
 [alias] May-aliases after instruction  *a = b;  are  {*a, b}

src/plugins/alias/tests/basic/oracle/assignment5.res.oracle

 [kernel] Parsing assignment5.c (with preprocessing)
 [alias] analysing function: main
 [alias] analysing instruction: int ***a = (int ***)0;
-[alias:unsafe-cast] assignment5.c:7: Warning: unsafe cast from int to int ***
 [alias] May-aliases after instruction  int ***a = (int ***)0;  are  <none>
 [alias] analysing instruction: int **b = (int **)0;
-[alias:unsafe-cast] assignment5.c:7: Warning: unsafe cast from int to int **
 [alias] May-aliases after instruction  int **b = (int **)0;  are  <none>
 [alias] analysing instruction: int *c = (int *)0;
-[alias:unsafe-cast] assignment5.c:7: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *c = (int *)0;  are  <none>
 [alias] analysing instruction: int *d = (int *)0;
-[alias:unsafe-cast] assignment5.c:7: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *d = (int *)0;  are  <none>
 [alias] analysing instruction: *a = b;
 [alias] May-aliases after instruction  *a = b;  are  {*a, b}

src/plugins/alias/tests/basic/oracle/cast1.res.oracle

 [kernel] Parsing cast1.c (with preprocessing)
 [alias] analysing function: main
 [alias] analysing instruction: int *a = (int *)0;
-[alias:unsafe-cast] cast1.c:8: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *a = (int *)0;  are  <none>
 [alias] analysing instruction: int *b = (int *)0;
-[alias:unsafe-cast] cast1.c:8: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *b = (int *)0;  are  <none>
 [alias] analysing instruction: float *c = (float *)0;
-[alias:unsafe-cast] cast1.c:9: Warning: unsafe cast from int to float *
 [alias] May-aliases after instruction  float *c = (float *)0;  are  <none>
 [alias] analysing instruction: float *d = (float *)0;
-[alias:unsafe-cast] cast1.c:9: Warning: unsafe cast from int to float *
 [alias] May-aliases after instruction  float *d = (float *)0;  are  <none>
 [alias] analysing instruction: a = (int *)c;
 [alias:unsafe-cast] cast1.c:10: Warning: unsafe cast from float * to int *

src/plugins/alias/tests/basic/oracle/conditional1.res.oracle

 [kernel] Parsing conditional1.c (with preprocessing)
 [alias] analysing function: main
 [alias] analysing instruction: int *a = (int *)0;
-[alias:unsafe-cast] conditional1.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *a = (int *)0;  are  <none>
 [alias] analysing instruction: int *b = (int *)0;
-[alias:unsafe-cast] conditional1.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *b = (int *)0;  are  <none>
 [alias] analysing instruction: int *c = (int *)0;
-[alias:unsafe-cast] conditional1.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *c = (int *)0;  are  <none>
 [alias] analysing instruction: a = b;
 [alias] May-aliases after instruction  a = b;  are  {a, b}

src/plugins/alias/tests/basic/oracle/function1.res.oracle

 [kernel] Parsing function1.c (with preprocessing)
 [alias] analysing function: main
 [alias] analysing instruction: int *a = (int *)0;
-[alias:unsafe-cast] function1.c:16: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *a = (int *)0;  are  <none>
 [alias] analysing instruction: int *b = (int *)0;
-[alias:unsafe-cast] function1.c:16: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *b = (int *)0;  are  <none>
 [alias] analysing instruction: int *c = (int *)0;
-[alias:unsafe-cast] function1.c:16: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *c = (int *)0;  are  <none>
 [alias] analysing instruction: int *d = (int *)0;
-[alias:unsafe-cast] function1.c:16: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *d = (int *)0;  are  <none>
 [alias] analysing instruction: swap(a,b);
 [alias] analysing function: swap
 [alias] analysing instruction: int *z = (int *)0;
-[alias:unsafe-cast] function1.c:7: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *z = (int *)0;  are  <none>
 [alias] analysing instruction: z = x;
 [alias] May-aliases after instruction  z = x;  are  {x, z}

src/plugins/alias/tests/basic/oracle/function2.res.oracle

@@ -49,15 +49,12 @@
 [alias] May-aliases at the end of function lrand48: ⊥
 [alias] analysing function: main
 [alias] analysing instruction: int *a = (int *)0;
-[alias:unsafe-cast] function2.c:14: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *a = (int *)0;  are  <none>
 [alias] analysing instruction: int *b = (int *)0;
-[alias:unsafe-cast] function2.c:14: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *b = (int *)0;  are  <none>
 [alias] analysing instruction: a = my_malloc(2);
 [alias] analysing function: my_malloc
 [alias] analysing instruction: int *res = (int *)0;
-[alias:unsafe-cast] function2.c:7: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *res = (int *)0;  are  <none>
 [alias] analysing instruction: res = (int *)malloc((size_t)size);
 [alias] May-aliases after instruction  res = (int *)malloc((size_t)size);  are

src/plugins/alias/tests/basic/oracle/function3.res.oracle

@@ -7,21 +7,16 @@
 [alias] analysing instruction: y = tmp;
 [alias] May-aliases after instruction  y = tmp;  are  {x, y, tmp}
 [alias] analysing instruction: __retres = (void *)0;
-[alias:unsafe-cast] function3.c:14: Warning: unsafe cast from int to void *
 [alias] May-aliases after instruction  __retres = (void *)0;  are  {x, y, tmp}
 [alias] May-aliases at the end of function f1: {x, y, tmp}
 [alias] analysing function: main
 [alias] analysing instruction: int *a = (int *)0;
-[alias:unsafe-cast] function3.c:19: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *a = (int *)0;  are  <none>
 [alias] analysing instruction: int *b = (int *)0;
-[alias:unsafe-cast] function3.c:19: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *b = (int *)0;  are  <none>
 [alias] analysing instruction: int *c = (int *)0;
-[alias:unsafe-cast] function3.c:19: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *c = (int *)0;  are  <none>
 [alias] analysing instruction: int *d = (int *)0;
-[alias:unsafe-cast] function3.c:19: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *d = (int *)0;  are  <none>
 [alias] analysing instruction: f1(a,b);
 [alias] May-aliases after instruction  f1(a,b);  are  {a, b}

src/plugins/alias/tests/basic/oracle/function4.res.oracle

@@ -3,10 +3,8 @@
 [alias] May-aliases at the end of function addr: <none>
 [alias] analysing function: main
 [alias] analysing instruction: int *a = (int *)0;
-[alias:unsafe-cast] function4.c:11: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *a = (int *)0;  are  <none>
 [alias] analysing instruction: int *b = (int *)0;
-[alias:unsafe-cast] function4.c:11: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *b = (int *)0;  are  <none>
 [alias] analysing instruction: int c = 0;
 [alias] May-aliases after instruction  int c = 0;  are  <none>

src/plugins/alias/tests/basic/oracle/function5.res.oracle

@@ -9,13 +9,10 @@
 [alias] May-aliases at the end of function choice: {x, y, __retres}
 [alias] analysing function: main
 [alias] analysing instruction: int *a = (int *)0;
-[alias:unsafe-cast] function5.c:16: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *a = (int *)0;  are  <none>
 [alias] analysing instruction: int *b = (int *)0;
-[alias:unsafe-cast] function5.c:16: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *b = (int *)0;  are  <none>
 [alias] analysing instruction: int *c = (int *)0;
-[alias:unsafe-cast] function5.c:16: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *c = (int *)0;  are  <none>
 [alias] analysing instruction: c = choice(a,b);
 [alias] May-aliases after instruction  c = choice(a,b);  are  {a, b, c}

src/plugins/alias/tests/basic/oracle/function6.res.oracle

 [kernel] Parsing function6.c (with preprocessing)
 [alias] analysing function: main
 [alias] analysing instruction: int *a = (int *)0;
-[alias:unsafe-cast] function6.c:15: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *a = (int *)0;  are  <none>
 [alias] analysing instruction: int *b = (int *)0;
-[alias:unsafe-cast] function6.c:15: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *b = (int *)0;  are  <none>
 [alias] analysing instruction: int *c = (int *)0;
-[alias:unsafe-cast] function6.c:15: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *c = (int *)0;  are  <none>
 [alias] analysing instruction: int *d = (int *)0;
-[alias:unsafe-cast] function6.c:15: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *d = (int *)0;  are  <none>
 [alias] analysing instruction: swap(a,b);
 [alias] analysing function: swap

src/plugins/alias/tests/basic/oracle/globctr.res.oracle

@@ -7,10 +7,8 @@
 [alias] May-aliases at the end of function f: <none>
 [alias] analysing function: main
 [alias] analysing instruction: int *a = (int *)0;
-[alias:unsafe-cast] globctr.c:8: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *a = (int *)0;  are  <none>
 [alias] analysing instruction: int *b = (int *)0;
-[alias:unsafe-cast] globctr.c:8: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *b = (int *)0;  are  <none>
 [alias] analysing instruction: f(a);
 [alias] May-aliases after instruction  f(a);  are  <none>

src/plugins/alias/tests/basic/oracle/switch1.res.oracle

 [kernel] Parsing switch1.c (with preprocessing)
 [alias] analysing function: main
 [alias] analysing instruction: int *a = (int *)0;
-[alias:unsafe-cast] switch1.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *a = (int *)0;  are  <none>
 [alias] analysing instruction: int *b = (int *)0;
-[alias:unsafe-cast] switch1.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *b = (int *)0;  are  <none>
 [alias] analysing instruction: int *c = (int *)0;
-[alias:unsafe-cast] switch1.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *c = (int *)0;  are  <none>
 [alias] analysing instruction: int *d = (int *)0;
-[alias:unsafe-cast] switch1.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *d = (int *)0;  are  <none>
 [alias] analysing instruction: int e = 0;
 [alias] May-aliases after instruction  int e = 0;  are  <none>

src/plugins/alias/tests/basic/oracle/switch2.res.oracle

 [kernel] Parsing switch2.c (with preprocessing)
 [alias] analysing function: main
 [alias] analysing instruction: int *a = (int *)0;
-[alias:unsafe-cast] switch2.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *a = (int *)0;  are  <none>
 [alias] analysing instruction: int *b = (int *)0;
-[alias:unsafe-cast] switch2.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *b = (int *)0;  are  <none>
 [alias] analysing instruction: int *c = (int *)0;
-[alias:unsafe-cast] switch2.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *c = (int *)0;  are  <none>
 [alias] analysing instruction: int *d = (int *)0;
-[alias:unsafe-cast] switch2.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *d = (int *)0;  are  <none>
 [alias] analysing instruction: int e = 0;
 [alias] May-aliases after instruction  int e = 0;  are  <none>

src/plugins/alias/tests/basic/oracle/while_for1.res.oracle

@@ -49,7 +49,6 @@
 [alias] May-aliases at the end of function lrand48: ⊥
 [alias] analysing function: main
 [alias] analysing instruction: int *s = (int *)0;
-[alias:unsafe-cast] while_for1.c:8: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *s = (int *)0;  are  <none>
 [alias] analysing instruction: int idx = 0;
 [alias] May-aliases after instruction  int idx = 0;  are  <none>

src/plugins/alias/tests/basic/oracle/while_for2.res.oracle

 [kernel] Parsing while_for2.c (with preprocessing)
 [alias] analysing function: main
 [alias] analysing instruction: int *a = (int *)0;
-[alias:unsafe-cast] while_for2.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *a = (int *)0;  are  <none>
 [alias] analysing instruction: int *b = (int *)0;
-[alias:unsafe-cast] while_for2.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *b = (int *)0;  are  <none>
 [alias] analysing instruction: int *c = (int *)0;
-[alias:unsafe-cast] while_for2.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *c = (int *)0;  are  <none>
 [alias] analysing instruction: a = b;
 [alias] May-aliases after instruction  a = b;  are  {a, b}

src/plugins/alias/tests/basic/oracle/while_for3.res.oracle

 [kernel] Parsing while_for3.c (with preprocessing)
 [alias] analysing function: main
 [alias] analysing instruction: int *a = (int *)0;
-[alias:unsafe-cast] while_for3.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *a = (int *)0;  are  <none>
 [alias] analysing instruction: int *b = (int *)0;
-[alias:unsafe-cast] while_for3.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *b = (int *)0;  are  <none>
 [alias] analysing instruction: int *c = (int *)0;
-[alias:unsafe-cast] while_for3.c:6: Warning: unsafe cast from int to int *
 [alias] May-aliases after instruction  int *c = (int *)0;  are  <none>
 [alias] analysing instruction: int i = 0;
 [alias] May-aliases after instruction  int i = 0;  are  <none>