Code annotation in the middle of labels

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

---

Id	Project	Category	View	Due Date	Updated
ID0001327	Frama-C	Kernel	public	2012-12-12	2012-12-12

Reporter	signoles	Assigned To	virgile	Resolution	open
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	-	Target Version	-	Fixed in Version	-

Description :

Consider this code:

void foo(int x) { switch (x) { case 0: /*@ assert \true; */ case 1: ; } }

Frama-C encloses both the assertion and the "case 1: ;" into a block inside the "case 0" as shown below. I'm not sure that it is the expected behavior (either the block should also include "case 0" or this program should be rejected as syntactically incorrect).

$ frama-c -kernel-debug 1 a.i /* Generated by Frama-C */ void foo(int x) {

/* */ /sid:2/ switch (x) {

/*  */
case 0: 
/*sid:3*/
/*block:begin*/
  { 
    /*  */
    /*sid:4*/ /*@ assert \true; */ ;
    case 1: /*sid:5*/ ; }
  
/*block:end*/

} /sid:8/ return; }

Note: if you add a semi-colon right after the assertion, there is no issue.