Translation of abrupt clause into assert do not take 'for :' clause into account
ID0001632: This issue was created automatically from Mantis Issue 1632. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001632 | Frama-C | Kernel > ACSL implementation | public | 2014-01-27 | 2014-10-29 |
| Reporter | virgile | Assigned To | virgile | Resolution | open |
| Priority | low | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | - |
Description :
In the program written given below, the returns clause is translated into two assert that are not related to the foo behavior, resulting in an unprovable assertion in the else branch.
Steps To Reproduce :
/*@ behavior foo: assumes a == 0; / int foo(int a) { /@ for foo: returns \result == 0; */ { if (a==0) { return 0; } else return 2; } }