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.