Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001327Frama-CKernelpublic2012-12-12 16:552012-12-12 16:55
Reportersignoles 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
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 /* 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

-  Notes
There are no notes attached to this issue.

- 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


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker