Unbound label in Jessie-generated Why file when using logic function in assigns clause

ID0000502: This issue was created automatically from Mantis Issue 502. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000502	Frama-C	Plug-in > jessie	public	2010-06-09	2010-06-13

Reporter	pascal	Assigned To	cmarche	Resolution	open
Priority	low	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Boron-20100401	Target Version	-	Fixed in Version	-

Description :

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)] ;