source: CIVL/examples/contracts/contractsMPI/mpiValid.c@ ff25b9a

1.23 2.0 main test-branch
Last change on this file since ff25b9a was 6a0885e, checked in by Ziqing Luo <ziqing@…>, 10 years ago

fix bugs in contract transformer

git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@3656 fb995dde-84ed-4084-dfe6-e5aef3e2452c

  • Property mode set to 100644
File size: 447 bytes
Line 
1#include <mpi.h>
2#include <civl-mpi.cvh>
3
4int main() {
5 MPI_Init(NULL, NULL);
6
7 MPI_Datatype datatype;
8 void * buf = NULL;
9 double * dbuf;
10
11 $havoc(&datatype);
12 $assume(datatype == MPI_DOUBLE || datatype == MPI_INT || datatype == MPI_CHAR || datatype == MPI_2INT);
13 buf = $mpi_valid(2, datatype);
14 if (datatype == MPI_DOUBLE) {
15 dbuf = (double *)buf;
16 dbuf[0] = 2.0;
17 $assert(dbuf[0] > 0);
18 }
19 $free(buf);
20 MPI_Finalize();
21}
Note: See TracBrowser for help on using the repository browser.