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 - 2019 MantisBT Team
Powered by Mantis Bugtracker