GitLab

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

---

Id	Project	Category	View	Due Date	Updated
ID0001434	Frama-C	Plug-in > wp	public	2013-05-29	2013-05-30

Reporter	Allan Blanchard	Assigned To	correnson	Resolution	no change required
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Fluorine-20130501	Target Version	-	Fixed in Version	-

Description :

I have this small program+spec :

#define SIZE 8 #define NUM 4

int table[NUM] = {0}; int pages[NUM*SIZE] = {0};

/@ predicate validindex(integer i) = \valid(table+i) && \forall integer j; 0 <= j < SIZE ==> \valid(pages+iSIZE+j); */

/@ predicate coherent_clean{L}(integer i) = \forall integer j; 0 <= j < table[i] <= SIZE ==> pages[iSIZE+j] == 0; */

/*@ requires \forall integer i; 0 <= i < NUM ==> validindex(i); / void init(void) { /@ loop invariant 0 <= i <= NUM; loop invariant \forall integer j; 0 <= j < i ==> coherent_clean(j); loop assigns i, table[0 .. NUM-1]; loop variant NUM - i; */ for(int i = 0; i < NUM; i++){ table[i] = 0; } }

This one is not proved by frama-C + WP. But if I inline the predicate, like this :

void init(void) { /@ loop invariant 0 <= i <= NUM; loop invariant \forall integer j; 0 <= j < i ==> \forall integer k; 0 <= k < table[j] <= SIZE ==> pages[jSIZE+k] == 0; loop assigns i, table[0 .. NUM-1]; loop variant NUM - i; */ for(int i = 0; i < NUM; i++){ table[i] = 0; } }

It perfectly works