2021-03-02 02:24 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000594Frama-CKernelpublic2012-09-19 17:16
Assigned Tovirgile 
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)

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

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

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

TagsNo tags attached.
Attached Files




yakobowski (manager)

This bug got resolved at some point.

-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