Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002296Frama-CPlug-in > wppublic2017-05-08 13:182017-05-08 13:18
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeverityfeatureReproducibilityalways
StatusassignedResolutionopen 
PlatformPhosphorus-20170501-beta1OSxubuntu 16.04.1OS Version
Product Version 
Target VersionFixed in Version 
Summary0002296: axiom about bounds of lsl result needed in the long run
DescriptionRunning "frama-c -wp and.c" on the attached program fails to prove the assertion in line 5, although it should follow immediately from the assignment in line 4.

Looking at the generated mlw file shows that "k=to_uint16(k)" can't be proven (variable name taken from c source). Apparently, the range boundaries of m from the contract in line 2 aren't propagated to m<<1.

In the long run, when bit operations will be handled in a satisfactory way, this issue should be resolved, too; the attached program can be used as a regeression test for it.
TagsNo tags attached.
Attached Filesc file icon and.c [^] (122 bytes) 2017-05-08 13:18 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2017-05-08 13:18 Jochen New Issue
2017-05-08 13:18 Jochen Status new => assigned
2017-05-08 13:18 Jochen Assigned To => correnson
2017-05-08 13:18 Jochen File Added: and.c


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker