Skip to content
Snippets Groups Projects
Commit 88562986 authored by Felix Ridoux's avatar Felix Ridoux
Browse files

[e-acsl] rebasing, conflicts resolving and oracles updating

parent 259f404f
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 10 additions and 16 deletions
src/plugins/e-acsl/tests/builtin/oracle_ci/strcat.res.oracle
+ 0
− 4
View file @ 88562986
...@@ -25,7 +25,3 @@ ...@@ -25,7 +25,3 @@
is not yet supported. is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[eva:alarm] FRAMAC_SHARE/libc/unistd.h:860: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/unistd.h:860: Warning:
function __gen_e_acsl_fork: postcondition 'result_ok_child_or_error' got status unknown.
src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle
+ 0
− 4
View file @ 88562986
...@@ -41,9 +41,5 @@ ...@@ -41,9 +41,5 @@
is not yet supported. is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[eva:alarm] FRAMAC_SHARE/libc/unistd.h:860: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/unistd.h:860: Warning:
function __gen_e_acsl_fork: postcondition 'result_ok_child_or_error' got status unknown.
[kernel:annot:missing-spec] tests/format/fprintf.c:15: Warning: [kernel:annot:missing-spec] tests/format/fprintf.c:15: Warning:
Neither code nor specification for function __e_acsl_builtin_fprintf, generating default assigns from the prototype Neither code nor specification for function __e_acsl_builtin_fprintf, generating default assigns from the prototype
src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle
+ 0
− 4
View file @ 88562986
...@@ -104,9 +104,5 @@ ...@@ -104,9 +104,5 @@
is not yet supported. is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[eva:alarm] FRAMAC_SHARE/libc/unistd.h:860: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/unistd.h:860: Warning:
function __gen_e_acsl_fork: postcondition 'result_ok_child_or_error' got status unknown.
[kernel:annot:missing-spec] tests/format/printf.c:180: Warning: [kernel:annot:missing-spec] tests/format/printf.c:180: Warning:
Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype
src/plugins/e-acsl/tests/memory/oracle_ci/separated.res.oracle
+ 7
− 1
View file @ 88562986
...@@ -35,11 +35,17 @@ ...@@ -35,11 +35,17 @@
[eva:alarm] tests/memory/separated.c:51: Warning: [eva:alarm] tests/memory/separated.c:51: Warning:
function __e_acsl_assert, behavior blocking: precondition got status invalid. function __e_acsl_assert, behavior blocking: precondition got status invalid.
[eva:alarm] tests/memory/separated.c:52: Warning: [eva:alarm] tests/memory/separated.c:52: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown. function __e_acsl_assert, behavior blocking: precondition got status invalid.
[eva:alarm] tests/memory/separated.c:60: Warning:
function __e_acsl_assert, behavior blocking: precondition got status invalid.
[eva:alarm] tests/memory/separated.c:60: Warning: [eva:alarm] tests/memory/separated.c:60: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown. function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/memory/separated.c:61: Warning:
function __e_acsl_assert, behavior blocking: precondition got status invalid.
[eva:alarm] tests/memory/separated.c:61: Warning: [eva:alarm] tests/memory/separated.c:61: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown. function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/memory/separated.c:62: Warning:
function __e_acsl_assert, behavior blocking: precondition got status invalid.
[eva:alarm] tests/memory/separated.c:62: Warning: [eva:alarm] tests/memory/separated.c:62: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown. function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/memory/separated.c:62: Warning: assertion got status unknown. [eva:alarm] tests/memory/separated.c:62: Warning: assertion got status unknown.
......
src/plugins/e-acsl/tests/temporal/oracle_ci/t_getenv.res.oracle
+ 3
− 3
View file @ 88562986
...@@ -10,12 +10,12 @@ ...@@ -10,12 +10,12 @@
Ignoring annotation. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:488: Warning: [eva:alarm] FRAMAC_SHARE/libc/stdlib.h:488: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown. function __e_acsl_assert, behavior blocking: precondition got status invalid.
[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:488: Warning: [eva:alarm] FRAMAC_SHARE/libc/stdlib.h:488: Warning:
function __gen_e_acsl_getenv: postcondition 'null_or_valid_result' got status unknown. function __gen_e_acsl_getenv: postcondition 'null_or_valid_result' got status unknown.
[eva:alarm] tests/temporal/t_getenv.c:14: Warning: [eva:alarm] tests/temporal/t_getenv.c:14: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown. function __e_acsl_assert, behavior blocking: precondition got status invalid.
[eva:alarm] tests/temporal/t_getenv.c:14: Warning: assertion got status unknown. [eva:alarm] tests/temporal/t_getenv.c:14: Warning: assertion got status unknown.
[eva:alarm] tests/temporal/t_getenv.c:15: Warning: [eva:alarm] tests/temporal/t_getenv.c:15: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown. function __e_acsl_assert, behavior blocking: precondition got status invalid.
[eva:alarm] tests/temporal/t_getenv.c:15: Warning: assertion got status unknown. [eva:alarm] tests/temporal/t_getenv.c:15: Warning: assertion got status unknown.
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