volatile annotation breaks type checker
ID0000480: This issue was created automatically from Mantis Issue 480. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000480 | Frama-C | Plug-in > jessie | public | 2010-05-12 | 2010-05-12 |
| Reporter | tomahawkins | Assigned To | cmarche | Resolution | open |
| Priority | normal | Severity | crash | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Boron-20100401 | Target Version | - | Fixed in Version | - |
Description :
Adding a volatile annotation on some variables breaks the type checker. (Why 2.26) For example:
#include <stdint.h>
// This works. //int32_t a;
// This doesn't. volatile int32_t a;
void f(double b) { a = (int32_t) b; }
Yields: e0082888@e0082888-laptop:~$ frama-c -jessie test.c [kernel] preprocessing with "gcc -C -E -I. -dD test.c" [jessie] Starting Jessie translation [jessie] Producing Jessie files in subdir test.jessie [jessie] File test.jessie/test.jc written. [jessie] File test.jessie/test.cloc written. [jessie] Calling Jessie tool in subdir test.jessie File "test.jc", line 34, characters 41-55: typing error: bad cast to integer [jessie] user error: Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs test.cloc test.jc