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 - 2019 MantisBT Team
Powered by Mantis Bugtracker