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 f102d73fa2acd8532fc8b3156a5b88d60a33e687..6c86a931f4cfdda1b19f4afaca6b6c70672c1d53 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 @@ -6,3 +6,4 @@ tests/runtime/block_valid.c:45:[value] warning: out of bounds write. assert \val tests/runtime/block_valid.c:46:[value] warning: out of bounds write. assert \valid(pmax); tests/runtime/block_valid.c:52:[value] warning: assertion got status unknown. tests/runtime/block_valid.c:54:[value] warning: assertion got status unknown. +[scope:rm_asserts] removing 2 assertion(s) diff --git a/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle index 27ca710aa080df7cf20e1d13f4e794d8f7f26724..e510a97a7e3e36ae2891f34fec54907783f7fd4b 100644 --- a/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle +++ b/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle @@ -32,3 +32,4 @@ tests/runtime/early_exit.c:117:[value] warning: accessing uninitialized left-val tests/runtime/early_exit.c:117:[value] warning: accessing left-value that contains escaping addresses. assert ¬\dangling(&q); tests/runtime/early_exit.c:99:[value] warning: locals {a0} escaping the scope of a block of while_valid through r +[scope:rm_asserts] removing 5 assertion(s) diff --git a/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle index 442101a5faaeba86557e6a5311d5a0cb708794c6..81b19d24dfee87eacbc3245e8da749a724dcfccc 100644 --- a/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle +++ b/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle @@ -14,3 +14,4 @@ tests/runtime/initialized.c:94:[value] warning: assertion got status unknown. tests/runtime/initialized.c:97:[value] warning: assertion got status unknown. tests/runtime/initialized.c:108:[value] warning: out of bounds write. assert \valid(partsi + i); tests/runtime/initialized.c:106:[value] warning: out of bounds write. assert \valid(partsc + i); +[scope:rm_asserts] removing 6 assertion(s) diff --git a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle index e3f9a03de82668f9c4ab780cdf0690e909146dcb..3204922bbb24f35d78484a73e324057184c38512 100644 --- a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle +++ b/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle @@ -22,3 +22,4 @@ FRAMAC_SHARE/libc/string.h:92:[value] warning: builtin Frama_C_strlen: possibly FRAMAC_SHARE/libc/string.h:94:[value] warning: function __gen_e_acsl_strlen: postcondition got status unknown. tests/runtime/mainargs.c:19:[value] warning: assertion got status unknown. tests/runtime/mainargs.c:20:[value] warning: assertion got status unknown. +[scope:rm_asserts] removing 1 assertion(s) diff --git a/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle index 4ba26f48cd6e370693ebb279c4e044607f5cbfb5..a0fd973000e791bef7fa1e8e4a0135cfc9bee504 100644 --- a/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle +++ b/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle @@ -3,3 +3,4 @@ tests/runtime/memalign.c:12:[kernel] warning: Neither code nor specification for function posix_memalign, generating default assigns from the prototype tests/runtime/memalign.c:14:[value] warning: accessing uninitialized left-value. assert \initialized(memptr); tests/runtime/memalign.c:14:[value] warning: out of bounds read. assert \valid_read(memptr); +[scope:rm_asserts] removing 2 assertion(s) diff --git a/src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle index 5f44363c23a158807043b12cfe276957d9661dd8..9fcbf305776edba4848243305184823c3f1a9b44 100644 --- a/src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle +++ b/src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle @@ -2,3 +2,4 @@ [e-acsl] translation done in project "e-acsl". tests/runtime/memsize.c:14:[value] warning: assertion got status unknown. tests/runtime/memsize.c:16:[value] warning: assertion got status invalid (stopping propagation). +[scope:rm_asserts] removing 6 assertion(s) diff --git a/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle index 38fd6f94cd3490e258dee1784f1fd3a64975ec72..a6402415ce9f4fdcd43b937e31100ba95336739e 100644 --- a/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle +++ b/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle @@ -3,3 +3,4 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown. tests/runtime/vector.c:26:[value] warning: accessing uninitialized left-value. assert \initialized(v2 + 2); tests/runtime/vector.c:28:[value] warning: assertion got status unknown. +[scope:rm_asserts] removing 1 assertion(s)