Commit 09031f36 authored by Andre Maroneze's avatar Andre Maroneze Committed by David Bühler
Browse files

sync with frama-c/frama-c!1618

parent 37881680
/* run.config
STDOPT: +"-no-val-builtins-auto"
STDOPT:
COMMENT: Behaviours of the \initialized E-ACSL predicate
*/
......
......@@ -18,16 +18,17 @@ tests/runtime/initialized.c:66:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:66:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/initialized.c:70:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:70:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/initialized.c:74:[value] warning: function realloc: precondition got status unknown.
tests/runtime/initialized.c:75:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:75:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/initialized.c:77:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:77:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/initialized.c:83:[value] warning: function free: precondition 'freeable' got status unknown.
tests/runtime/initialized.c:84:[value] warning: function free: precondition 'freeable' got status unknown.
tests/runtime/initialized.c:85:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:85:[value] warning: accessing left-value that contains escaping addresses.
assert ¬\dangling(&p);
tests/runtime/initialized.c:85:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/initialized.c:86:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:86:[value] warning: accessing left-value that contains escaping addresses.
assert ¬\dangling(&q);
tests/runtime/initialized.c:86:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/initialized.c:94:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
......@@ -35,4 +36,4 @@ tests/runtime/initialized.c:97:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:97:[value] warning: function __e_acsl_assert: precondition 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)
[scope:rm_asserts] removing 5 assertion(s)
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment