Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000651Frama-CPlug-in > jessiepublic2010-12-24 16:042010-12-24 16:04
Reporterevdenis 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in Version 
Summary0000651: array id "shift"
Description
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
TagsNo tags attached.
Attached Filesc file icon alg.c [^] (249 bytes) 2010-12-24 16:04 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2010-12-24 16:04 evdenis New Issue
2010-12-24 16:04 evdenis Status new => assigned
2010-12-24 16:04 evdenis Assigned To => cmarche
2010-12-24 16:04 evdenis File Added: alg.c


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker