Skip to content
Snippets Groups Projects

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

Merged Virgile Prevosto requested to merge fix/acsl-example into master
1 file
+ 3
2
Compare changes
  • Side-by-side
  • Inline
+ 3
2
@@ -29,6 +29,7 @@ ACSL is a <em>formal</em> language.</p>
@@ -29,6 +29,7 @@ ACSL is a <em>formal</em> language.</p>
<div class="sidecode">
<div class="sidecode">
<pre>
<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>
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>
@@ -38,8 +39,8 @@ ACSL is a <em>formal</em> language.</p>
\forall integer i;
\forall integer i;
0 <= i < n ==> a[i] == 0;
0 <= i < n ==> a[i] == 0;
*/
*/
void set_to_0(int* a, int n){
void set_to_0(int* a, size_t n){
int i;
size_t i;
/*@
/*@
loop invariant 0 <= i <= n;
loop invariant 0 <= i <= n;
Loading