Frama-C Bug Tracking System - Frama-C
View Issue Details
0000651Frama-CPlug-in > jessiepublic2010-12-24 16:042010-12-24 16:04
evdenis 
cmarche 
normalminoralways
assignedopen 
Frama-C Boron-20100401 
 
0000651: array id "shift"
void alg( void ) { long shift[255]; /*@ @ loop invariant 0 <= i <= 255; @ loop variant 255 - i; @ loop invariant \forall integer k; 0 <= k < i ==> @ shift[k] == -1; @*/ for ( unsigned i = 0; i < 255; ++i ) shift[i] = -1; } tester@ubuntu-fm:~/workspace/test5$ frama-c -jessie -jessie-atp gui alg1.c [kernel] preprocessing with "gcc -C -E -I. -dD alg1.c" [jessie] Starting Jessie translation [jessie] Producing Jessie files in subdir alg1.jessie [jessie] File alg1.jessie/alg1.jc written. [jessie] File alg1.jessie/alg1.cloc written. [jessie] Calling Jessie tool in subdir alg1.jessie Generating Why function alg [jessie] Calling VCs generator. gwhy-bin [...] why/alg1.why Computation of VCs... decomp_fun_type=long_P pointer ref File "why/alg1.why", line 452, characters 36-73: This term cannot be applied (either it is not a function or it is applied to non pure arguments) make: *** [alg1.stat] Error 1 [jessie] user error: Jessie subprocess failed: make -f alg1.makefile gui
No tags attached.
c alg.c (249) 2010-12-24 16:04
https://bts.frama-c.com/file_download.php?file_id=144&type=bug
Issue History
2010-12-24 16:04evdenisNew Issue
2010-12-24 16:04evdenisStatusnew => assigned
2010-12-24 16:04evdenisAssigned To => cmarche
2010-12-24 16:04evdenisFile Added: alg.c

There are no notes attached to this issue.