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.