Kernel error with RTE generated annotations: invalid operands (bitwise)
ID0000594:
**This issue was created automatically from Mantis Issue 594. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000594 | Frama-C | Kernel | public | 2010-10-02 | 2012-09-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
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.
issue