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 - 2018 MantisBT Team
Powered by Mantis Bugtracker