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).