source: CIVL/examples/contracts/contractsMPI/mpiValid.c@ 397ae5f

main test-branch
Last change on this file since 397ae5f was ea777aa, checked in by Alex Wilton <awilton@…>, 3 years ago

Moved examples, include, build_default.properties, common.xml, and README out from dev.civl.com into the root of the repo.

git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@5704 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.