Periodic commit

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

diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h
index 1cd0378be1d808dc9e1a90d1e25ecff73dfd30e8..89ae374a5a8d8d742c04b6c264ff4e30e8f0a27d 100644 (file)
--- a/src/Headers/constraint.h
+++ b/src/Headers/constraint.h
@@ -1,3 +1,10 @@
+typedef union constraintTermValue_
+{
+  exprNode expr;
+  sRef     sref;
+  int      intlit;
+} constraintTermValue;
+
 typedef enum
 {
   LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE
@@ -6,41 +13,110 @@ arithType;
 
 typedef enum
 {
- BUFFSIZE, STRINGLEN, VALUE
+ BUFFSIZE, STRINGLEN, VALUE, CALLSAFE,
+ MAXSET, MINSET, MAXREAD, MINREAD,
+ NULLTERMINATED,
+ INCOP,
+ UNDEFINED
 }
 constraintType;
 
-typedef struct constraint {
-  exprNode expr1;
-  exprNode expr2;
-  arithType restriction;
-  constraintType kind;  
-} constraint;
+typedef enum
+{
+  PLUS,
+  MINUS
+}
+constraintExprOp;
+
+
+typedef enum
+{
+EXPRNODE, SREF,
+INTLITERAL
+} constraintTermType;
 
 
-#define max_constraints 10
+struct _constraintTerm {
+  fileloc loc;
+  constraintTermValue value;
+  constraintTermType kind;
+};
 
-struct _constraintList {
-  constraint constraints[max_constraints];
-  int numconstraints;
+abst_typedef struct _constraintTerm * constraintTerm;
+
+struct constraintExpr_ {
+  constraintType c1;
+  constraintTerm t1;
+  constraintExprOp op;
+  struct constraintExpr_ * e1;
+};
+# define constraintExpr_undefined ((constraintExpr)NULL)
+
+typedef struct constraintExpr_ * constraintExpr;
+abst_typedef struct constr_ * constr;
+
+
+struct _constraint {
+  constraintType c1;
+  constraintTerm t1;
+  arithType       ar;
+  constraintExpr  e1;
+  bool post;
 } ;
 
-typedef struct _constraintList *constraintList;
-typedef struct _constraintList constraintList_;
+#define max_constraints 100
+
+//constraint constraint_create (exprNode e1, exprNode e2,  arithType restriction, constraintType kind);
+
+constraint constraint_createReadSafe (exprNode p_e1, exprNode p_e2);
+
+constraint constraint_makeInc_Op (exprNode p_e1);
+
+/*@i22*/
+/*@-czechfcns*/
+bool constraint_resolve (/*@unused@*/ constraint c);
+     
+/*@out@*/ constraintTerm new_constraintTermExpr (void);
+constraintTerm exprNode_makeConstraintTerm (/*@only@*/ exprNode e);
+
+constraintTerm intLit_makeConstraintTerm (int p_i);
+
+/*@special@*/ constraintExpr makeConstraintExpr (/*@only@*/ /*@notnull@*/ constraintTerm term)
+ /*@post:isnull result->e1@*/
+     /*@post:notnull result->t1@*/
+     /*@defines result->e1, result->t1, result->c1@, result->op*/;
+     
+constraintExpr makeConstraintExprIntlit (int p_i);
+
+/*@relnull@*/ constraint constraint_makeReadSafeExprNode ( exprNode p_po, exprNode p_ind);
+
+constraint constraint_makeWriteSafeExprNode (exprNode p_po, exprNode p_ind);
+
+constraint constraint_makeReadSafeInt (exprNode p_t1, int p_index);
+
+constraint constraint_makeEnsureMaxReadAtLeast (exprNode p_t1, exprNode p_t2, fileloc p_sequencePoint);
+
+constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, fileloc sequencePoint);
+
+constraint constraint_makeSideEffectPostIncrement (exprNode t1,  fileloc p_sequencePoint);
+void constraintType_print (constraintType c1);
+
+
+constraintExpr makePostOpInc (exprNode t1);
+
+
+
+void constraintTerm_print (constraintTerm term);
+
+void arithType_print (arithType ar);
+
+void constraintExpr_print (constraintExpr ex);
+
+void constraint_print (constraint c);
+/*@=czechfcns*/
+//#warning take this out
+#include "constraintList.h"
 
-/*@constant null constraintList constraintList_undefined; @*/
-# define constraintList_undefined      ((constraintList) NULL)
-# define constraintList_isDefined(s)   ((s) != constraintList_undefined)
-# define constraintList_isUndefined(s) ((s) == constraintList_undefined)
-//# define constraintList_isEmpty(s)     (constraint_size(s) == 0)
 
-constraintList constraintList_new ();
-constraintList constraintList_init (constraintList);
-constraintList constraintList_add (constraintList, constraint);
-constraintList constraintList_merge (constraintList, constraintList);
-constraintList constraintList_exprNodemerge (exprNode, exprNode);
 
-void constraintList_print (constraintList);
 
-constraint constraint_create (exprNode e1, exprNode e2,  arithType restriction, constraintType kind);
-extern  cstring exprNode_generateConstraints (exprNode e);