[tests] partial update

tests/libc/oracle/fc_libc.1.res.oracle

@@ -4783,7 +4783,7 @@ int unsetenv(char const *name)
     requires
       alignment_is_a_suitable_power_of_two:
         alignment ≥ sizeof(void *) ∧
-        ((unsigned int)alignment & ((unsigned int)alignment - 1)) ≡ 0;
+        ((size_t)alignment & ((size_t)alignment - 1)) ≡ 0;
     assigns __fc_heap_status, \result;
     assigns __fc_heap_status
       \from (indirect: alignment), size, __fc_heap_status;
@@ -4820,7 +4820,7 @@ int posix_memalign(void **memptr, size_t alignment, size_t size)
   assert
   alignment_is_a_suitable_power_of_two:
     alignment ≥ sizeof(void *) ∧
-    ((unsigned int)alignment & ((unsigned int)alignment - 1)) ≡ 0;
+    ((size_t)alignment & ((size_t)alignment - 1)) ≡ 0;
    */
   ;
   *memptr = malloc(size);

tests/misc/oracle/obfuscate.res.oracle

@@ -123,7 +123,7 @@ int F3(int f2)
   V3 = 0;
   if (f2) goto L2;
   V3 ++;
-  /*@ assert property: V3 ≢ 0? 1 ≢ 0: 0 ≢ 0; */ ;
+  /*@ assert property: V3? 1 ≢ 0: 0 ≢ 0; */ ;
   L2: ;
   return V3;
 }

tests/spec/oracle/all.res.oracle

@@ -29,7 +29,7 @@ axiomatic Test {
   
   axiom e: P ⊻ Q;
   
-  axiom f: 0 ≢ 0? P: Q;
+  axiom f: 0? P: Q;
   
   axiom g: (P ⇒ P) ∧ (¬P ⇒ Q);
   
@@ -39,13 +39,13 @@ axiomatic Test {
   
   }
  */
-/*@ predicate R(ℤ i, ℤ j) = (1 ≢ 0? i + j: (j: j)) ≡ i + j;
+/*@ predicate R(ℤ i, ℤ j) = (1? i + j: (j: j)) ≡ i + j;
  */
-/*@ predicate S(ℤ i, ℤ j) = (1 ≢ 0? (i: j): j) ≡ j;
+/*@ predicate S(ℤ i, ℤ j) = (1? (i: j): j) ≡ j;
  */
-/*@ predicate T(ℤ i, ℤ j) = (1 ≢ 0? i: j) ≡ i;
+/*@ predicate T(ℤ i, ℤ j) = (1? i: j) ≡ i;
  */
-/*@ lemma tauto: 0 ≢ 0? T(0, 0): R(1, 2);
+/*@ lemma tauto: 0? T(0, 0): R(1, 2);
  */
 /*@ lemma tauto2: (R(0, 1) ⇒ S(3, 4)) ∧ (¬R(0, 1) ⇒ T(5, 6));
  */

tests/spec/oracle/null_ptr.res.oracle

@@ -22,7 +22,7 @@ void f(char *x)
   return;
 }
 
-/*@ ensures (\result ≢ 0) ≡ \true; */
+/*@ ensures \result ≡ \true; */
 int g(void)
 {
   int __retres;

tests/spec/oracle/parsing.res.oracle

@@ -7,9 +7,9 @@
 /* Generated by Frama-C */
 /*@ lemma bidon{Here}: ∀ int *t; ¬(*(t + 0) > 0);
  */
-/*@ lemma bidon1{Here}: ∀ int *t; !(*(t + 0) ≢ 0) ≡ (0 ≢ 0);
+/*@ lemma bidon1{Here}: ∀ int *t; !*(t + 0) ≡ 0;
  */
-/*@ lemma bidon2{Here}: ∀ int *t; !(*(t + 0) ≢ 0) ≡ (0 ≢ 0);
+/*@ lemma bidon2{Here}: ∀ int *t; !*(t + 0) ≡ 0;
  */
 /*@
 predicate foo{L}(int *a, int *b, int length) =

tests/spec/oracle/real_typing_bts1309.res.oracle

@@ -3,7 +3,7 @@
 void foo(int c)
 {
   float f = (float)1.0;
-  /*@ assert 0.0 ≤ (c ≢ 0? f: 2.0); */ ;
+  /*@ assert 0.0 ≤ (c? f: 2.0); */ ;
   return;
 }
 

tests/syntax/oracle/static_formals_1.res.oracle

@@ -2,23 +2,23 @@
 [kernel] Parsing tests/syntax/static_formals_2.c (with preprocessing)
 /* Generated by Frama-C */
 /*@ requires /* vid:23, lvid:23 */x < 10; */
-static int /* vid:52 */f(int /* vid:23, lvid:23 */x);
+static int /* vid:54 */f(int /* vid:23, lvid:23 */x);
 
-int /* vid:26 */g(void)
+int /* vid:28 */g(void)
 {
-  int /* vid:27 */tmp;
-  /* vid:27 */tmp = /* vid:52 */f(4);
-  return /* vid:27 */tmp;
+  int /* vid:29 */tmp;
+  /* vid:29 */tmp = /* vid:54 */f(4);
+  return /* vid:29 */tmp;
 }
 
-/*@ requires /* vid:47, lvid:47 */x < 10; */
-static int /* vid:53 */f_0(int /* vid:47, lvid:47 */x);
+/*@ requires /* vid:49, lvid:49 */x < 10; */
+static int /* vid:55 */f_0(int /* vid:49, lvid:49 */x);
 
-int /* vid:50 */h(void)
+int /* vid:52 */h(void)
 {
-  int /* vid:51 */tmp;
-  /* vid:51 */tmp = /* vid:53 */f_0(6);
-  return /* vid:51 */tmp;
+  int /* vid:53 */tmp;
+  /* vid:53 */tmp = /* vid:55 */f_0(6);
+  return /* vid:53 */tmp;
 }