*** empty log message ***

[splint.git] / src / uentry.c

diff --git a/src/uentry.c b/src/uentry.c
index 06be66a73ca4641f1d7328417c8d42798cc4c39e..978285080c346effff68b22d7f6afd79a3644752 100644 (file)
--- a/src/uentry.c
+++ b/src/uentry.c
@@ -1087,6 +1087,16 @@ static void uentry_reflectClauses (uentry ue, functionClauseList clauses)
              uentry_setModifies (ue, modifiesClause_takeMods (mlc));
            }
        }
+      else if (functionClause_isEnsures (el))
+       {
+         constraintList cl = functionClause_takeEnsures (el);
+         uentry_setPostconditions (ue, cl);
+       }
+      else if (functionClause_isRequires (el))
+       {
+         constraintList cl = functionClause_takeRequires (el);
+         uentry_setPreconditions (ue, cl);
+       }
       else if (functionClause_isState (el))
        {
          stateClause sc = functionClause_takeState (el);
@@ -7701,22 +7711,25 @@ checkMetaState (/*@notnull@*/ uentry old, /*@notnull@*/ uentry unew,
                        }
                      else
                        {
-                         if (mustConform 
-                             && optgenerror 
-                             (FLG_INCONDEFS,
-                              message ("%s %q inconsistently %rdeclared %s %s, %s as %s",
-                                       uentry_ekindName (unew),
-                                       uentry_getName (unew),
-                                       uentry_isDeclared (old),
-                                       fcnErrName (unew),
-                                       metaStateInfo_unparseValue (msinfo, 
-                                                                   stateValue_getValue (newval)),
-                                       uentry_specOrDefName (old),
-                                       metaStateInfo_unparseValue (msinfo,
-                                                                   stateValue_getValue (oldval))),
-                              uentry_whereDeclared (unew)))
+                         if (!stateValue_isError (newval))
                            {
-                             uentry_showWhereSpecified (old);
+                             if (mustConform 
+                                 && optgenerror 
+                                 (FLG_INCONDEFS,
+                                  message ("%s %q inconsistently %rdeclared %s %s, %s as %s",
+                                           uentry_ekindName (unew),
+                                           uentry_getName (unew),
+                                           uentry_isDeclared (old),
+                                           fcnErrName (unew),
+                                           metaStateInfo_unparseValue (msinfo, 
+                                                                       stateValue_getValue (newval)),
+                                           uentry_specOrDefName (old),
+                                           metaStateInfo_unparseValue (msinfo,
+                                                                       stateValue_getValue (oldval))),
+                                  uentry_whereDeclared (unew)))
+                               {
+                                 uentry_showWhereSpecified (old);
+                               }
                            }
                        }