Given an MPI program:

#include <mpi.h>
 ...
#include <stdio.h>

int a, b, ...;

... function(){
  ...
}
...

int main(){
  ....
}

It is translated to a CIVL-C program by ABC:

#include <mpi.h> // all included files are moved above to the new file scope.
...
#include <stdio.h>

$input int argc;//optional, only necessary when the original main function has arguments.
$input char** argv;//optional, only necessary when the original main function has arguments.
$input int NPROCS;
$input int NPROCS_UPPER;
$input int NPROCS_LOWER;
$assume NPROCS_LOWER < NPROCS && NPROCS <= NPROCS_UPPER;
CMPI_Gcomm GCOMM_WORLD = CMPI_Gcomm_create($here, NPROCS);

void MPI_Process(int _rank){
  ...
}

void main(){
  $proc procs[NPROCS];
   
  for(int i = 0; i < NPROCS; i++){
    procs[i] = $spawn MPI_Process(i);
  }
  for(int i = 0; i < NPROCS; i++){
    $wait(procs[i]);
  }
  CMPI_Gcomm_destroy(GCOMM_WORLD);
}

Whereas MPI_Process() is a wrapper of the original MPI program with some additional :

void MPI_Process(int _rank){
  MPI_Comm MPI_COMM_WORLD = MPI_Comm_create($here, _rank);
  
  //SLIGHTLY-MODIFIED ORIGINAL PROGRAM;
  int a, b, ...;
  ... function(){...}
  ...
  ... __main(){...} // renamed main() to __main()
  ....
  //ORIGINAL PROGRAM ENDS HERE;
  __main();
  MPI_Comm_destroy(MPI_COMM_WORLD);
}