Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000348Frama-CPlug-in > jessiepublic2009-12-03 10:392009-12-03 14:19
Reporterboris 
Assigned Tocmarche 
PrioritynormalSeveritymajorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090901 
Target VersionFixed in Version 
Summary0000348: Arithmetic safety of bitwise operators cannot be verified
DescriptionJessie cannot verify arithmetic safety in the following code: typedef unsigned int uint32; uint32 b1(uint32 x, uint32 y) { return x^y; } uint32 b2(uint32 x, uint32 y) { return x&y; } uint32 b3(uint32 x, uint32 y) { return x|y; } uint32 b4(uint32 x) { return ~x; }
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000594)
boris (reporter)
2009-12-03 12:56

Jessie generates VCs for arithmetic overflow and can't prove any of them. Hence this code doesn't verify.

- Issue History
Date Modified Username Field Change
2009-12-03 10:39 boris New Issue
2009-12-03 12:56 boris Note Added: 0000594
2009-12-03 14:19 signoles Status new => assigned
2009-12-03 14:19 signoles Assigned To => cmarche


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker