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