loop invariant cannot conclude (due to an assertion)
ID0001172: This issue was created automatically from Mantis Issue 1172. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001172 | Frama-C | Kernel > ACSL implementation | public | 2012-04-23 | 2012-04-23 |
| Reporter | nmuller | Assigned To | virgile | Resolution | no change required |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | - |
Description :
<<< abs_new_1.c >>> The previous verison, "abs_new.c" code had some minor problems with the annotations, that it was not able to validate two assertions, when used using Jessie, but the code was changed and analysed using "WP", we found out that we again had some problems, this time it was only one assertion in the last part of the program at "line:59", which was not getting validated, rest of the other assertions of the same type were getting validated in the previous loops, so we inserted a "loop invariant for the same assertion" without removing the existing unknown assertion and we tried to prove it by Wp , interestingly this time the assertion was validated but the loop invariant corresponding to the assertion was "time out" (although the time out has been increased up to 200).
Quite interesting indeed, as we are not that strong in the underlying theory of the WP analyser, but to our understanding on looking on to the prolem,we feel that the an assertion for any line of C code inside a loop should be declared as a loop invariant, so that it goes around like in a circle, first it validates the assertion and comes back to the loop invariant in order to be valid, but in our case the once the assertion is valid, its not able to retrace back to the loop invariant to validate it, and so the loop invariant becomes "time out".