Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000594Frama-CKernelpublic2010-10-02 10:572012-09-19 17:16
Reporterdpariente 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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

-  Notes
(0002834)
yakobowski (manager)
2012-04-05 01:21

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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker