LoopCurrent
and LoopEntry
are indeed not supported by WP in Fluorine. This is fixed in the development version (see http://bts.frama-c.com/view.php?id=1353), and should appear in the next release.
Regarding the other pre-defined labels,
Pre
always refers to the state at the beginning of the function.Old
can only be used in a contract, and refers to the pre-state of this contract (i.e. the state in which therequires
andassumes
clauses are evaluated). It is thus equivalent toPre
for a function contract, but not for a statement contract (unless you make a contract enclosing the main block of your function).Here
means the program point where the corresponding annotation is evaluated. In a contract, its meaning depends on the clause in which it appears.Post
can only be used inensures
,assigns
,allocates
orfrees
clauses, and refer to the state at the end of the contract.