Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002246Frama-CPlug-in > wppublic2016-08-19 01:302016-12-05 20:30
Reporterghulette 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSLinuxOS VersionUbuntu 16.04
Product VersionFrama-C Aluminium 
Target VersionFixed in Version 
Summary0002246: Switch statements seem to be unsound
Description// Run the following to see the problem: // $ frama-c -wp -wp-rte bad.c // // Frama-C does not detect the error in the ensures condition. You // can cause WP to report the error by commenting out the case 0 line, // or by passing the -simplify-cfg option. Maybe a problem with // switch statements? int x; /*@ requires x != 1; assigns x; ensures x != 1; */ void bad (int e) { switch (e) { case 0: break; case 1: x = 1; break; } }
Steps To ReproduceSee comments in description.
Additional Information$ frama-c --version Aluminium-20160501
TagsNo tags attached.
Attached Filesc file icon bad.c [^] (448 bytes) 2016-08-19 01:30 [Show Content]

- Relationships

-  Notes
(0006254)
correnson (manager)
2016-08-23 09:50

Thanks for reporting. The problem is related to simplification of empty (nop) switch cases.
(0006256)
correnson (manager)
2016-08-23 13:42

Fixed in trunk.
(0006302)
yakobowski (manager)
2016-12-05 20:30

Fixed in Frama-C Silicon.

- Issue History
Date Modified Username Field Change
2016-08-19 01:30 ghulette New Issue
2016-08-19 01:30 ghulette Status new => assigned
2016-08-19 01:30 ghulette Assigned To => correnson
2016-08-19 01:30 ghulette File Added: bad.c
2016-08-23 09:50 correnson Note Added: 0006254
2016-08-23 09:50 correnson Status assigned => acknowledged
2016-08-23 09:54 correnson Note Added: 0006255
2016-08-23 13:25 correnson Note Deleted: 0006255
2016-08-23 13:42 correnson Note Added: 0006256
2016-08-23 13:42 correnson Status acknowledged => resolved
2016-08-23 13:42 correnson Resolution open => fixed
2016-12-05 20:30 yakobowski Status resolved => closed
2016-12-05 20:30 yakobowski Note Added: 0006302


Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker