*** empty log message ***

[splint.git] / src / exprNode.c

diff --git a/src/exprNode.c b/src/exprNode.c
index 4f36072412172350d108aeb8c8837cad8b28b3be..5e533e31524256788812c1c92facb759658fb200 100644 (file)
--- a/src/exprNode.c
+++ b/src/exprNode.c
@@ -105,16 +105,15 @@ static ctype ctypeType;
 static ctype filelocType; 
 static bool initMod = FALSE;
 
-static void exprNode_defineConstraints(/*@sef@*/ /*@special@*/ /*@notnull@*/ exprNode p_e)
-     /*@defines p_e->requiresConstraints,  p_e->ensuresConstraints,  p_e->trueEnsuresConstraints,  p_e->falseEnsuresConstraints @*/
-     ;
-     
-# define exprNode_defineConstraints(e)  \
-do{                                      (e)->requiresConstraints = constraintList_makeNew(); \
-                                         (e)->ensuresConstraints = constraintList_makeNew(); \
-                                         (e)->trueEnsuresConstraints = constraintList_makeNew(); \
-                                           (e)->falseEnsuresConstraints = constraintList_makeNew(); } while(FALSE)
-
+static void exprNode_defineConstraints(/*@sef@*/ /*@special@*/ /*@notnull@*/ exprNode e)
+   /*@defines e->requiresConstraints,  e->ensuresConstraints, 
+              e->trueEnsuresConstraints,  e->falseEnsuresConstraints @*/ 
+{
+  e->requiresConstraints = constraintList_makeNew (); 
+  e->ensuresConstraints = constraintList_makeNew (); 
+  e->trueEnsuresConstraints = constraintList_makeNew (); 
+  e->falseEnsuresConstraints = constraintList_makeNew (); 
+}
 
 /*
 ** must occur after library has been read
@@ -3189,8 +3188,20 @@ reflectEnsuresClause (uentry le, exprNode f, exprNodeList args)
                        } end_sRefSet_elements;
                    }
                }
-           } end_stateClauseList_elements ;
-           
+           } end_stateClauseList_elements ;        
+       }
+
+      DPRINTF (("Here: %s / %s",
+               uentry_unparseFull (le),
+               bool_unparse (uentry_hasMetaStateEnsures (le))));
+
+      if (uentry_hasMetaStateEnsures (le))
+       {
+         metaStateConstraint msc = uentry_getMetaStateEnsures (le);
+
+         TPRINTF (("Meta state constraint for %s: %s", uentry_unparse (le),
+                   metaStateConstraint_unparse (msc)));
+
        }
     }
 }
@@ -9964,9 +9975,12 @@ checkOneRepExpose (sRef ysr, sRef base,
                   sRef s2b)
 {
   if (!(sRef_isOnly (ysr) || sRef_isKeep (ysr) 
-       || sRef_isOwned (ysr) || sRef_isExposed (ysr)))
+       || sRef_isOwned (ysr) 
+       || sRef_isExposed (ysr)))
     {
-      if (sRef_isAnyParam (base) && !sRef_isExposed (base))
+      if (sRef_isAnyParam (base) && !sRef_isExposed (base)
+         && !sRef_isObserver (base)) /* evans 2001-07-11: added isObserver */
+
        {
          if (sRef_isIReference (ysr))
            {