Blog

Tag Archives: ACSL

loop assigns, part 2
Virgile Prevosto on 15 October 2010

Context Last week's post asked how to express a loop assigns for the following code: void fill(char* a char x) { for(;*a;a++) *a = x; return; } The difficulty here is that the pointer a is modified at each step of the loop and that we must take this fact...

Read More

Specification of loop assigns
Virgile Prevosto on 6 October 2010

A simple example Broadly speaking, every location which is not mentioned in such a clause should have the same value when exiting the corresponding code as it when entering it. For instance, if we take the following declaration (extracted from ACSL by Example) /*@ assigns \ othing; */ bool equal(const...

Read More