Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 173
    • Issues 173
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2543
Closed
Open
Issue created Apr 07, 2009 by Virgile Prevosto@virgileOwner

Jessie crashes on simple program without annotations

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)

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking