Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000038Frama-CPlug-in > jessiepublic2009-04-07 15:312009-04-10 10:08
Assigned Tocmarche 
PlatformOSOS Version
Product VersionFrama-C Lithium-20081201 
Target VersionFixed in Version 
Summary0000038: Jessie crashes on simple program without annotations
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));


~/progs/fc/tst> frama-c -jessie-analysis tst4.c
[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/] Error 1
Jessie subprocess failed: make -f tst4.makefile simplify
Additional InformationClaude Marché: Issues lies in the lack of a conversion from int32 into int in pset generation (in jessie plugin)
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2009-04-07 15:31 virgile New Issue
2009-04-07 15:41 signoles Status new => acknowledged
2009-04-10 10:08 signoles Status acknowledged => assigned
2009-04-10 10:08 signoles Assigned To => cmarche

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker