X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/ba45e1e46d0f012cf3abdb631baa428f00a63378..8e37b772b38d8082ae5ccd4e6d74a8fe7271b705:/src/functionConstraint.c

diff --git a/src/functionConstraint.c b/src/functionConstraint.c
index d806132..d6ce732 100644
--- a/src/functionConstraint.c
+++ b/src/functionConstraint.c
@@ -27,7 +27,6 @@
 
 # include "lclintMacros.nf"
 # include "basic.h"
-# include "mtincludes.h"
 
 static /*@only@*/ /*@notnull@*/ /*@special@*/ functionConstraint  /*@i32 need special? @*/
 functionConstraint_alloc (functionConstraintKind kind) /*@defines result->kind@*/
@@ -86,46 +85,59 @@ extern functionConstraint functionConstraint_conjoin (functionConstraint f1, fun
     }
 }
 
-extern constraintList functionConstraint_getBufferConstraint (functionConstraint node)
+extern constraintList functionConstraint_getBufferConstraints (functionConstraint node)
 {
-  llassert (functionConstraint_isDefined (node));
-
-  if (node->kind == FCT_CONJUNCT)
+  if (functionConstraint_isDefined (node))
     {
-      if (functionConstraint_hasBufferConstraint (node->constraint.conjunct.op1))
+      if (node->kind == FCT_CONJUNCT)
 	{
-	  return functionConstraint_getBufferConstraint (node->constraint.conjunct.op1);
+	  return constraintList_addListFree (functionConstraint_getBufferConstraints (node->constraint.conjunct.op1),
+					     functionConstraint_getBufferConstraints (node->constraint.conjunct.op2));
 	}
       else
 	{
-	  llassert (functionConstraint_hasBufferConstraint (node->constraint.conjunct.op2));
-	  return functionConstraint_getBufferConstraint (node->constraint.conjunct.op2);
+	  if (node->kind == FCT_BUFFER)
+	    {
+	      return constraintList_copy (node->constraint.buffer);
+	    }
+	  else
+	    {
+	      return constraintList_undefined;
+	    }
 	}
     }
-
-  llassert (node->kind == FCT_BUFFER);
-  return node->constraint.buffer;
+  else
+    {
+      return constraintList_undefined;
+    }
 }
 
-extern metaStateConstraint functionConstraint_getMetaStateConstraint (functionConstraint node)
+extern metaStateConstraintList functionConstraint_getMetaStateConstraints (functionConstraint node)
 {
-  llassert (functionConstraint_isDefined (node));
-
-  if (node->kind == FCT_CONJUNCT)
+  if (functionConstraint_isDefined (node))
     {
-      if (functionConstraint_hasMetaStateConstraint (node->constraint.conjunct.op1))
+      if (node->kind == FCT_CONJUNCT)
 	{
-	  return functionConstraint_getMetaStateConstraint (node->constraint.conjunct.op1);
+	  return metaStateConstraintList_append 
+	    (functionConstraint_getMetaStateConstraints (node->constraint.conjunct.op1),
+	     functionConstraint_getMetaStateConstraints (node->constraint.conjunct.op2));
 	}
       else
 	{
-	  llassert (functionConstraint_hasMetaStateConstraint (node->constraint.conjunct.op2));
-	  return functionConstraint_getMetaStateConstraint (node->constraint.conjunct.op2);
+	  if (node->kind == FCT_METASTATE)
+	    {
+	      return metaStateConstraintList_single (node->constraint.metastate);
+	    }
+	  else
+	    {
+	      return metaStateConstraintList_undefined;
+	    }
 	}
     }
-
-  llassert (node->kind == FCT_METASTATE);
-  return node->constraint.metastate;
+  else
+    {
+      return metaStateConstraintList_undefined;
+    }
 }
 
 extern bool functionConstraint_hasBufferConstraint (functionConstraint node)
@@ -179,6 +191,8 @@ extern functionConstraint functionConstraint_copy (functionConstraint node)
     {
       return functionConstraint_undefined;
     }
+
+  BADBRANCHRET (functionConstraint_undefined);
 }
 
 extern void functionConstraint_free (/*@only@*/ functionConstraint node) 
@@ -196,7 +210,8 @@ extern void functionConstraint_free (/*@only@*/ functionConstraint node)
 	case FCT_CONJUNCT:
 	  functionConstraint_free (node->constraint.conjunct.op1);
 	  functionConstraint_free (node->constraint.conjunct.op2);
-	  BADDEFAULT;
+	  break;
+        BADDEFAULT;
 	}
       
       sfree (node);