Frama-C Bug Tracking System - Frama-C
View Issue Details
0000594Frama-CKernelpublic2010-10-02 10:572012-09-19 17:16
dpariente 
virgile 
normalminoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Oxygen-20120901 
0000594: Kernel error with RTE generated annotations: invalid operands (bitwise)
Analyzing: 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.
No tags attached.
Issue History
2010-10-02 10:57dparienteNew Issue
2010-10-05 08:38signolesStatusnew => assigned
2010-10-05 08:38signolesAssigned To => virgile
2012-04-05 01:21yakobowskiNote Added: 0002834
2012-04-05 01:21yakobowskiStatusassigned => resolved
2012-04-05 01:21yakobowskiResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed

Notes
(0002834)
yakobowski   
2012-04-05 01:21   
This bug got resolved at some point.