*** empty log message ***

[splint.git] / src / uentry.c

diff --git a/src/uentry.c b/src/uentry.c
index 9f5f3a5bc7f20fdce4163fae9e9f99ab2c5084fe..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);