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 c1d9032cb645ecaacc70d4f1af007be95b72369d..0b02e09b98b4a40aafb0895b7524d3459d38496c 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 5971cd977e189cd4aeeb7a9dbdc05b7bcca6432f..046a6a7f967f4de51161c85675714c523fe96060 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 691e6c40c96abdd8f892a4ee9a5730b1311440a1..99a62eef221249385b08dee71e0d519b78fc0716 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 f07006ab7b9f349145414cf225baf363499be4b9..4b2242866946650c5afa1b2f4093f6c918b70c82 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 16132535368f9e2ddd498ef8720a79f326f43c42..daaa64cf446c6daed768612578c53b74ef169f47 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.