Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000722Frama-CKernel > ACSL implementationpublic2011-02-14 15:102014-02-12 16:54
Reporterpatrick 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0000722: bitwise operator
Description1/ Feature request: implementation of x --> y and x <--> y at least as ~x|y and ~x^y

2/ Bug: lemma a: \forall int x; (x|x == -1); is not correctly parsed.

3/ Bug: lemma a: forall int x; (x|x) == -1 ; is correctly parsed, but pretty printed
as \forall int x; (x|x == -1); which is not correctly parsed.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0001498)
patrick (developer)
2011-02-14 15:16

bug 2 and 3 are still there...
(0003947)
patrick (developer)
2013-06-12 16:32

Bug 3 has been corrected, but when?
That could be done when reviewing the pretty printer for Fluorine.

Since
  \forall int x; (x|x) == -1;
is now pretty printed as follow
  \forall int x; (x|x) == -1;
bug 2 can be no more considered as a bug.

So,
  \forall int x; (x|x == -1);
isn't a correct predicate.
(0003948)
patrick (developer)
2013-06-12 16:35

1/ Feature request: implemented
2/ This bug is not confirmed
3/ Bug: corrected

- Issue History
Date Modified Username Field Change
2011-02-14 15:10 patrick New Issue
2011-02-14 15:10 patrick Status new => assigned
2011-02-14 15:10 patrick Assigned To => virgile
2011-02-14 15:16 svn Checkin
2011-02-14 15:16 patrick Note Added: 0001498
2011-02-14 15:17 patrick Description Updated
2013-06-12 16:32 patrick Note Added: 0003947
2013-06-12 16:35 patrick Note Added: 0003948
2013-06-12 16:35 patrick Status assigned => resolved
2013-06-12 16:35 patrick Resolution open => fixed
2013-06-18 10:53 signoles Status resolved => closed
2013-06-18 10:53 signoles Fixed in Version => Frama-C Fluorine-20130401


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker