From c08cd123340a0b291d4ddf67db137890125aa38e Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 15 Feb 2022 09:49:39 +0100
Subject: [PATCH] [acsl] provides an example that can actually be verified by
 WP

---
 html/acsl.html | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/html/acsl.html b/html/acsl.html
index 1ff03588..96f7efab 100755
--- a/html/acsl.html
+++ b/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;
-- 
GitLab