Skip to content
Snippets Groups Projects
Commit ef3641da authored by Boris Yakobowski's avatar Boris Yakobowski
Browse files

Adapt to trunk branch feature/eva/remove-redundant-alarms-default

parent 2ac4afb3
No related branches found
No related tags found
No related merge requests found
...@@ -6,3 +6,4 @@ tests/runtime/block_valid.c:45:[value] warning: out of bounds write. assert \val ...@@ -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: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:52:[value] warning: assertion got status unknown.
tests/runtime/block_valid.c:54:[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)
...@@ -32,3 +32,4 @@ tests/runtime/early_exit.c:117:[value] warning: accessing uninitialized left-val ...@@ -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. tests/runtime/early_exit.c:117:[value] warning: accessing left-value that contains escaping addresses.
assert ¬\dangling(&q); assert ¬\dangling(&q);
tests/runtime/early_exit.c:99:[value] warning: locals {a0} escaping the scope of a block of while_valid through r 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)
...@@ -14,3 +14,4 @@ tests/runtime/initialized.c:94:[value] warning: assertion got status unknown. ...@@ -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: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: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); tests/runtime/initialized.c:106:[value] warning: out of bounds write. assert \valid(partsc + i);
[scope:rm_asserts] removing 6 assertion(s)
...@@ -22,3 +22,4 @@ FRAMAC_SHARE/libc/string.h:92:[value] warning: builtin Frama_C_strlen: possibly ...@@ -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. 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:19:[value] warning: assertion got status unknown.
tests/runtime/mainargs.c:20:[value] warning: assertion got status unknown. tests/runtime/mainargs.c:20:[value] warning: assertion got status unknown.
[scope:rm_asserts] removing 1 assertion(s)
...@@ -3,3 +3,4 @@ ...@@ -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: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: accessing uninitialized left-value. assert \initialized(memptr);
tests/runtime/memalign.c:14:[value] warning: out of bounds read. assert \valid_read(memptr); tests/runtime/memalign.c:14:[value] warning: out of bounds read. assert \valid_read(memptr);
[scope:rm_asserts] removing 2 assertion(s)
...@@ -2,3 +2,4 @@ ...@@ -2,3 +2,4 @@
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
tests/runtime/memsize.c:14:[value] warning: assertion got status unknown. tests/runtime/memsize.c:14:[value] warning: assertion got status unknown.
tests/runtime/memsize.c:16:[value] warning: assertion got status invalid (stopping propagation). tests/runtime/memsize.c:16:[value] warning: assertion got status invalid (stopping propagation).
[scope:rm_asserts] removing 6 assertion(s)
...@@ -3,3 +3,4 @@ ...@@ -3,3 +3,4 @@
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown. 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:26:[value] warning: accessing uninitialized left-value. assert \initialized(v2 + 2);
tests/runtime/vector.c:28:[value] warning: assertion got status unknown. tests/runtime/vector.c:28:[value] warning: assertion got status unknown.
[scope:rm_asserts] removing 1 assertion(s)
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment