From c58613cc4fc2d6ace73c7f7840a71c7201afa2e2 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Tue, 13 Aug 2013 13:32:43 +0200 Subject: [PATCH 1/1] model-checker : ignore in_use in s_smpi_mpi_datatype --- src/smpi/smpi_mpi_dt.c | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/smpi/smpi_mpi_dt.c b/src/smpi/smpi_mpi_dt.c index 0db4d81a21..5fb0a1d17e 100644 --- a/src/smpi/smpi_mpi_dt.c +++ b/src/smpi/smpi_mpi_dt.c @@ -13,6 +13,8 @@ #include "private.h" #include "smpi_mpi_dt_private.h" +#include "mc/mc.h" +#include "simgrid/modelchecker.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(smpi_mpi_dt, smpi, "Logging specific to SMPI (datatype)"); @@ -299,6 +301,9 @@ void smpi_datatype_create(MPI_Datatype* new_type, int size,int lb, int ub, int h new_t->substruct = struct_type; new_t->in_use=0; *new_type = new_t; + + if(MC_is_active()) + MC_ignore(&(new_t->in_use), sizeof(new_t->in_use)); } void smpi_datatype_free(MPI_Datatype* type){ @@ -321,12 +326,18 @@ void smpi_datatype_free(MPI_Datatype* type){ void smpi_datatype_use(MPI_Datatype type){ if(type)type->in_use++; + + if(MC_is_active()) + MC_ignore(&(type->in_use), sizeof(type->in_use)); } void smpi_datatype_unuse(MPI_Datatype type){ if(type && type->in_use-- == 0 && (type->flags & DT_FLAG_DESTROYED)) smpi_datatype_free(&type); + + if(MC_is_active()) + MC_ignore(&(type->in_use), sizeof(type->in_use)); } -- 2.20.1