diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 5623a49326f7b2fa2c1af1c4c7cddec14c543e6f..845919d8d1d0f03e82e61fb3fcc0d2d8fc5f221a 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/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
 
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 9c0399ad475d798fd4f968f5fae4bf5175b29eb7..0c95ee14a2c78bdc8ccf69d66875628a261e63c9 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/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"
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index bc130617463ae326596dafb96a28133d71449c03..06e4720e294a3e4c737f3c4adce2f988dbe72670 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/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
diff --git a/src/plugins/wp/tests/wp_acsl/pointer.i b/src/plugins/wp/tests/wp_acsl/pointer.i
index d0d0f10cb85a0737f5b028fc949bfc6137e867cd..168d9b15459d12c414362372de20bcebfba81ea8 100644
--- a/src/plugins/wp/tests/wp_acsl/pointer.i
+++ b/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; }
diff --git a/src/plugins/wp/tests/wp_plugin/frame.i b/src/plugins/wp/tests/wp_plugin/frame.i
index 912625538c990094b2e828bac15cef5d293a2e4e..1292d5e277bbfb4698a455092cbcd1ef73038452 100644
--- a/src/plugins/wp/tests/wp_plugin/frame.i
+++ b/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 ;
 }
diff --git a/src/plugins/wp/tests/wp_usage/code_spec.i b/src/plugins/wp/tests/wp_usage/code_spec.i
index b325e6d35247bc48ae65c38faff8609299caf2b4..30c1819dcc10e3e11f611eaea823f56e05b53864 100644
--- a/src/plugins/wp/tests/wp_usage/code_spec.i
+++ b/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;
 
 }
diff --git a/tests/builtins/alloc.c b/tests/builtins/alloc.c
index 51579426082c5843d774bd7665136ad3954eb7d1..33f24cdc7d6562f40487a3693fa2b380742edc42 100644
--- a/tests/builtins/alloc.c
+++ b/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 */
diff --git a/tests/builtins/imprecise-malloc-free.c b/tests/builtins/imprecise-malloc-free.c
index 0e5bcc75dcb45755de57ede0ab97fbe1d0095472..8c3a3bc6021c3c6247b3e505e483ea7afa9cca40 100644
--- a/tests/builtins/imprecise-malloc-free.c
+++ b/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);
diff --git a/tests/builtins/imprecise.c b/tests/builtins/imprecise.c
index c462cafa2bffce124b4ab965ba77eeaff1053c7b..9a82adfd802158be07d033d1daaf18c74f45d011 100644
--- a/tests/builtins/imprecise.c
+++ b/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;
 }
