2021-01-21 05:10 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001327Frama-CKernelpublic2012-12-12 16:55
Reportersignoles 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
Product Version 
Target VersionFixed in Version 
Summary0001327: Code annotation in the middle of labels
DescriptionConsider 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
<skip trace>
/* 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.
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes
There are no notes attached to this issue.
+Notes

-Issue History
Date Modified Username Field Change
2012-12-12 16:55 signoles New Issue
2012-12-12 16:55 signoles Status new => assigned
2012-12-12 16:55 signoles Assigned To => virgile
+Issue History