diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle index 866775deb449cbdd83ea9ad4507f0b1ff45923a9..f00de121ac82a98f0e3af977e2920a5e8165fde9 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle +++ b/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 diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle index c7ca85958eaa12f1ab7e8d2075e03b2f7d6bea4d..b40011aa16f07458cf45dcdd3f32e8dfdd3cb8d2 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle +++ b/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 diff --git a/src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle index 40117d300f16d19e44fd30248488e295cc8763c0..f823c92a099a5cfe847912d04c2991eb2fe24bbf 100644 --- a/src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle +++ b/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. diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c index 919d94500618e8194d65885ea58a19b36a93f6e4..c855442f720f74e4ed0491ed9aab2c4745491103 100644 --- a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c +++ b/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); diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c index fb6536a08a67d37f2d59309375d6f26fffd0c887..c212a2c38bb7b613b64dfdd4e3fc16884d09291e 100644 --- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c +++ b/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;