diff --git a/tests/builtins/long_init.c b/tests/builtins/long_init.c
index 9bc8495470a27d634efc83e19c39c8071fc8dc10..c244b17b5e377a30cd1b3c1707309d7afd422031 100644
--- a/tests/builtins/long_init.c
+++ b/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);
diff --git a/tests/builtins/long_init2.c b/tests/builtins/long_init2.c
index 564442c150e071b35b31d1cc716752574113d705..065358b2e68c111dec1dbeaaa9636b5bc9ee7e69 100644
--- a/tests/builtins/long_init2.c
+++ b/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);
diff --git a/tests/builtins/long_init3.c b/tests/builtins/long_init3.c
index e5e30d8ce93bccb314cbdb19d5c3929b03dca33f..b3b97e7aee3843079508e5a32d403045ec253e08 100644
--- a/tests/builtins/long_init3.c
+++ b/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);
diff --git a/tests/builtins/memchr.c b/tests/builtins/memchr.c
index 6a3f5b4b777fa9347e93fbca99606d4031b9f7c2..7b39c55a84529e8cdd1e28b6fe2637e7f4fad4eb 100644
--- a/tests/builtins/memchr.c
+++ b/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
diff --git a/tests/builtins/memcpy.c b/tests/builtins/memcpy.c
index 8ef2b0ac8551bf4898b88a5605f518ea0efbdf50..3b438a803377db9cfbd9a59047e0389b70807c0d 100644
--- a/tests/builtins/memcpy.c
+++ b/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) {
diff --git a/tests/builtins/oracle/alloc_weak.res.oracle b/tests/builtins/oracle/alloc_weak.res.oracle
index 2ec25a88debd1b7cbc0849be4ba6dc6e570937c9..8a75c2737771cbf31721f82e0c5357668bcef26f 100644
--- a/tests/builtins/oracle/alloc_weak.res.oracle
+++ b/tests/builtins/oracle/alloc_weak.res.oracle
@@ -1,4 +1,6 @@
 [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
diff --git a/tests/builtins/strchr.c b/tests/builtins/strchr.c
index 398a3d3c25cc3925cdd5fd73fbc4793e4cb6353f..e3678b241247fc7dbf44ea6e501954fd6267c6fe 100644
--- a/tests/builtins/strchr.c
+++ b/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
diff --git a/tests/builtins/strlen.c b/tests/builtins/strlen.c
index 91cf082a9ab75f2a1500cd3170dc0fafe4569e32..619b8a59cea78efbc477ebb2ee84ba8817105093 100644
--- a/tests/builtins/strlen.c
+++ b/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
diff --git a/tests/builtins/strnlen2.c b/tests/builtins/strnlen2.c
index 9ea4b3c856fbeafe45a4b7eea93baf93c5f4ab0a..241fb154832c0be774de85abdbca880c0a5340e8 100644
--- a/tests/builtins/strnlen2.c
+++ b/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
diff --git a/tests/builtins/wcslen.c b/tests/builtins/wcslen.c
index 906cc2d487f187e2fb1c8c90de19bea7bed56419..dea7cd1aad9aba23f6b081452fb1dee572a146fb 100644
--- a/tests/builtins/wcslen.c
+++ b/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
diff --git a/tests/slicing/slice_no_body.i b/tests/slicing/slice_no_body.i
index 9c249f20d9f10a391b1ad939bb7e8605473596a7..2c58ae1277dcdd908e0b5a56197d85d042d07856 100644
--- a/tests/slicing/slice_no_body.i
+++ b/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;
 }
diff --git a/tests/syntax/merge_loc.i b/tests/syntax/merge_loc.i
index 91608458af61dc964abf13056fdb07163cb87be1..8f08173f151e39627df74d38288858a1a2d9d68d 100644
--- a/tests/syntax/merge_loc.i
+++ b/tests/syntax/merge_loc.i
@@ -20,4 +20,4 @@ extern int baz;
 
 extern int baz;
 
-int z = &baz;
+int z = (int) &baz;
diff --git a/tests/syntax/type_redef.i b/tests/syntax/type_redef.i
index 11cbac589195649a9565fbf93bd965e79a2ad9a2..28d719f063809920a5154b132e156ec2b7a78f05 100644
--- a/tests/syntax/type_redef.i
+++ b/tests/syntax/type_redef.i
@@ -61,7 +61,7 @@ typedef int magic;
 void i() {
   typedef void (*magic)(void); //valid
   { typedef struct {int obj;} magic; } //valid
-  magic m = g; //valid (test scoping of local typedef)
+  magic m = (magic) g; //valid (test scoping of local typedef)
 }
 magic m = 2; //valid (test scoping of local typedef)
 
diff --git a/tests/value/addition.i b/tests/value/addition.i
index ed227add3f673ce1d7f11adc306f8113dfa01f43..98f1a90a1bd68c46596e419037578be602011a78 100644
--- a/tests/value/addition.i
+++ b/tests/value/addition.i
@@ -35,15 +35,15 @@ int main(int u2, int u3, int u4)
 
   p2 = ~((int)&p1);
 
-  p3 = &(t[(char)(&p1)]);
+  p3 = (int) &(t[(char)(&p1)]);
 
-  p4 = &(tt[(char)(&p1)].a);
+  p4 = (int) &(tt[(char)(&p1)].a);
 
-  p5 = &(ttt[(char)(&p1)][(char)&p2]);
+  p5 = (int) &(ttt[(char)(&p1)][(char)&p2]);
 
-  p6 = &(ttt[(char)(&p1)][u2]);
+  p6 = (int) &(ttt[(char)(&p1)][u2]);
 
-  p7 = &(ttt[u2][(char)(&p2)]);
+  p7 = (int) &(ttt[u2][(char)(&p2)]);
 
   p8 = (&p1 + 1) < &p2;
 
diff --git a/tests/value/array_ptr.i b/tests/value/array_ptr.i
index 74ddfa99602e1c7568926960410af68800606211..2305c9fb1ab1538f2c32d762bef108b9ede3f265 100644
--- a/tests/value/array_ptr.i
+++ b/tests/value/array_ptr.i
@@ -11,6 +11,6 @@ int f(param_check **x) {
 param_check l={1};
 
 int main() {
-  int g = &l;
+  int g = (int) &l;
   f((param_check **)&g);
 }
diff --git a/tests/value/bitfield.i b/tests/value/bitfield.i
index 2fb52b64f96093712e675247e38975766c49a633..595e57138722f50050cc50b5bc27dcdaa4533292 100644
--- a/tests/value/bitfield.i
+++ b/tests/value/bitfield.i
@@ -120,14 +120,14 @@ void main_old (){
 
   h.a = VV;
 
-  v.c = &v;
-  v.d = &v + 1;
+  v.c = (int) &v;
+  v.d = (int) (&v + 1);
   v.d = v.d + 1;
   v.a = 4;
   v.b = 7;
   f(v.b);
   h.b = foo + foo + h.a + h.b;
-  h.c = &v +1;
+  h.c = (int) (&v +1);
 
   k8.b = 8;
   kr8.b = return_8();
diff --git a/tests/value/call_simple.i b/tests/value/call_simple.i
index 9c259df2d066b8bb65d278e79e7aa536a9aeb503..3447eff300e65df8695e892242ef8a599982adfa 100644
--- a/tests/value/call_simple.i
+++ b/tests/value/call_simple.i
@@ -4,7 +4,7 @@ void f(int* a,int b,int c) {
   int *i=a;
   *i = 0;
   a = 0;
-  X = a+b+c;
+  X = (int) (a+b+c);
 }
 
 int main (int ll) {
diff --git a/tests/value/cmp_ptr.i b/tests/value/cmp_ptr.i
index 0d499b504eb8f99916d6587a98920d6df884e669..198a11aacafb3b00f5ac7bc29616a246c9dfba81 100644
--- a/tests/value/cmp_ptr.i
+++ b/tests/value/cmp_ptr.i
@@ -20,7 +20,7 @@ int main (int u) {
   
   if (p >= &(T[5])) {*p=88;*q=77;}
   x = !(&y+2);
-  *(int*)&ff = &y + 2;
+  *(int*)&ff = (int) (&y + 2);
   y = !ff;
 
   
diff --git a/tests/value/context_free.i b/tests/value/context_free.i
index c53e2fabea58b76808b04c0a7cd8ba9f242667bf..67ecd1b2ea552d2ceaf2f35225959450711bd72f 100644
--- a/tests/value/context_free.i
+++ b/tests/value/context_free.i
@@ -58,7 +58,7 @@ void f(int x, float y, int **p, int (*g)(char const*), void *vv, void **vvv, int
   char* pvoid = svoid.p;
   *pvoid = 1;
   pvoid = qvoid;
-  *pvoid = &pvoid;
+  *pvoid = (char) &pvoid;
   if (vol) { g("toto"); }
 
 }
diff --git a/tests/value/downcast.i b/tests/value/downcast.i
index c375fa7c92f7cccc2bf1aad3a02fa6576e55fd62..e979236ea122b6149c761eb12b5af28192441efa 100644
--- a/tests/value/downcast.i
+++ b/tests/value/downcast.i
@@ -88,9 +88,9 @@ void main6_val_warn_converted_signed() {
   }
   if (v) {
     int *p = &v;
-    int x = p; // No warning as an address fits in an integer.
-    short y = p; // Warnings, as an address may not fit in short.
-    unsigned short z = p; // No warninng on unsigned casts.
+    int x = (int) p; // No warning as an address fits in an integer.
+    short y = (short) p; // Warnings, as an address may not fit in short.
+    unsigned short z = (unsigned short) p; // No warninng on unsigned casts.
   }
 }
 
diff --git a/tests/value/from_call.i b/tests/value/from_call.i
index 4ca66207715c4824e3a85ea245a3407362d9adf0..54942abc2008129dc2246818b5ad9c6212d8a156 100644
--- a/tests/value/from_call.i
+++ b/tests/value/from_call.i
@@ -67,8 +67,8 @@ int access_tab(int ind)
 }
 
 int AA,AR,AS;
-int At[2]={&AA};
-int Ar[2]={&AA};
+int At[2]={(int)&AA};
+int Ar[2]={(int)&AA};
 int *Ap=At;
 
 /*@ assigns AR \from Ap[..] ;
diff --git a/tests/value/from_ptr.i b/tests/value/from_ptr.i
index 010d07507e8e7cace74abdaf06fab958721b8f62..2910e0d3451455f017d16b77539f21b9d82ab121 100644
--- a/tests/value/from_ptr.i
+++ b/tests/value/from_ptr.i
@@ -9,8 +9,8 @@ int p[10][10][10]={0};
 long *q;
 
 void main(int c) {
-  i = &p[11];
-  i = &p[10];
+  i = (long) &p[11];
+  i = (long) &p[10];
 
   if (c)
     // This branch is assumed to be dead since "i" is an invalid pointer.
@@ -21,8 +21,8 @@ void main(int c) {
 }
 
 void main1(int c) {
-  i = &p[1];
-  i = &p[0];
+  i = (long) &p[1];
+  i = (long) &p[0];
 
   if (c) *((int*)i) = a;
 
diff --git a/tests/value/join_misaligned.i b/tests/value/join_misaligned.i
index 800a8e72bcbbfd5c55ebd0e73d95821692e6f419..52e76f487c5f2defacbc432c816b42f96549e316 100644
--- a/tests/value/join_misaligned.i
+++ b/tests/value/join_misaligned.i
@@ -20,7 +20,7 @@ void main(int c)
       ((char*)u)[6]='c';
       *((short*)((char*)v+6))=0x44444444;
       *((short*)((char*)w+6))=57;
-      *((int*)((char*)y+6))=&t;
+      *((int*)((char*)y+6))= (int) &t;
       *((short*)(&z[3])) = 0x1111;
       *((short*) &a) = 0xFFFF;
       *((short*) &a+1) = 0xFFFF;
@@ -34,7 +34,7 @@ void main(int c)
       x[0]=1;
       x[1]=0;
       x[2]=1;
-      *((int*)((char*)y+7))=&u;
+      *((int*)((char*)y+7))= (int) &u;
       a = va;
       a <<= 12;
       a--;
diff --git a/tests/value/mini_pointrer.i b/tests/value/mini_pointrer.i
index 1e9c9b3272e7d171a26770126a72e9f17438dff6..5cfc288a044a616dcd2eb3d2a65ea3d98767140d 100644
--- a/tests/value/mini_pointrer.i
+++ b/tests/value/mini_pointrer.i
@@ -3,7 +3,7 @@ int**ppp;
 int pp[2];
 int p;
 void main(int c1, int c2, int c3) {
-  pp [c1] = &T[c1];
+  pp [c1] = (int) &T[c1];
   if (c2) ppp = &pp; else ppp = &T[-1];
   **ppp=9;
  
diff --git a/tests/value/nonlin.c b/tests/value/nonlin.c
index e87dec750c6bcf3352b6e4a15a0cdf01f3c60c8c..173929f555a96b0ca01f8e7585879fb4895598af 100644
--- a/tests/value/nonlin.c
+++ b/tests/value/nonlin.c
@@ -20,7 +20,7 @@ void subdivide_pointer () {
      reduction, as it cannot improve the bounds of the result). */
   y = *(p + i - i);
   /* The splitted lvalue contains a pointer value: no subdivision. */
-  i = v ? i : &x;
+  i = v ? i : (int) &x;
   y = *(p + i - i);
 }
 
diff --git a/tests/value/not_ct_array_arg.i b/tests/value/not_ct_array_arg.i
index 8390478b48446cec8113107d9fa9d718e1cfddca..e5fd2a58500b58d753d61ea019083be9e0fc8d67 100644
--- a/tests/value/not_ct_array_arg.i
+++ b/tests/value/not_ct_array_arg.i
@@ -9,7 +9,7 @@ volatile int v;
 void main(int a, int tb[10][a], int tc[a][10]) {
   *(int*)tb = 1;
   Frama_C_dump_each();
-  tb[9][100] = &tb;
+  tb[9][100] = (int) &tb;
   Frama_C_dump_each();
   tc[1][1] = 3;
   if (v)
diff --git a/tests/value/offset_top.i b/tests/value/offset_top.i
index 31e6080d55d93289f89b3d271cca4ede3e64cf98..622fb05071d988ce41f4cd37df1af1151f4af73a 100644
--- a/tests/value/offset_top.i
+++ b/tests/value/offset_top.i
@@ -7,5 +7,5 @@ int TAB[10];
 
 void main() {
   int i;
-  i = &TAB[*T];
+  i = (int) &TAB[*T];
 }
diff --git a/tests/value/oracle/bitfield.res.oracle b/tests/value/oracle/bitfield.res.oracle
index 33cb56816c05377a097ed27b988f80e50b2408b6..05b0967b0520a71f78f122b82d7b572800408561 100644
--- a/tests/value/oracle/bitfield.res.oracle
+++ b/tests/value/oracle/bitfield.res.oracle
@@ -550,8 +550,8 @@ void main_old(void)
   else Frama_C_show_each(3);
   VV = (unsigned int)h.a;
   h.a = (unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(2))))VV;
-  v.c = (int __attribute__((__FRAMA_C_BITFIELD_SIZE__(22))))(& v);
-  v.d = (int __attribute__((__FRAMA_C_BITFIELD_SIZE__(32))))(& v + 1);
+  v.c = (int __attribute__((__FRAMA_C_BITFIELD_SIZE__(22))))((int)(& v));
+  v.d = (int __attribute__((__FRAMA_C_BITFIELD_SIZE__(32))))((int)(& v + 1));
   /*@ assert Eva: signed_overflow: -2147483648 ≤ (int)v.d + 1; */
   /*@ assert Eva: signed_overflow: (int)v.d + 1 ≤ 2147483647; */
   v.d = (int __attribute__((__FRAMA_C_BITFIELD_SIZE__(32))))((int)v.d + 1);
@@ -561,7 +561,7 @@ void main_old(void)
   /*@ assert Eva: signed_overflow: -2147483648 ≤ foo + foo; */
   /*@ assert Eva: signed_overflow: foo + foo ≤ 2147483647; */
   h.b = (int __attribute__((__FRAMA_C_BITFIELD_SIZE__(4))))(((foo + foo) + (int)h.a) + (int)h.b);
-  h.c = (int __attribute__((__FRAMA_C_BITFIELD_SIZE__(22))))(& v + 1);
+  h.c = (int __attribute__((__FRAMA_C_BITFIELD_SIZE__(22))))((int)(& v + 1));
   k8.b = (int __attribute__((__FRAMA_C_BITFIELD_SIZE__(4))))8;
   tmp = return_8();
   kr8.b = (int __attribute__((__FRAMA_C_BITFIELD_SIZE__(4))))tmp;
diff --git a/tests/value/oracle/pointer_int_cast.res.oracle b/tests/value/oracle/pointer_int_cast.res.oracle
index 1348a0a3af6be94ec73e01e8b8f65b5ec8422b72..078dfbbd5bee8472325f2b748799bbafe9459628 100644
--- a/tests/value/oracle/pointer_int_cast.res.oracle
+++ b/tests/value/oracle/pointer_int_cast.res.oracle
@@ -1,4 +1,6 @@
 [kernel] Parsing tests/value/pointer_int_cast.i (no preprocessing)
+[kernel:typing:int-conversion] tests/value/pointer_int_cast.i:9: Warning: 
+  Conversion from a pointer to an integer without an explicit cast
 [eva] Analyzing a complete application starting at g
 [eva] Computing initial state
 [eva] Initial state computed
diff --git a/tests/value/origin.i b/tests/value/origin.i
index cf5adb70c04273207b229e8546ba5b04a6af375f..4be9a4a8f122b25568557980c4387a7ff6b3b21a 100644
--- a/tests/value/origin.i
+++ b/tests/value/origin.i
@@ -18,7 +18,7 @@ void origin_arithmetic_1(void) {
 void origin_arithmetic_2(int c1) {
   pa2 = (int*)(-(int)ta2);
   qa2 = c1 ? pa2 : (int*)(-(int)tta2);
-  *qa2 = &aa2;
+  *qa2 = (int) &aa2;
 }
 /************/
 void origin_arithmetic_3(void) {
diff --git a/tests/value/period.c b/tests/value/period.c
index 3b1ec68adec0992c44e28f0db0570eb350282365..5df43565146d323a5ac703cd79ee0800ed357e96 100644
--- a/tests/value/period.c
+++ b/tests/value/period.c
@@ -52,5 +52,5 @@ void main()
   *p = 1;
   p = (&g + (int)&g) - (int)&g; // creates a garbled mix
   int vg = *p;
-  *p = &vg;
+  *p = (int) &vg;
 }
diff --git a/tests/value/reading_null.i b/tests/value/reading_null.i
index 088ddb074bb8d841c17e85f04ba8e80557d0ab4f..1c0589b1d40018d09ac518a3dd790949bab88d0c 100644
--- a/tests/value/reading_null.i
+++ b/tests/value/reading_null.i
@@ -51,6 +51,6 @@ void main1(int c){
 
   int X1;
   int* X2;
-  X1 = X2;
+  X1 = (int) X2;
 
 }
diff --git a/tests/value/struct3.i b/tests/value/struct3.i
index 4df620d73074d93ae39de633c6784bab3137ce81..d3e0a39bac3f4ef44583c651347d2cac1097b65d 100644
--- a/tests/value/struct3.i
+++ b/tests/value/struct3.i
@@ -43,5 +43,5 @@ void main () {
 
   s2 = s1; // Creates a garbled mix internally; make sure not to log it
 
-  s2.a = s2.c + (int) s2.c; // creates a garbled mix in the struct
+  s2.a = (int) (s2.c + (int) s2.c); // creates a garbled mix in the struct
 }
diff --git a/tests/value/struct_array.i b/tests/value/struct_array.i
index 98af64f4a99d7937e84a277363da7c25a07da2e5..cfe0e9ab48851779b00a9a9d50ac6d8f47cab6b8 100644
--- a/tests/value/struct_array.i
+++ b/tests/value/struct_array.i
@@ -12,7 +12,7 @@ struct st1 {
 };
 int *outp;
 int x,y,z1,z2,z3,z4;
-struct st1 T[22] = { {1,2,0,&x}, {&z1,&z2,&z3,&y},{&z4,2,0,&x},{1,2,0,&x} };
+struct st1 T[22] = { {1,2,0,&x}, {(int)&z1,(int)&z2,&z3,&y},{(int)&z4,2,0,&x},{1,2,0,&x} };
 
 struct S {
   int a;
diff --git a/tests/value/struct_incl.i b/tests/value/struct_incl.i
index b21e07739aa598c1e2d8c7afd31643f3e5c56732..9fdf1d88821b51cd49281a6d7552bee4b2a37e90 100644
--- a/tests/value/struct_incl.i
+++ b/tests/value/struct_incl.i
@@ -25,9 +25,9 @@ struct st1 s8,s7;
 long x,y,z,t; volatile int v;
 
 void main () {
-  x = &s1.d[9];
-  y = &s1.d[10];
-  z = &s1.b;
+  x = (long) &s1.d[9];
+  y = (long) &s1.d[10];
+  z = (long) &s1.b;
 
 
   
diff --git a/tests/value/symbolic_locs.i b/tests/value/symbolic_locs.i
index 63172f4ea02ffb574d2b42d67d78a2b02c296b30..2ac419472e47bc79b7ccb1cb51bb5d4eec380569 100644
--- a/tests/value/symbolic_locs.i
+++ b/tests/value/symbolic_locs.i
@@ -51,7 +51,7 @@ void main4_scope_right() {
   unsigned int i = v;  //@ assert i <= 8;
   {
     int x;
-    t[i] = &x;
+    t[i] = (int) &x;
     Frama_C_dump_each();
   }
   Frama_C_dump_each(); // Should be empty, x out-of-scope
diff --git a/tests/value/volatile.c b/tests/value/volatile.c
index 39f7ee77336db634a1212db1de85245e8f9f8ea0..300df2f38b8c9773912b1a704090706eea65a039 100644
--- a/tests/value/volatile.c
+++ b/tests/value/volatile.c
@@ -80,7 +80,7 @@ int * volatile main2() {
   int * volatile p1, * volatile p2, * volatile p3;
   p1 = G ? 0 : &X;
   p2 = &X;
-  k = G ? 0 : &X;
+  k = G ? 0 : (int) &X;
   p3 = k;
   return k;
 }
diff --git a/tests/value/volatilestruct.c b/tests/value/volatilestruct.c
index bb84b75e8bb34cbc7bdba41dedb70fd52ea17eb2..3eadd6f1d021d77813b2583fb992264039f8d6f7 100644
--- a/tests/value/volatilestruct.c
+++ b/tests/value/volatilestruct.c
@@ -28,7 +28,7 @@ void main() {
   char *q1 = p->f4.f1;
   int *q2 = p->f4.f2;
   int i = p->f5;
-  int j = p->f4.f2;
+  int j = (int) p->f4.f2;
 
   int r = (&x - p->f4.f1)+1;
   int s = (&y - p->f4.f2)+3;