Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001750Frama-CPlug-in > wppublic2014-04-11 18:502015-03-17 22:17
Reporterjens 
Assigned Topatrick 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in VersionFrama-C Sodium 
Summary0001750: Frama-C/WP fails to discharge simple bit operation for small integer types
DescriptionIn the attached file there are for simple functions that computes

     b = a & 1;
     //@ assert b == 0 || b == 1;

where a and b are of type
  unsigned char, unsigned short, unsigned int and unsigned long.

Only for the types unsigned int and unsigned long cab WP (in fact QED) discharge the assertion.
Both alt-ergo and CVC4 fail on unsigned char and unsigned short.

I would be very nice if Frama-C/WP could handle the other cases automatically as well.
TagsNo tags attached.
Attached Filesc file icon bit_and.c [^] (402 bytes) 2014-04-11 18:50 [Show Content]

- Relationships
related to 0001751closedpatrick Frama-C/WP "forgets" a proven assertion 

-  Notes
(0005218)
patrick (developer)
2014-06-10 12:48

Some axioms have to be added for alt-ergo:

axiom bit_test_introduction_land :
  (forall x:int [land(x, 1)| land(1, x)].
  ((not (land(x, 1) = 0)) -> bit_test(x, 0)))

axiom bit_test_introduction_land_bis :
  (forall x:int [land(x, 1)| land(1, x)].
  (bit_test(x, 0) -> (land(x, 1) = 1)))
(0005221)
patrick (developer)
2014-06-11 11:19

Fix committed to master branch.

- Issue History
Date Modified Username Field Change
2014-04-11 18:50 jens New Issue
2014-04-11 18:50 jens Status new => assigned
2014-04-11 18:50 jens Assigned To => correnson
2014-04-11 18:50 jens File Added: bit_and.c
2014-06-02 16:15 correnson Relationship added related to 0001751
2014-06-02 16:15 correnson Assigned To correnson => patrick
2014-06-10 12:48 patrick Note Added: 0005218
2014-06-11 11:19 patrick Note Added: 0005221
2014-06-11 11:19 patrick Status assigned => resolved
2014-06-11 11:19 patrick Resolution open => fixed
2015-03-17 22:17 signoles Fixed in Version => Frama-C Sodium
2015-03-17 22:17 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker