LoopEntry vs LoopInit

ID0002203: This issue was created automatically from Mantis Issue 2203. Further discussion may take place here.

Id	Project	Category	View	Due Date	Updated
ID0002203	Frama-C	Documentation > ACSL	public	2016-01-26	2016-06-21


Reporter	jens	Assigned To	virgile	Resolution	fixed
Priority	high	Severity	text	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Magnesium	Target Version	-	Fixed in Version	Frama-C Aluminium

Description :

In Example 2.30 (Page 43) of the ACSL implementation document (for both Magnesium and Sodium) the code snippet uses the label "LoopInit". I think "LoopEntry" is meant.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information