2021-01-24 07:02 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001750Frama-CPlug-in > wppublic2015-03-17 22:17
Reporterjens 
Assigned Topatrick 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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 Files
  • c file icon bit_and.c (402 bytes) 2014-04-11 18:50 -
    
    void bit_and_char(unsigned char a)
    {
       unsigned char b = a & 1;
       //@ assert b == 0 || b == 1;
    }
    
    void bit_and_short(unsigned short a)
    {
       unsigned short b = a & 1;
       //@ assert b == 0 || b == 1;
    }
    
    void bit_and_int(unsigned int a)
    {
       unsigned int b = a & 1;
       //@ assert b == 0 || b == 1;
    }
    
    void bit_and_long(unsigned long a)
    {
       unsigned long b = a & 1;
       //@ assert b == 0 || b == 1;
    }
    
    
    c file icon bit_and.c (402 bytes) 2014-04-11 18:50 +

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

-Notes

~0005218

patrick (developer)

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)

Fix committed to master branch.
+Notes

-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 Source_changeset_attached => framac master 959cc69e
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
+Issue History