]> andersk Git - splint.git/blobdiff - src/functionConstraint.c
Added mtgrammar.c.der
[splint.git] / src / functionConstraint.c
index d806132acdb7a9ca74b9c453b6d6d09109edcb3e..d6ce73274c4cf8e5fda42999ea35e308c8becc68 100644 (file)
@@ -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);
This page took 0.101532 seconds and 4 git commands to generate.