Skip to content
Snippets Groups Projects
Commit 4e848baf authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

update oracles wrt kernel changes

parent f6d069d4
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
+ 3
− 3
View file @ 4e848baf
...@@ -3,11 +3,11 @@ ...@@ -3,11 +3,11 @@
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown. FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/initialized.c:66:[value] warning: assertion got status unknown. tests/runtime/initialized.c:66:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:70:[value] warning: assertion got status unknown. tests/runtime/initialized.c:70:[value] warning: assertion got status unknown.
FRAMAC_SHARE/libc/stdlib.h:348:[value] warning: function realloc: precondition got status unknown. FRAMAC_SHARE/libc/stdlib.h:358:[value] warning: function realloc: precondition got status unknown.
FRAMAC_SHARE/libc/stdlib.h:363:[value] warning: function realloc, behavior dealloc: precondition got status unknown. FRAMAC_SHARE/libc/stdlib.h:373:[value] warning: function realloc, behavior dealloc: precondition got status unknown.
tests/runtime/initialized.c:75:[value] warning: assertion got status unknown. tests/runtime/initialized.c:75:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:77:[value] warning: assertion got status unknown. tests/runtime/initialized.c:77:[value] warning: assertion got status unknown.
FRAMAC_SHARE/libc/stdlib.h:335:[value] warning: function free, behavior deallocation: precondition 'freeable' got status unknown. FRAMAC_SHARE/libc/stdlib.h:345:[value] warning: function free, behavior deallocation: precondition 'freeable' got status unknown.
tests/runtime/initialized.c:85:[value] warning: assertion got status unknown. tests/runtime/initialized.c:85:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:86:[value] warning: assertion got status unknown. tests/runtime/initialized.c:86:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:94:[value] warning: assertion got status unknown. tests/runtime/initialized.c:94:[value] warning: assertion got status unknown.
......
src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
+ 1
− 1
View file @ 4e848baf
...@@ -2,6 +2,6 @@ ...@@ -2,6 +2,6 @@
[e-acsl] warning: annotating undefined function `getenv': [e-acsl] warning: annotating undefined function `getenv':
the generated program may miss memory instrumentation the generated program may miss memory instrumentation
if there are memory-related annotations. if there are memory-related annotations.
FRAMAC_SHARE/libc/stdlib.h:407:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:417:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
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