Tag Archives: ACSL

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