labels defined before loops and used after loops are not correctly translated in jessie

ID0001047: This issue was created automatically from Mantis Issue 1047. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0001047	Frama-C	Plug-in > jessie	public	2011-12-12	2011-12-12

Reporter	chernikova	Assigned To	cmarche	Resolution	open
Priority	normal	Severity	major	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Carbon-20110201	Target Version	-	Fixed in Version	-

Description :

An example with a label in a ghost (or not) statement: void main(){ int p = 1; int i;

//@ ghost L:
for (i=0; i<10; i++)
p = 2;
//@ assert \at(p,L)==p-1;

}

frama-c -jessie labels-bug.c results as: ... File "labels-bug.jc", line 52, characters 38-46: typing error: label `L' not found ...

labels-bug.jc contains label L: .... (C_1 : (p = 1)); (L : ()); (C_2 : (i = 0));

  loop 
  while (true)
  {  
   ...
  };
  (while_0_break : ());
  
  {  
     (assert for default: (C_7 : (\at(p,L) == (p - 1))));
     ()
  };

Attachments

• labels-bug.c