Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000480Frama-CPlug-in > jessiepublic2010-05-12 18:572010-05-12 18:57
Assigned Tocmarche 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in Version 
Summary0000480: volatile annotation breaks type checker
DescriptionAdding a volatile annotation on some variables breaks the type checker. (Why 2.26) For example: #include // 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
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2010-05-12 18:57 tomahawkins New Issue
2010-05-12 18:57 tomahawkins Status new => assigned
2010-05-12 18:57 tomahawkins Assigned To => cmarche

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker