Tag Archives: ACSL

restrict is not good for modular reasoning
Pascal Cuoq on 2 August 2012

ACSL There were quite a few posts recently that were concerned with ACSL, and a few more are planned for the near future. ACSL is a specification language for C (comparable with JML for Java, for those who know about JML). Some people call it a BISL, for “Behavioral Interface...

Read More

On arrays vs. pointer, the ACSL way
Virgile Prevosto on 31 July 2012

Some time ago, we saw that in C arrays and pointers have some subtle differences. A facetious colleague just remarked that this is also the case in ACSL especially if you use the \at(e L) construction which basically says that e is supposed to be evaluated in the state when...

Read More

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