[kernel] updated oracles wrt simplified casts

Only modifications introduced by non necessary casts elimination

tests/rte/oracle/addsub_unsigned.1.res.oracle

@@ -19,7 +19,7 @@ int main(void)
   uy = 0x80000000U + 0x80000000U;
   /*@ assert rte: unsigned_overflow: 2U * 0x80000000U ≤ 4294967295; */
   uy = 2U * 0x80000000U;
-  /*@ assert rte: unsigned_overflow: ux + (unsigned int)2 ≤ 4294967295; */
+  /*@ assert rte: unsigned_overflow: ux + 2 ≤ 4294967295; */
   uz = ux + (unsigned int)2;
   __retres = 0;
   return __retres;

tests/rte/oracle/addsub_unsigned_typedef.1.res.oracle

@@ -20,7 +20,7 @@ int main(void)
   uy = 0x80000000U + 0x80000000U;
   /*@ assert rte: unsigned_overflow: 2U * 0x80000000U ≤ 4294967295; */
   uy = 2U * 0x80000000U;
-  /*@ assert rte: unsigned_overflow: ux + (unsigned int)2 ≤ 4294967295; */
+  /*@ assert rte: unsigned_overflow: ux + 2 ≤ 4294967295; */
   uz = ux + (uint)2;
   __retres = 0;
   return __retres;

tests/rte_manual/oracle/unsigned.1.res.oracle

@@ -8,8 +8,8 @@ unsigned int f(unsigned int a, unsigned int b)
   unsigned int z;
   /*@ assert rte: unsigned_overflow: a << 3 ≤ 4294967295; */
   x = a << 3;
-  /*@ assert rte: unsigned_overflow: 0 ≤ b * (unsigned int)2; */
-  /*@ assert rte: unsigned_overflow: b * (unsigned int)2 ≤ 4294967295; */
+  /*@ assert rte: unsigned_overflow: 0 ≤ b * 2; */
+  /*@ assert rte: unsigned_overflow: b * 2 ≤ 4294967295; */
   y = b * (unsigned int)2;
   /*@ assert rte: unsigned_overflow: 0 ≤ x - y; */
   /*@ assert rte: unsigned_overflow: x - y ≤ 4294967295; */

tests/spec/oracle/null_ptr.res.oracle

@@ -10,12 +10,12 @@
  */
 /*@ predicate eq(char *x, char *y) = x ≡ y;
  */
-/*@ predicate my_null(char *x) = x ≡ (char *)((void *)0);
+/*@ predicate my_null(char *x) = x ≡ (char *)0;
  */
 void f(char *x)
 {
   x = (char *)0;
-  /*@ assert x ≡ (char *)((void *)0); */ ;
+  /*@ assert x ≡ (char *)0; */ ;
   /*@ assert my_null(x); */ ;
   /*@ assert null(x); */ ;
   /*@ assert eq(x, (char *)0); */ ;

tests/value/oracle/downcast.0.res.oracle

@@ -28,9 +28,9 @@
 [eva] computing for function main4_pointer <- main.
   Called from tests/value/downcast.i:159.
 [eva:alarm] tests/value/downcast.i:54: Warning: 
-  signed overflow. assert -9223372036854775808 ≤ p + (long long)100;
+  signed overflow. assert -9223372036854775808 ≤ p + 100;
 [eva:alarm] tests/value/downcast.i:54: Warning: 
-  signed overflow. assert p + (long long)100 ≤ 9223372036854775807;
+  signed overflow. assert p + 100 ≤ 9223372036854775807;
 [eva] Recording results for main4_pointer
 [eva] Done for function main4_pointer
 [eva] computing for function main5_wrap_signed <- main.

tests/value/oracle/downcast.1.res.oracle

@@ -40,9 +40,9 @@
 [eva] computing for function main4_pointer <- main.
   Called from tests/value/downcast.i:159.
 [eva:alarm] tests/value/downcast.i:54: Warning: 
-  signed overflow. assert -9223372036854775808 ≤ p + (long long)100;
+  signed overflow. assert -9223372036854775808 ≤ p + 100;
 [eva:alarm] tests/value/downcast.i:54: Warning: 
-  signed overflow. assert p + (long long)100 ≤ 9223372036854775807;
+  signed overflow. assert p + 100 ≤ 9223372036854775807;
 [eva:alarm] tests/value/downcast.i:56: Warning: 
   signed downcast. assert -2147483648 ≤ p;
 [eva:alarm] tests/value/downcast.i:56: Warning: 

tests/value/oracle/downcast.2.res.oracle

@@ -42,9 +42,9 @@
 [eva] computing for function main4_pointer <- main.
   Called from tests/value/downcast.i:159.
 [eva:alarm] tests/value/downcast.i:54: Warning: 
-  signed overflow. assert -9223372036854775808 ≤ p + (long long)100;
+  signed overflow. assert -9223372036854775808 ≤ p + 100;
 [eva:alarm] tests/value/downcast.i:54: Warning: 
-  signed overflow. assert p + (long long)100 ≤ 9223372036854775807;
+  signed overflow. assert p + 100 ≤ 9223372036854775807;
 [eva:alarm] tests/value/downcast.i:55: Warning: 
   unsigned downcast. assert 0 ≤ p;
 [eva:alarm] tests/value/downcast.i:55: Warning: 

tests/value/oracle/downcast.3.res.oracle

@@ -38,9 +38,9 @@
 [eva] computing for function main4_pointer <- main.
   Called from tests/value/downcast.i:159.
 [eva:alarm] tests/value/downcast.i:54: Warning: 
-  signed overflow. assert -9223372036854775808 ≤ p + (long long)100;
+  signed overflow. assert -9223372036854775808 ≤ p + 100;
 [eva:alarm] tests/value/downcast.i:54: Warning: 
-  signed overflow. assert p + (long long)100 ≤ 9223372036854775807;
+  signed overflow. assert p + 100 ≤ 9223372036854775807;
 [eva:alarm] tests/value/downcast.i:56: Warning: 
   signed downcast. assert -2147483648 ≤ p;
 [eva:alarm] tests/value/downcast.i:56: Warning: 

tests/value/oracle/downcast.4.res.oracle

@@ -28,9 +28,9 @@
 [eva] computing for function main4_pointer <- main.
   Called from tests/value/downcast.i:159.
 [eva:alarm] tests/value/downcast.i:54: Warning: 
-  signed overflow. assert -9223372036854775808 ≤ p + (long long)100;
+  signed overflow. assert -9223372036854775808 ≤ p + 100;
 [eva:alarm] tests/value/downcast.i:54: Warning: 
-  signed overflow. assert p + (long long)100 ≤ 9223372036854775807;
+  signed overflow. assert p + 100 ≤ 9223372036854775807;
 [eva] Recording results for main4_pointer
 [eva] Done for function main4_pointer
 [eva] computing for function main5_wrap_signed <- main.