Changes between Version 16 and Version 17 of Introduction

Timestamp:

12/31/18 14:30:52 (7 years ago)

Author:

siegel

Comment:

--

Introduction

@@ -584 +584 @@
 === Verifying C/MPI Programs ===
 
+CIVL can verify C/MPI programs that use a subset of MPI.    The instructions for sequential programs apply equally to MPI programs.  In addition, one must specify either (1) the number of processes for the MPI program, or (2) an upper and a lower bound on the number of processes for the MPI program.
+
+In the following example, the C/MPI program `ring.c` is verified for exactly 5 processes:
+
+{{{
+civl verify -input_mpi_nprocs=5 ring.c
+}}}
+
+In the following example, `ring.c` is verified for any number of processes between 2 and 5, inclusive:
+
+{{{
+civl verify -input_mpi_nprocs_lo=2 -input_mpi_nprocs_hi=5 ring.c
+}}}
+