Changes between Version 14 and Version 15 of Introduction

Timestamp:

12/31/18 14:11:53 (7 years ago)

Author:

siegel

Comment:

--

Introduction

@@ -429 +429 @@
 Since almost anything you can do in sequential C is also legal CIVL-C, there is not much you have to do to apply the verifier to C programs.
 
-The verifier requires a complete program --- i.e., there must be a main function --- and there is usually some set-up that you want to do for CIVL that is different than what you want the program to do in normal use.    For this reason, there is a preprocessor object-like macro `_CIVL` which is defined when using the CIVL verifier.   This allows you to insert some CIVL-C code that will be used for verification, without interfering with the normal compilation and use of the program.   An example follows.
+The verifier requires a complete program --- i.e., there must be a main function --- and there is usually some set-up that you want to do for CIVL that is different than what you want the program to do in normal use.    For this reason, there is a preprocessor object-like macro `_CIVL` which is defined when using the CIVL verifier.   This allows you to insert some CIVL-C code that will be used for verification, without interfering with the normal compilation and use of the program.   Consider the following example, `sum.c`:
 
 {{{
@@ -449 +449 @@
 }}}
 
+The program can be compiled and executed as usual...
+
 {{{
 $ cc -o sum sum.c
@@ -455 +457 @@
 $ 
 }}}
+
+...and it can be verified using CIVL:
 
 {{{
@@ -490 +494 @@
 }}}
 
-
-There are some limitations.   Support for the standard library is only partial.   Small bounds will have to be placed on many parameters in order for CIVL verification to terminate (or terminate in a reasonable amount of time).  
-
-Another approach for separating the CIVL driver code from the "real" program is to place these in separate translation units.   
+Another approach for separating the CIVL driver code from the "real" program is to place these in separate translation units.   In the following example, a toy library "sumlib" has been implemented using a header file `sumlib.h` and an implementation `sumlib.c`:
+
+{{{
+basie:sumlib siegel$ cat sumlib.c
+
+#include "sumlib.h"
+int sum(int n) {
+  int result = 0;
+  for (int i=1; i<=n; i++) result += i;
+  return result;
+}
+}}}
+
+A simple test has been implemented in a separate translation unit named `sumlib_test.c`.   The translation units can be compiled, linked, and executed, in the usual way.
+
+{{{
+basie:sumlib siegel$ cat sumlib_test.c
+
+#include <stdio.h>
+#include <assert.h>
+#include "sumlib.h"
+#define N 100
+int main() {
+  int result = sum(N);
+  printf("N=%d, sum = %d\n", N, result);
+  assert(result == (N+1)*N/2);
+}
+
+basie:sumlib siegel$ cc sumlib_test.c sumlib.c
+basie:sumlib siegel$ ./a.out
+N=100, sum = 5050
+}}}
+
+Finally, a CIVL verification driver is provided in another translation unit, `sumlib_driver.cvl`.   The CIVL verifier can be applied to the whole program composed of the two translation units `sumlib_driver.cvl` and `sumlib.c`:
+
+{{{
+basie:sumlib siegel$ cat sumlib_driver.cvl
+
+#include <stdio.h>
+#include "sumlib.h"
+$input int B=5, N;
+$assume(1<=N && N<=B);
+int main() {
+  int result = sum(N);
+  printf("N=%d, sum = %d\n", N, result);
+  $assert(result == (N+1)*N/2);
+}
+
+basie:sumlib siegel$ civl verify sumlib_driver.cvl sumlib.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 ===
+sumlib_driver.cvl  (sumlib_driver.cvl)
+sumlib.h  (sumlib.h)
+sumlib.c  (sumlib.c)
+
+
+=== Command ===
+civl verify sumlib_driver.cvl sumlib.c 
+
+=== Stats ===
+   time (s)            : 2.78
+   memory (bytes)      : 163053568
+   max process count   : 1
+   states              : 47
+   states saved        : 32
+   state matches       : 0
+   transitions         : 46
+   trace steps         : 16
+   valid calls         : 49
+   provers             : cvc4, z3
+   prover calls        : 13
+
+=== Result ===
+The standard properties hold for all executions.
+}}}
+
+There are limitations to the application of CIVL to C programs.   Support for the standard library is only partial.   Small bounds will have to be placed on many parameters in order for CIVL verification to terminate (or terminate in a reasonable amount of time).  
 
 === Verifying C/MPI Programs ===