]> andersk Git - splint.git/blobdiff - src/Headers/functionConstraint.h
*** empty log message ***
[splint.git] / src / Headers / functionConstraint.h
index b2d46192c6d1a549ab452d327e14107768da9ed4..a8cfc68de88201c4f528a21bf27ca697b26883dc 100644 (file)
@@ -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,6 +41,10 @@ extern functionConstraint
 functionConstraint_createMetaStateConstraint (/*@only@*/ metaStateConstraint) ;
 
 extern bool functionConstraint_hasBufferConstraint (functionConstraint) /*@*/ ;
+extern bool functionConstraint_hasMetaStateConstraint (functionConstraint) /*@*/ ;
+
+extern functionConstraint
+functionConstraint_conjoin (/*@only@*/ functionConstraint, /*@only@*/ functionConstraint) ;
 
 extern /*@observer@*/ constraintList functionConstraint_getBufferConstraint (functionConstraint) /*@*/ ;
 extern /*@observer@*/ metaStateConstraint functionConstraint_getMetaStateConstraint (functionConstraint) /*@*/ ;
This page took 0.119264 seconds and 4 git commands to generate.