type error in generated why file
ID0000178: This issue was created automatically from Mantis Issue 178. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000178 | Frama-C | Plug-in > jessie | public | 2009-07-09 | 2009-07-09 |
| Reporter | derepas | Assigned To | cmarche | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Beryllium-20090601-beta1 | Target Version | - | Fixed in Version | - |
Description :
Let us consider the following program 'simple.c': void g(int * j, int *k) { int tmp= *j; *j=*k; *k=tmp; }
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).