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.
Steps To Reproduce
Additional InformationReported on Frama-C Discuss
TagsNo tags attached.
Relationships
Attached Files
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

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.