Changes between Version 12 and Version 13 of Introduction

Timestamp:

12/29/18 20:41:10 (7 years ago)

Author:

siegel

Comment:

--

Introduction

@@ -425 +425 @@
 
 
-=== Verifying C Programs ===
-
+=== Verifying Sequential C Programs ===
+
+
+{{{
+#include <assert.h>
+#include <stdio.h>
+#ifdef _CIVL
+#include <civlc.cvh>
+$input int B=5, N;
+$assume(1<=N && N<=B);
+#else
+#define N 100
+#endif
+int sum=0;
+int main() {
+  for (int i = 1; i <= N; i++) sum += i;
+  printf("N=%d, sum = %d\n", N, sum);
+  assert(sum == (N+1)*N/2);
+}
+}}}
+
+{{{
+$ cc -o sum sum.c
+$ ./sum
+N=100, sum = 5050
+$ 
+}}}
+
+{{{
+$ civl verify sum.c 
+CIVL v1.18+ of 2018-12-28 -- http://vsl.cis.udel.edu/civl
+N=5, sum = 15
+N=4, sum = 10
+N=3, sum = 6
+N=2, sum = 3
+N=1, sum = 1
+
+=== Source files ===
+sum.c  (sum.c)
+
+
+=== Command ===
+civl verify sum.c 
+
+=== Stats ===
+   time (s)            : 2.26
+   memory (bytes)      : 163053568
+   max process count   : 1
+   states              : 51
+   states saved        : 31
+   state matches       : 0
+   transitions         : 50
+   trace steps         : 16
+   valid calls         : 54
+   provers             : cvc4, z3
+   prover calls        : 13
+
+=== Result ===
+The standard properties hold for all executions.
+$
+}}}