ID0000038: **This issue was created automatically from Mantis Issue 38. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0000038 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-04-10 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | open | | **Priority** | normal | **Severity** | minor | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - | ### Description : [bug 7541 from old bts, reported by Boris Hollas] Jessie crashes on the following code: void Copy(int *p, int *q) { *q = *p; } int foo(int a[]) { int i=1; Copy(&a[0], &a[i]); return i; } int main() { int a[2] = {1,2}; printf("%d\n", foo(a)); } Output: ~/progs/fc/tst> frama-c -jessie-analysis tst4.c Parsing [preprocessing] running gcc -C -E -I. -include C:\Frama-C\share\frama-c\jessie\jessie_prolog.h -dD tst4.c tst4.c:17: Warning: Body of function main falls-through. Adding a return statement Cleaning unused parts Symbolic link Starting semantical analysis Starting Jessie translation No code for function printf, default assigns generated tst4.c:15: Warning: skipping all arguments of implicit prototype printf Producing Jessie files in subdir tst4.jessie File tst4.jessie/tst4.jc written. File tst4.jessie/tst4.cloc written. Calling Jessie tool in subdir tst4.jessie Generating Why function Copy Generating Why function foo Generating Why function main Calling VCs generator. why -simplify [...] why/tst4.why File "why/tst4.why", line 1418, characters 8-49: Term i_27 is expected to have type int make: *** [simplify/tst4_why.sx] Error 1 Jessie subprocess failed: make -f tst4.makefile simplify ### Additional Information : Claude Marché: Issues lies in the lack of a conversion from int32 into int in pset generation (in jessie plugin)