Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001108Frama-CPlug-in > wppublic2012-02-29 16:172012-09-19 17:16
Reportercorrenson 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001108: Bitwise Operators
DescriptionNo correspondance between C-bitwise operations of natural int-model and ACSL-bitwise ones.
Error in translation of (~) in C.
Additional InformationReported on Frama-C Discuss
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0002742)
correnson (manager)
2012-02-29 17:00

Partially fixed in R17407.
Still need work on casts, shfts and associated rte.
Current solution is :

/*@
  axiomatic Bitwise {
  axiom char_int: \forall integer x ; (TRIGGER: (char)(int) x) == (char) x ;
  }
@*/
                                                                                                                           
int main()
{
    char a = 5;
    char b = ~a;
                                                                                                                           
    //@ assert b == (char) ~a;
                                                                                                                           
    return 0;
}

[wp] Running WP plugin...
[wp] warning: Missing RTE guards
[wp] [Alt-Ergo] Goal store_main_assert : Valid
(0002745)
patrick (developer)
2012-03-01 09:59

That is fixed for:
//@ ensures \result == (int) (a & b);
int band(int a,int b) { return a & b ; }
//@ ensures \result == (int) (a | b);
int bor(int a,int b) { return a | b ; }
//@ ensures \result == (int) (a ^ b);
int bxor(int a,int b) { return a ^ b ; }
//@ ensures \result == (int) (~a) ;
int bnot(int a) { return ~a ; }
//@ ensures \result == (int) (a << n) ;
int lshift(int a,int n) { return a << n ; }
//@ ensures \result == (int) (a >> n) ;
int rshift(int a,int n) { return a >> n ; }

Of course, rshift and lshift have RTE threads.
They require a precondition.

- Issue History
Date Modified Username Field Change
2012-02-29 16:17 correnson New Issue
2012-02-29 16:17 correnson Status new => assigned
2012-02-29 16:17 correnson Assigned To => correnson
2012-02-29 17:00 correnson Note Added: 0002742
2012-02-29 17:00 correnson Status assigned => acknowledged
2012-03-01 09:59 patrick Note Added: 0002745
2012-03-01 10:00 patrick Status acknowledged => resolved
2012-03-01 10:00 patrick Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker