loop invariant as hypothesis
ID0001621: This issue was created automatically from Mantis Issue 1621. Further discussion may take place here.
Id | Project | Category | View | Due Date | Updated |
---|---|---|---|---|---|
ID0001621 | Frama-C | Plug-in > wp | public | 2014-01-20 | 2014-01-24 |
Reporter | Anne | Assigned To | correnson | Resolution | open |
Priority | normal | Severity | minor | Reproducibility | have not tried |
Platform | - | OS | - | OS Version | - |
Product Version | Frama-C Fluorine-20130601 | Target Version | - | Fixed in Version | - |
Description :
Not sure if this is a bug or the intended behavior, but I am surprised that on the example below, I get:
[wp] [Alt-Ergo] Goal typed_f_loop_inv_l_nbits_established : Unknown
It seems that the loop invariant l_wsize is not used as an hypothesis ?
🚯
Steps To Reproduce void f (unsigned int wsize) {
unsigned int nbits = 0;
/*@ loop invariant l_wsize: wsize == 4 || wsize == 5 || wsize == 6;
@ loop invariant l_nbits: 0 <= nbits < wsize;
*/
for(int i = 0; i < 10; i++) {
}
}
Edited by Allan Blanchard