Tag Archives: ACSL

The restrict qualifier as an element of specification
Pascal Cuoq on 25 July 2012

An insightful interjection Stephen Canon, whose explanations about the fine points of floating-point I have appreciated on StackOverflow chimed in on the subject of the restrict qualifier. With minor edits for consistency with this blog's formatting: Consider memcpy(); its arguments are declared restrict. This not only means that the source...

Read More

Loop assigns, part 3: On the importance of loop invariants
Virgile Prevosto on 27 October 2010

Context Last week's post mentioned that it is not possible to prove the following loop assigns with Jessie: void fill(char* a, char x) { //@ loop assigns a, \at(a,Pre)[0..(a-\at(a,Pre)-1)]; for(;*a;a++) *a = x; return; } and in fact this annotation is not provable. An hint to where the issue lies...

Read More

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