Merge branch 'feature/eva/pointer-comparable' into 'master'

sync with frama-c/frama-c!1644

See merge request frama-c/e-acsl!190

src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle

@@ -32,7 +32,5 @@ tests/gmp/longlong.i:17:[value] warning: function __e_acsl_assert: precondition
 [value] using specification for function __gmpz_get_si
 tests/gmp/longlong.i:17:[value] Assigning imprecise value to __gen_e_acsl__4.
     The imprecision originates from Library function
-tests/gmp/longlong.i:17:[value] warning: pointer comparison.
-    assert \pointer_comparable((void *)__gen_e_acsl__4, (void *)1);
 [value] using specification for function __gmpz_clear
 [value] done for function main

src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle

@@ -31,7 +31,5 @@ tests/gmp/longlong.i:17:[value] warning: function __e_acsl_assert: precondition
 [value] using specification for function __gmpz_tdiv_r
 tests/gmp/longlong.i:17:[value] Assigning imprecise value to __gen_e_acsl_eq.
     The imprecision originates from Library function
-tests/gmp/longlong.i:17:[value] warning: pointer comparison.
-    assert \pointer_comparable((void *)__gen_e_acsl_eq, (void *)0);
 [value] using specification for function __gmpz_clear
 [value] done for function main

src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle

@@ -4,7 +4,6 @@ tests/runtime/block_valid.c:24:[value] warning: function __e_acsl_assert: precon
 tests/runtime/block_valid.c:26:[value] warning: function __e_acsl_assert: precondition got status unknown.
 tests/runtime/block_valid.c:29:[value] warning: function __e_acsl_assert: precondition got status unknown.
 tests/runtime/block_valid.c:31:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/runtime/block_valid.c:39:[value] warning: pointer comparison. assert \pointer_comparable((void *)pmin, (void *)pmax);
 tests/runtime/block_valid.c:45:[value] warning: out of bounds write. assert \valid(pmin);
 tests/runtime/block_valid.c:46:[value] warning: out of bounds write. assert \valid(pmax);
 tests/runtime/block_valid.c:49:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c

@@ -82,9 +82,6 @@ int main(int argc, char **argv)
   char *pmax = malloc(sizeof(int));
   __e_acsl_store_block((void *)(& pmax),(size_t)8);
   __e_acsl_full_init((void *)(& pmax));
-  /*@ assert
-      Value: ptr_comparison: \pointer_comparable((void *)pmin, (void *)pmax);
-  */
   if ((unsigned long)pmin > (unsigned long)pmax) {
     char *t = pmin;
     __e_acsl_store_block((void *)(& t),(size_t)8);

src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c

@@ -9,12 +9,6 @@ int main(void)
   __e_acsl_store_block((void *)(arr),(size_t)16);
   __e_acsl_full_init((void *)(& arr));
   int arr2[4] = {1, 2, 3, 4};
-  /*@ assert
-      Value: ptr_comparison:
-        \pointer_comparable((void *)((unsigned long)((unsigned long)(&arr) +
-                                                     sizeof(arr))),
-                           (void *)(&arr2));
-  */
   if (! ((unsigned long)(& arr) + sizeof(arr) == (unsigned long)(& arr2))) {
     __retres = 0;
     goto return_label;