From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Tue, 13 Aug 2013 11:32:43 +0000 (+0200)
Subject: model-checker : ignore in_use in s_smpi_mpi_datatype
X-Git-Tag: v3_9_90~128^2~4
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/c58613cc4fc2d6ace73c7f7840a71c7201afa2e2?hp=61fc380a9a01658181035a0d204c98967c27d7a4

model-checker : ignore in_use in s_smpi_mpi_datatype
---

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));
 }