*** empty log message ***

[splint.git] / src / Headers / functionConstraint.h

diff --git a/src/Headers/functionConstraint.h b/src/Headers/functionConstraint.h
index b2d46192c6d1a549ab452d327e14107768da9ed4..0a5dcf47763e577d6a183bfe4282901cc1df8325 100644 (file)
--- a/src/Headers/functionConstraint.h
+++ b/src/Headers/functionConstraint.h
@@ -11,7 +11,7 @@
 
 typedef enum
 {
-  FCT_BUFFER, FCT_METASTATE
+  FCT_BUFFER, FCT_METASTATE, FCT_CONJUNCT
 } functionConstraintKind ;
 
 struct s_functionConstraint {
@@ -19,6 +19,7 @@ struct s_functionConstraint {
   union {
     /*@only@*/ constraintList buffer;
     /*@only@*/ metaStateConstraint metastate;
+    struct { functionConstraint op1; functionConstraint op2; } conjunct;
   } constraint;
 } ;
 
@@ -40,9 +41,13 @@ extern functionConstraint
 functionConstraint_createMetaStateConstraint (/*@only@*/ metaStateConstraint) ;
 
 extern bool functionConstraint_hasBufferConstraint (functionConstraint) /*@*/ ;
+extern bool functionConstraint_hasMetaStateConstraint (functionConstraint) /*@*/ ;
 
-extern /*@observer@*/ constraintList functionConstraint_getBufferConstraint (functionConstraint) /*@*/ ;
-extern /*@observer@*/ metaStateConstraint functionConstraint_getMetaStateConstraint (functionConstraint) /*@*/ ;
+extern functionConstraint
+functionConstraint_conjoin (/*@only@*/ functionConstraint, /*@only@*/ functionConstraint) ;
+
+extern /*@only@*/ constraintList functionConstraint_getBufferConstraints (functionConstraint) /*@*/ ;
+extern /*@only@*/ metaStateConstraintList functionConstraint_getMetaStateConstraints (functionConstraint) /*@*/ ;
 
 extern cstring functionConstraint_unparse (functionConstraint) /*@*/ ;
 extern void functionConstraint_free (/*@only@*/ functionConstraint) ;