"why" reports "unbound label"
ID0000361: This issue was created automatically from Mantis Issue 361. Further discussion may take place here.
|ID0000361||Frama-C||Plug-in > jessie||public||2009-12-15||2010-04-19|
|Product Version||Frama-C Beryllium-20090901||Target Version||-||Fixed in Version||Frama-C Boron-20100401|
"why" reports an "unbound label" if a C-label of a statement having more than one effect (e.g. "b[j++] = 3;") is referred to in an "\at(...)" within an acsl-assertion. See attached file "labelBug.c"; process it with and without the initial "#define showBug" uncommented.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information