Added (limited) support for implicit annotations.

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

diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h
index 89ae374a5a8d8d742c04b6c264ff4e30e8f0a27d..58b8de6d665a0413c41eb46308aa5d1ebe8dfc23 100644 (file)
--- a/src/Headers/constraint.h
+++ b/src/Headers/constraint.h
@@ -1,9 +1,6 @@
-typedef union constraintTermValue_
-{
-  exprNode expr;
-  sRef     sref;
-  int      intlit;
-} constraintTermValue;
+#ifndef __constraint_h__
+
+#define __constraint_h__
 
 typedef enum
 {
@@ -11,63 +8,26 @@ typedef enum
 }
 arithType;
 
-typedef enum
-{
- BUFFSIZE, STRINGLEN, VALUE, CALLSAFE,
- MAXSET, MINSET, MAXREAD, MINREAD,
- NULLTERMINATED,
- INCOP,
- UNDEFINED
-}
-constraintType;
-
-typedef enum
-{
-  PLUS,
-  MINUS
-}
-constraintExprOp;
-
-
-typedef enum
-{
-EXPRNODE, SREF,
-INTLITERAL
-} constraintTermType;
-
-
-struct _constraintTerm {
-  fileloc loc;
-  constraintTermValue value;
-  constraintTermType kind;
-};
-
-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;
+//abst_typedef struct constr_ * constr;
 
 
 struct _constraint {
-  constraintType c1;
-  constraintTerm t1;
+  constraint     orig;
+  constraintExpr lexpr;
   arithType       ar;
-  constraintExpr  e1;
+  constraintExpr  expr;
   bool post;
+  exprNode generatingExpr;
 } ;
 
-#define max_constraints 100
+abst_typedef struct _constraintTerm * constraintTerm;
 
 //constraint constraint_create (exprNode e1, exprNode e2,  arithType restriction, constraintType kind);
 
+
+constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant);
+
+
 constraint constraint_createReadSafe (exprNode p_e1, exprNode p_e2);
 
 constraint constraint_makeInc_Op (exprNode p_e1);
@@ -77,14 +37,11 @@ constraint constraint_makeInc_Op (exprNode p_e1);
 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:isnull result->expr@*/
      /*@post:notnull result->t1@*/
-     /*@defines result->e1, result->t1, result->c1@, result->op*/;
+     /*@defines result->expr, result->t1, result->c1@, result->op*/;
      
 constraintExpr makeConstraintExprIntlit (int p_i);
 
@@ -99,24 +56,79 @@ constraint constraint_makeEnsureMaxReadAtLeast (exprNode p_t1, exprNode p_t2, fi
 constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, fileloc sequencePoint);
 
 constraint constraint_makeSideEffectPostIncrement (exprNode t1,  fileloc p_sequencePoint);
-void constraintType_print (constraintType c1);
-
+void constraint_overWrite (constraint c1, constraint c2);
+constraint constraint_copy (constraint c);
 
 constraintExpr makePostOpInc (exprNode t1);
 
 
+bool fileloc_closer (fileloc  loc1, fileloc  loc2, fileloc  loc3);
+
+
+cstring arithType_print (arithType ar) /*@*/;
+
+
+fileloc constraint_getFileloc (constraint c);
+cstring constraint_print (constraint c) /*@*/;
+constraint constraint_makeWriteSafeInt (exprNode po, int ind);
+
+exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src);
+
+constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
+
+constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint);
+
+/*@only@*/ constraint constraint_preserveOrig (/*@returned@*/ /*@only@*/ constraint c) /*@modifies c @*/;
+/*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
+                                                  exprNodeList arglist);
+
+cstring  constraint_printDetailed (constraint c);
+
+constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint);
 
-void constraintTerm_print (constraintTerm term);
+constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
+constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint);
+constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
+
+/*drl add 11/28/2000 */
+constraint constraint_makeSRefWriteSafeInt (sRef s, int ind);
+constraint constraint_makeSRefReadSafeInt (sRef s, int ind);
+/*drl add 11/26/2000 */
+void constraint_printError (constraint c, fileloc loc);
+constraint constraint_doSRefFixConstraintParam (constraint precondition,
+                                               exprNodeList arglist);
+
+constraint constraint_makeSRefSetBufferSize (sRef s, int size);
+
+constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall);
+
+constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer);
+
+constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint);
+bool constraint_search (constraint c, constraintExpr old);
+
+constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r);
+
+constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e);
+
+bool constraint_hasMaxSet(constraint c);
+
+/*from constraintGenreation.c*/
+bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv,  fileloc sequencePoint);
+
+constraintList exprNode_traversRequiresConstraints (exprNode e);
+constraintList exprNode_traversEnsuresConstraints (exprNode e);
 
-void arithType_print (arithType ar);
 
-void constraintExpr_print (constraintExpr ex);
 
-void constraint_print (constraint c);
 /*@=czechfcns*/
 //#warning take this out
 #include "constraintList.h"
 
+#include "constraintExpr.h"
+#include "constraintTerm.h"
+#include "constraintResolve.h"
+#include "constraintOutput.h"
 
-
+#endif