T g0, T2 g1, ...;
/*@\mpi_collective(kind, comm):
    requires Gamma;
    requires psi;
    assigns  Delta;
    ensures  phi;
    ensures  Upsilon;
 */
T f(T a, T2 *b, ...) {

  return expr;
}


void f_driver() {
  $mpi_comm_rank, $mpi_comm_size;
  MPI_Comm_rank(comm. &$mpi_comm_rank);
  MPI_Comm_size(comm. &$mpi_comm_size);
  T a, T2 *b, ...;
  $havoc(&a); $havoc(&b); ...;
  T2 b_obj;

  MPI_Barrier(...);
  $assume(psi[b == &b_obj / \valid(b), ...]);
  MPI_Barrier(...);
  $collate_state _pre_cs = $mpi_snapshot(comm, $here);
  $run $when ($collate_complete(_pre_cs)) $collate_vc(Gamma, _pre_cs);

  $write_set_push();  f_origin();
  $mem m = $write_set_pop();
  $assert($mem_contains(Delta, m));

  $collate_state _post_cs = $mpi_snapshot(comm, $here);
  $run $when ($collate_complete(_post_cs))
    $collate_vc(Upsilon, _post_cs);

  MPI_Barrier(comm);
  $state * _pre_s = $collate_get_state(_pre_cs);
  $assert(phi[$value_at/\old, \on]);
  MPI_Barrier(comm);
  $mpi_unsnapshot(_pre_cs);
  $mpi_unsnapshot(_post_cs);
}

T f(T a, T2 *b, ...) {
  $mpi_comm_rank, $mpi_comm_size;
  MPI_Comm_rank(comm. &$mpi_comm_rank);
  MPI_Comm_size(comm. &$mpi_comm_size);

  $collate_state _pre_cs = $mpi_snapshot(comm, $here);
  $run $when ($collate_complete(_pre_cs)) {
    $collate_vc(Gamma, _pre_cs);
    $with (_s_pre) $assert(psi);
  }
  
  $havoc(Delta);

  $collate_state _cs_post = $mpi_snapshot(comm, $here);
  $state* _s_post = $collate_get_state(_cs_post);
  $run $when ($collate_complete(_cs_post)) {
    $collate_vc(Upsilon, _cs_post);
    $with (_s_post) $aassume(phi);
  }
  $mpi_unsnapshot(_pre_cs);
  $mpi_unsnapshot(_post_cs);
}