diff --git a/html/acsl.html b/html/acsl.html index 1ff03588e0b4bec4b79c4c6ebddebb56e3937453..96f7efab59a3ada87bf4ac463cbfaf52c230efc6 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 <stddef.h> /*@ 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;