From 7b9f19012bd13bfd0699a2b9d7eb7aee9e891e4f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Tue, 28 Jan 2020 14:24:17 +0100 Subject: [PATCH] [Eva] Updates test oracles. --- .../oracle_ci/at_on-purely-logic-variables.res.oracle | 2 -- .../e-acsl/tests/arith/oracle_ci/quantif.res.oracle | 7 ------- .../tests/examples/oracle_ci/linear_search.res.oracle | 4 ++-- tests/libc/oracle/string_c.res.oracle | 7 +++++-- tests/value/oracle/forall.res.oracle | 2 +- 5 files changed, 8 insertions(+), 14 deletions(-) diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle index c1d9032cb64..0b02e09b98b 100644 --- a/src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle +++ b/src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle @@ -59,8 +59,6 @@ function __e_acsl_assert: precondition got status unknown. [eva:alarm] tests/arith/at_on-purely-logic-variables.c:7: Warning: function __e_acsl_assert: precondition got status unknown. -[eva:alarm] tests/arith/at_on-purely-logic-variables.c:6: Warning: - function __gen_e_acsl_f: postcondition got status unknown. [eva:alarm] tests/arith/at_on-purely-logic-variables.c:8: Warning: function __gen_e_acsl_f: postcondition got status unknown. [eva:alarm] tests/arith/at_on-purely-logic-variables.c:16: Warning: diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle index 5971cd977e1..046a6a7f967 100644 --- a/src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle +++ b/src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle @@ -1,8 +1,5 @@ [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". -[eva:alarm] tests/arith/quantif.i:9: Warning: assertion got status unknown. -[eva:alarm] tests/arith/quantif.i:10: Warning: assertion got status unknown. -[eva:alarm] tests/arith/quantif.i:11: Warning: assertion got status unknown. [eva:alarm] tests/arith/quantif.i:15: Warning: function __e_acsl_assert: precondition got status unknown. [eva:alarm] tests/arith/quantif.i:15: Warning: assertion got status unknown. @@ -12,14 +9,10 @@ [eva:alarm] tests/arith/quantif.i:24: Warning: assertion got status unknown. [eva:alarm] tests/arith/quantif.i:30: Warning: function __e_acsl_assert: precondition got status unknown. -[eva:alarm] tests/arith/quantif.i:30: Warning: assertion got status unknown. [eva:alarm] tests/arith/quantif.i:31: Warning: function __e_acsl_assert: precondition got status unknown. [eva:alarm] tests/arith/quantif.i:32: Warning: function __e_acsl_assert: precondition got status unknown. -[eva:alarm] tests/arith/quantif.i:32: Warning: assertion got status unknown. [eva:alarm] tests/arith/quantif.i:33: Warning: function __e_acsl_assert: precondition got status unknown. -[eva:alarm] tests/arith/quantif.i:33: Warning: assertion got status unknown. -[eva:alarm] tests/arith/quantif.i:37: Warning: assertion got status unknown. [eva:alarm] tests/arith/quantif.i:40: Warning: assertion got status unknown. diff --git a/src/plugins/e-acsl/tests/examples/oracle_ci/linear_search.res.oracle b/src/plugins/e-acsl/tests/examples/oracle_ci/linear_search.res.oracle index 691e6c40c96..99a62eef221 100644 --- a/src/plugins/e-acsl/tests/examples/oracle_ci/linear_search.res.oracle +++ b/src/plugins/e-acsl/tests/examples/oracle_ci/linear_search.res.oracle @@ -4,10 +4,10 @@ function __gen_e_acsl_search: precondition got status unknown. [eva:alarm] tests/examples/linear_search.i:7: Warning: function __e_acsl_assert: precondition got status unknown. -[eva:alarm] tests/examples/linear_search.i:18: Warning: - loop invariant got status unknown. [eva:alarm] tests/examples/linear_search.i:18: Warning: function __e_acsl_assert: precondition got status unknown. +[eva:alarm] tests/examples/linear_search.i:18: Warning: + loop invariant got status unknown. [eva:alarm] tests/examples/linear_search.i:10: Warning: function __e_acsl_assert: precondition got status unknown. [eva:alarm] tests/examples/linear_search.i:13: Warning: diff --git a/tests/libc/oracle/string_c.res.oracle b/tests/libc/oracle/string_c.res.oracle index f07006ab7b9..4b224286694 100644 --- a/tests/libc/oracle/string_c.res.oracle +++ b/tests/libc/oracle/string_c.res.oracle @@ -769,8 +769,9 @@ function memchr, behavior found: postcondition 'result_same_base' got status valid. (Behavior may be inactive, no reduction performed.) [eva] share/libc/string.h:80: function memchr, behavior found: postcondition 'result_char' got status valid. (Behavior may be inactive, no reduction performed.) -[eva:alarm] share/libc/string.h:81: Warning: - function memchr, behavior found: postcondition 'result_in_str' got status unknown. (Behavior may be inactive, no reduction performed.) +[kernel] share/libc/string.c:248: Warning: using size of 'void' +[eva] share/libc/string.h:81: + function memchr, behavior found: postcondition 'result_in_str' got status valid. (Behavior may be inactive, no reduction performed.) [eva:alarm] share/libc/string.h:86: Warning: function memchr, behavior not_found: postcondition 'result_null' got status invalid. (Behavior may be inactive, no reduction performed.) [eva] Recording results for memchr @@ -801,6 +802,8 @@ function memchr: precondition 'initialization' got status valid. [eva] tests/libc/string_c.c:231: function memchr: precondition 'danglingness' got status valid. +[eva:alarm] share/libc/string.h:81: Warning: + function memchr, behavior found: postcondition 'result_in_str' got status unknown. (Behavior may be inactive, no reduction performed.) [eva] Recording results for memchr [eva] Done for function memchr [eva] tests/libc/string_c.c:232: assertion got status valid. diff --git a/tests/value/oracle/forall.res.oracle b/tests/value/oracle/forall.res.oracle index 16132535368..daaa64cf446 100644 --- a/tests/value/oracle/forall.res.oracle +++ b/tests/value/oracle/forall.res.oracle @@ -8,7 +8,7 @@ [eva:alarm] tests/value/forall.i:9: Warning: function main: precondition got status unknown. [eva] tests/value/forall.i:11: assertion got status valid. -[eva:alarm] tests/value/forall.i:12: Warning: assertion got status unknown. +[eva] tests/value/forall.i:12: assertion got status valid. [eva] tests/value/forall.i:13: assertion got status valid. [eva:alarm] tests/value/forall.i:15: Warning: assertion got status unknown. [eva:alarm] tests/value/forall.i:16: Warning: assertion got status unknown. -- GitLab