[acsl] provides an example that can actually be verified by WP

html/acsl.html

@@ -29,6 +29,7 @@ ACSL is a <em>formal</em> language.</p>
 
 <div class="sidecode">
 <pre>
+#include &lt;stddef.h&gt;
 /*@
   requires \valid(a+(0..n-1));<span class=inline>1</span><sidenote>ACSL provides specification primitives to cover the low-level aspects of the C programming language</sidenote><point></point>
 
@@ -38,8 +39,8 @@ ACSL is a <em>formal</em> language.</p>
   \forall integer i;
     0 <= i < n ==> a[i] == 0;
 */
-void set_to_0(int* a, int n){
-  int i;
+void set_to_0(int* a, size_t n){
+  size_t i;
 
   /*@
     loop invariant 0 <= i <= n;