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
Reportertomahawkins 
Assigned Tocmarche 
PrioritynormalSeveritycrashReproducibilityalways
StatusassignedResolutionopen 
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 <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

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