diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-166.i b/src/plugins/e-acsl/tests/bts/issue-eacsl-166.i new file mode 100644 index 0000000000000000000000000000000000000000..94f943aee103cc71ebda6afc97a1261da87a2e5d --- /dev/null +++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-166.i @@ -0,0 +1,23 @@ +/* run.config + COMMENT: Change order of options to run Eva before E-ACSL so that the ensures + COMMENT: clause is proven invalid before running E-ACSL. Eva will prove the + COMMENT: ensures invalid under hypotheses of reachability, this test shows + COMMENT: that when we duplicate the invalid property statuses, we remove the + COMMENT: hypotheses to satisfy kernel invariants. + OPT: @GLOBAL@ @EVA@ -then @EACSL@ -then-last @EVENTUALLY@ +*/ +/* run.config_dev + COMMENT: No need to compile and execute the test since we know the property + COMMENT: will be invalid. + DONTRUN: +*/ + +/*@ ensures \result == 1; */ +int f() { + return 0; +} + +int main() { + f(); + return 0; +} diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-166.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-166.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..efd60b0c45111cc5fd9ae4a646b2e53e109bb55c --- /dev/null +++ b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-166.res.oracle @@ -0,0 +1,6 @@ +[eva:alarm] tests/bts/issue-eacsl-166.i:15: Warning: + function f: postcondition got status invalid. +[e-acsl] beginning translation. +[e-acsl] translation done in project "e-acsl". +[eva:alarm] tests/bts/issue-eacsl-166.i:15: Warning: + function __e_acsl_assert, behavior blocking: precondition got status invalid.