2021-03-02 14:26 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000722Frama-CKernel > ACSL implementationpublic2014-02-12 16:54
Reporterpatrick 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0001498

patrick (developer)

bug 2 and 3 are still there...

~0003947

patrick (developer)

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)

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

-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
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
2013-12-19 01:12 patrick Source_changeset_attached => framac master d732d699
2014-02-12 16:54 patrick Source_changeset_attached => framac stable/neon d732d699
+Issue History