Frama-C Bug Tracking System - Frama-C
View Issue Details
0000502Frama-CPlug-in > jessiepublic2010-06-09 10:432010-06-13 13:02
pascal 
cmarche 
lowminoralways
assignedopen 
Frama-C Boron-20100401 
 
0000502: Unbound label in Jessie-generated Why file when using logic function in assigns clause
rot13.c: _________ /*@ predicate string_of_length{L}(unsigned char *s, integer n) = n >= 0 && \valid_range(s, 0, n) && s[n] == 0 && \forall integer k ; (0 <= k < n) ==> (s[k] != 0) ; lemma always_the_same_length{L}: \forall unsigned char *s, integer n1, integer n2 ; (string_of_length(s, n1) && string_of_length(s, n2)) ==> n1 == n2 ; */ /*@ axiomatic Length { logic integer length{L}(unsigned char *s) reads s[..] ; axiom string_length{L}: \forall integer n, unsigned char *s ; string_of_length(s, n) ==> length(s) == n ; } */ /*@ assigns \nothing ; */ unsigned char rot13_char(unsigned char c) { if ((c >= 'a' && c <= 'm') || (c >= 'A' && c <= 'M')) return c + 13; if ((c >= 'n' && c <= 'z') || (c >= 'N' && c <= 'Z')) return c - 13; return c; } /*@ requires \exists integer n ; 0 <= n <= 2000000000 && string_of_length(s,n) ; assigns s[..length{Old}(s)] ; // ensures is_rot13{Pre,Post}(s,s) ; */ void rot13(unsigned char *s) { int i; for(i=0; s[i]; ++i) { s[i] = rot13_char(s[i]); } } _________ Command: frama-c-Jessie -jessie rot13.c Obtained result: ... [jessie] Calling Jessie tool in subdir rot13.jessie Generating Why function rot13_char Generating Why function rot13 [jessie] Calling VCs generator. gwhy-bin [...] why/rot13.why Computation of VCs... File "why/rot13.why", line 836, characters 30-66: Unbound label '' make: *** [rot13.stat] Error 1 [jessie] user error: Jessie subprocess failed: make -f rot13.makefile gui The problem is caused by the line: assigns s[..length{Old}(s)] ;
No tags attached.
Issue History
2010-06-09 10:43pascalNew Issue
2010-06-09 10:43pascalStatusnew => assigned
2010-06-09 10:43pascalAssigned To => cmarche
2010-06-10 19:18svnCheckin

There are no notes attached to this issue.