loop assigns error

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

---

Id	Project	Category	View	Due Date	Updated
ID0000650	Frama-C	Kernel	public	2010-12-24	2011-01-10

Reporter	evdenis	Assigned To	virgile	Resolution	not fixable
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Boron-20100401	Target Version	-	Fixed in Version	Frama-C Boron-20100401

Description :

Reproduced only when loop assigns is used.

First:

#include <limits.h> #include <unistd.h>

#define uchar unsigned char

#define BC_LEN UCHAR_MAX + 1

const uchar* alg( void ) { ssize_t bad_character[BC_LEN];

/*@
  @ loop invariant 0 <= i <= BC_LEN;
  @ loop variant BC_LEN - i;
      @ loop assigns bad_character[0..BC_LEN];
  @ loop invariant \forall integer k; 0 <= k < i ==>
  @ 		bad_character[k] == -1;
  @*/
for ( size_t i = 0; i < BC_LEN; ++i )
	bad_character[i] = -1;

return NULL;

}

tester@ubuntu-fm:~/workspace/test1$ frama-c alg1.c [kernel] preprocessing with "gcc -C -E -I. -dD alg1.c" alg1.c:16:[kernel] user error: Error during annotations analysis: unbound logic variable BC_LEN

16 - Third string with loop.

Second:

#include <limits.h> #include <unistd.h>

#define uchar unsigned char

#define BC_LEN UCHAR_MAX + 1

const uchar* alg( void ) { ssize_t bad_character[BC_LEN];

/*@
  @ loop invariant 0 <= i <= BC_LEN;
  @ loop variant BC_LEN - i;
      @ loop assigns bad_character[0..256];
  @ loop invariant \forall integer k; 0 <= k < i ==>
  @ 		bad_character[k] == -1;
  @*/
for ( size_t i = 0; i < BC_LEN; ++i )
	bad_character[i] = -1;

return NULL;

}

tester@ubuntu-fm:~/workspace/test1$ frama-c alg2.c [kernel] preprocessing with "gcc -C -E -I. alg2.c" alg2.c:14:[kernel] user error: Error during annotations analysis: unbound logic variable BC_LEN

14 - First string with loop.

Attachments

• alg1.c