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++) {
  }
}