Skip to content
GitLab
Projects Groups Topics 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
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 168
    • Issues 168
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • 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
  • #1527

assign makes Jessie crash

ID0000303: This issue was created automatically from Mantis Issue 303. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0000303 Frama-C Plug-in > jessie public 2009-10-26 2014-02-12
Reporter boris Assigned To cmarche Resolution duplicate
Priority normal Severity crash Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Beryllium-20090901 Target Version - Fixed in Version -

Description :

Code [1] makes Jessie crash [2] on Beryllium-20090901.

[1] /*@ requires \valid(p) && \valid(q); ensures *p == \old(*q); ensures *q == \old(*p); assigns *p, *q; */ void Swap(int *p, int *q) { int temp; temp = *p; *p = *q; *q = temp; }

void Foo() { const int n=10; int a[n]; int i;

for(i=0; i<n; i++) a[i]=0; //@ loop assigns a[0..n-1]; for(i=1; i<n; i++) Swap(&a[i], &a[0]); }

[2] [kernel] preprocessing with "gcc -C -E -I. -dD tst.c" tst.c:17:[kernel] warning: Variable-sized local variable a [jessie] Starting Jessie translation [kernel] No code for function __builtin_alloca, default assigns generated [jessie] Producing Jessie files in subdir tst.jessie [jessie] File tst.jessie/tst.jc written. [jessie] File tst.jessie/tst.cloc written. [jessie] Calling Jessie tool in subdir tst.jessie Generating Why function Swap Generating Why function Foo ** Jc_interp_misc.transpose_location_list: TODO: parameters ** memory (mem-field(int_M),q_4) in memory set (mem-field(int_M),p_3), (mem-field(int_M),q_4) File "jc/jc_interp_misc.ml", line 733, characters 1-1: Uncaught exception: File "jc/jc_interp_misc.ml", line 733, characters 1-7: Assertion failed [jessie] user error: Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs tst.cloc tst.jc

Additional Information :

See also bug 80 http://bts.frama-c.com/view.php?id=80

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