2021-03-02 02:24 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000594Frama-CKernelpublic2012-09-19 17:16
Reporterdpariente 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0000594: Kernel error with RTE generated annotations: invalid operands (bitwise)
DescriptionAnalyzing:

void f(unsigned long x)
{ short y;
  y = (short )((x >> 4) & 255UL);
}

with:
frama-c -rte -rte-precond e105.c -print -no-unicode -ocode e105b.c

and then, analyzing the output file with:
frama-c e105b.c -no-unicode

gives:
e105b.c:5:[kernel] user error: invalid operands to binary &; unexpected integer and boolean in annotation.

TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0002834

yakobowski (manager)

This bug got resolved at some point.
+Notes

-Issue History
Date Modified Username Field Change
2010-10-02 10:57 dpariente New Issue
2010-10-05 08:38 signoles Status new => assigned
2010-10-05 08:38 signoles Assigned To => virgile
2012-04-05 01:21 yakobowski Note Added: 0002834
2012-04-05 01:21 yakobowski Status assigned => resolved
2012-04-05 01:21 yakobowski 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
+Issue History