Prewinter break editing commit.

[splint.git] / src / clabstract.c

diff --git a/src/clabstract.c b/src/clabstract.c
index 2773f5fec6c291dad4e166f2ebde220f82c07d98..05754eff3dd86adfa505e2c42102a56229faf284 100644 (file)
--- a/src/clabstract.c
+++ b/src/clabstract.c
@@ -51,6 +51,12 @@
 ** right values are available in the right place.
 */
 
+/*drl*/
+static  constraintList fcnConstraints = NULL;
+
+//static  constraintList fcnPreConditions = NULL;
+
+
 static /*@only@*/ sRefSet fcnModifies = sRefSet_undefined;
 static /*@only@*/ /*@null@*/ specialClauses specClauses = specialClauses_undefined;
 static bool fcnNoGlobals = FALSE;
@@ -177,6 +183,12 @@ static void reflectModGlobs (uentry ue)
       fcnModifies = sRefSet_undefined;
     }
 
+  if (fcnConstraints)
+    {
+      uentry_setPreconditions (ue, fcnConstraints);
+      fcnConstraints = constraintList_undefined;
+    }
+
   if (uentry_isFunction (ue))
     {
       uentry_setSpecialClauses (ue, specClauses);
@@ -268,6 +280,17 @@ void setFunctionSpecialClause (lltok stok, sRefSet s,
   DPRINTF (("Added to specclauses: %s", specialClauses_unparse (specClauses)));
 }
 
+constraintList getFunctionConstraints (void)
+{
+  return constraintList_copy (fcnConstraints);
+}
+
+void setFunctionConstraints (constraintList c)
+{
+  #warning m leak
+  fcnConstraints = constraintList_copy (c);
+}
+
 void setFunctionModifies (sRefSet s)
 {
   sRefSet_free (fcnModifies);