I have the following program:
#define mARRAY_LEN(a) ((int)(sizeof(a) / sizeof((a)[0])))
typedef struct {
int value;
} Item_t;
typedef struct {
Item_t items[10];
int count;
} Table_t;
/*@
requires \valid(table);
requires 0 <= index <= table->count;
requires table->count < mARRAY_LEN(table->items);
assigns table->items[index..\old(table->count)];
assigns table->count;
ensures \forall integer j; 0 <= j < index ==> table->items[j] == \old(table->items[j]);
ensures \forall integer j; index < j <= \old(table->count) ==> table->items[j] == \old(table->items[j-1]);
ensures table->items[index] == item;
ensures table->count == \old(table->count) + 1;
*/
static void tableInsert(Table_t *table, int index, Item_t item)
{
/*@
loop invariant index <= i <= table->count;
loop invariant \forall integer j; 0 <= j < i ==>
table->items[j] == \at(table->items[j], Pre);
loop invariant \forall integer j; i < j <= table->count ==>
table->items[j] == \at(table->items[j-1], Pre);
loop assigns i, table->items[index+1 .. table->count];
loop variant i - index;
*/
for (int i = table->count; i > index; i--) {
//@ assert(i > 0);
table->items[i] = table->items[i - 1];
}
table->items[index] = item;
table->count++;
}
When I test it using:
frama-c -wp-verbose 0 -wp Test.c -then -report
WP is not able to proof it:
[kernel] Parsing Test.c (with preprocessing)
[wp] Warning: Missing RTE guards
[report] Computing properties status...
-------------------------------------------------------------------------------
--- Properties of Function 'tableInsert'
--------------------------------------------------------------------------------
[ Partial ] Post-condition (file Test.c, line 21)
By Wp.typed, with pending:
- Loop assigns (file Test.c, line 40)
- Invariant (file Test.c, line 32)
- Invariant (file Test.c, line 37)
[ Partial ] Post-condition (file Test.c, line 22)
By Wp.typed, with pending:
- Loop assigns (file Test.c, line 40)
- Invariant (file Test.c, line 32)
- Invariant (file Test.c, line 37)
[ Partial ] Post-condition (file Test.c, line 23)
By Wp.typed, with pending:
- Loop assigns (file Test.c, line 40)
- Invariant (file Test.c, line 32)
- Invariant (file Test.c, line 37)
[ - ] Post-condition (file Test.c, line 25)
tried with Wp.typed.
[ Valid ] Exit-condition (generated)
by Unreachable Annotations.
[ Partial ] Termination-condition (generated)
By Trivial Termination, with pending:
- Loop assigns (file Test.c, line 40)
- Invariant (file Test.c, line 32)
- Invariant (file Test.c, line 37)
[ - ] Loop assigns (file Test.c, line 40)
tried with Wp.typed.
[ - ] Assigns (file Test.c, line 18)
tried with Wp.typed.
[ Partial ] Loop variant at loop (file Test.c, line 44)
By Wp.typed, with pending:
- Loop assigns (file Test.c, line 40)
- Invariant (file Test.c, line 32)
- Invariant (file Test.c, line 37)
[ - ] Invariant (file Test.c, line 32)
tried with Wp.typed.
[ Partial ] Invariant (file Test.c, line 34)
By Wp.typed, with pending:
- Loop assigns (file Test.c, line 40)
- Invariant (file Test.c, line 32)
- Invariant (file Test.c, line 37)
[ - ] Invariant (file Test.c, line 37)
tried with Wp.typed.
[ Partial ] Assertion (file Test.c, line 45)
By Wp.typed, with pending:
- Loop assigns (file Test.c, line 40)
- Invariant (file Test.c, line 32)
- Invariant (file Test.c, line 37)
[ - ] Default behavior
tried with Frama-C kernel.
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
1 Completely validated
7 Locally validated
6 To be validated
14 Total
--------------------------------------------------------------------------------
But when I change the type of the value in Item_t to unsigned int WP is able to proof it.
[kernel] Parsing Test.c (with preprocessing)
[wp] Warning: Missing RTE guards
[report] Computing properties status...
--------------------------------------------------------------------------------
--- Properties of Function 'tableInsert'
--------------------------------------------------------------------------------
[ Valid ] Post-condition (file Test.c, line 21)
by Wp.typed.
[ Valid ] Post-condition (file Test.c, line 22)
by Wp.typed.
[ Valid ] Post-condition (file Test.c, line 23)
by Wp.typed.
[ Valid ] Post-condition (file Test.c, line 25)
by Wp.typed.
[ Valid ] Exit-condition (generated)
by Unreachable Annotations.
[ Valid ] Termination-condition (generated)
by Trivial Termination.
[ Valid ] Loop assigns (file Test.c, line 40)
by Wp.typed.
[ Valid ] Assigns (file Test.c, line 18)
by Wp.typed.
[ Valid ] Loop variant at loop (file Test.c, line 44)
by Wp.typed.
[ Valid ] Invariant (file Test.c, line 32)
by Wp.typed.
[ Valid ] Invariant (file Test.c, line 34)
by Wp.typed.
[ Valid ] Invariant (file Test.c, line 37)
by Wp.typed.
[ Valid ] Assertion (file Test.c, line 45)
by Wp.typed.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
14 Completely validated
14 Total
--------------------------------------------------------------------------------
It gets even more crazy, the proof works with long and short and char, or anything else. But not with int. int32_t doesn't work either.
Can someone please explain me why that is?
One only needs to modify this line so that the proof succeeds:
loop assigns i, table->items[index+1 .. table->count];
to
loop assigns i, table->items[index+1 .. \at(table->count, Pre)];
for some reason, that I should investigate in details, the separation with the items is hard to find for provers. Or at some point WP simplifies too many things. I don't know. Anyway the result is that we are not able to prove that table->count is not modified through the assigns.
Now, why does it work when changing the datatype to any other type?
It is due to the memory models. When another type is chosen, WP dispatches the count and the value in two different symbolic memories, which guarantees for free that they are separated (and solvers do not even have to reason about it anymore). Thus, table->count is a constant in the generated verification condition.