Changes between Version 13 and Version 14 of Introduction

Timestamp:

12/30/18 23:48:42 (7 years ago)

Author:

siegel

Comment:

--

Introduction

@@ -427 +427 @@
 === Verifying Sequential C Programs ===
 
+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.
 
 {{{
@@ -488 +491 @@
 
 
+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.   
+
 === Verifying C/MPI Programs ===