Skip to content
Snippets Groups Projects
Commit b0d6a40b authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl] Add test for issue e-acsl#166

parent e762f5a6
No related branches found
No related tags found
No related merge requests found
/* 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;
}
[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.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment