GitLab

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

---

Id	Project	Category	View	Due Date	Updated
ID0002246	Frama-C	Plug-in > wp	public	2016-08-19	2016-12-05

Reporter	ghulette	Assigned To	correnson	Resolution	fixed
Priority	normal	Severity	major	Reproducibility	always
Platform	-	OS	Linux	OS Version	Ubuntu 16.04
Product Version	Frama-C Aluminium	Target Version	-	Fixed in Version	-

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; } }

Additional Information :

$ frama-c --version Aluminium-20160501

Steps To Reproduce :

See comments in description.

Attachments

• bad.c