Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000178Frama-CPlug-in > jessiepublic2009-07-09 11:542009-07-09 18:11
Assigned Tocmarche 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090601-beta1 
Target VersionFixed in Version 
Summary0000178: type error in generated why file
DescriptionLet us consider the following program 'simple.c':
void g(int * j, int *k) {
  int tmp= *j;

void f(int * vector, int size) {
  int i=0;
  if (i<size)
    g (&vector[i],&vector[i+1]);

The command line 'frama-c -main f -jessie simple.c' generates the following error:
[kernel...] preprocessing with "gcc -C -E -I. -dD simple.c"
Starting Jessie translation
Producing Jessie files in subdir simple.jessie
File simple.jessie/simple.jc written.
File simple.jessie/simple.cloc written.
Calling Jessie tool in subdir simple.jessie
Generating Why function g
Generating Why function f
Calling VCs generator.
gwhy-bin [...] why/simple.why
Computation of VCs...
File "why/simple.why", line 552, characters 9-49:
Term i is expected to have type int
make: *** [simple.stat] Erreur 1
Jessie subprocess failed: make -f simple.makefile gui

The funny thing is that when the body of function g is empty this error does not occur (though the error seems to be in function f).
TagsNo tags attached.
Attached Files

- Relationships
related to 0000370closedcmarche pragma JessieIntegerModel 

-  Notes
virgile (developer)
2009-07-09 18:11

it seems like an integer_of_int32 conversion is missing when translating arguments of ranges of integers.

- Issue History
Date Modified Username Field Change
2009-07-09 11:54 derepas New Issue
2009-07-09 18:11 virgile Note Added: 0000243
2009-07-09 18:11 virgile Assigned To => cmarche
2009-07-09 18:11 virgile Status new => confirmed
2010-01-14 08:41 signoles Relationship added related to 0000370

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker