Jessie: infinite or not annotated loops
ID0000103: This issue was created automatically from Mantis Issue 103. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000103 | Frama-C | Plug-in > jessie | public | 2009-05-27 | 2009-12-03 |
| Reporter | dpariente | Assigned To | cmarche | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | - |
Description :
(This issue was previously discussed through private messages but not fully resolved. It is now recorded into the BTS for traceability reasons.)
As all POs generated by Jessie/Why from the following annotated code are automatically discharged by ATPs, one might conclude that ensures clause is also validated! Which is not the case, of course!
Source code:
//@ requires \valid(p); assigns *p; ensures p==4; void g(intp){ int i=0; while(1>0) { *p=3; } }
Commande line: frama-c -jessie-analysis -jessie-gui file.c
What could be done in Jessie to warn users about:
- the loop for which termination condition or loop variant are not provided?
- unreachable return control point due to infinite loop (=> no post-condition can be met)?