Frama-C Bug Tracking System - Frama-C
View Issue Details
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.
Relationships
Attached Files

Notes
(0002742)
correnson   
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   
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 ModifiedUsernameFieldChange
2012-02-29 16:17corrensonNew Issue
2012-02-29 16:17corrensonStatusnew => assigned
2012-02-29 16:17corrensonAssigned To => correnson
2012-02-29 17:00corrensonNote Added: 0002742
2012-02-29 17:00corrensonStatusassigned => acknowledged
2012-03-01 09:59patrickNote Added: 0002745
2012-03-01 10:00patrickStatusacknowledged => resolved
2012-03-01 10:00patrickResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed