X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/86d93ed383c14be2a4548bd8ab98e4c1a79cb1f0..210066f9dd04de7d7d2f04d320b39a52f28b290b:/src/Headers/constraint.h?ds=sidebyside

diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h
index 39a1195..57676f4 100644
--- a/src/Headers/constraint.h
+++ b/src/Headers/constraint.h
@@ -4,19 +4,19 @@
 
 typedef enum
 {
-  LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE
+  LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE,
 }
 arithType;
 
 struct s_constraint {
-  constraint     orig;
-  constraint     or;
-  bool           fcnPre;
+  arithType ar;
+  constraint orig;
+  constraint or;
+  bool fcnPre;
   constraintExpr lexpr;
-  arithType       ar;
-  constraintExpr  expr;
+  constraintExpr expr;
   bool post;
-  /*@observer@*/ /*@exposed@*/ /*@dependent@*/ exprNode generatingExpr;
+  /*@exposed@*/ /*@dependent@*/ exprNode generatingExpr;
 } ;
 
 /*@constant null constraint constraint_undefined; @*/
@@ -35,33 +35,40 @@ extern void constraint_free (/*@only@*/  constraint p_c);
 
 /* constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant); */
 
-/*@i22*/
 /*@-czechfcns*/
 
-extern constraint constraint_makeReadSafeExprNode ( /*@dependent@*/ /*@observer@*/ exprNode p_po, /*@dependent@*/ /*@observer@*/ exprNode p_ind);
+extern constraint 
+constraint_makeReadSafeExprNode (/*@observer@*/ exprNode p_po,
+				 /*@observer@*/ exprNode p_ind);
 
-extern /*@only@*/ constraint constraint_makeWriteSafeExprNode (/*@dependent@*/ /*@observer@*/ exprNode p_po, /*@dependent@*/ /*@observer@*/ exprNode p_ind);
+extern /*@only@*/ constraint constraint_makeWriteSafeExprNode (/*@observer@*/ exprNode p_po, 
+							       /*@observer@*/ exprNode p_ind);
 
-extern /*@only@*/ constraint constraint_makeReadSafeInt (/*@dependent@*/ /*@observer@*/ exprNode p_t1, int p_index);
+extern /*@only@*/ constraint constraint_makeReadSafeInt (/*@observer@*/ exprNode p_t1, int p_index);
 
-extern /*@only@*/ constraint constraint_makeEnsureMaxReadAtLeast (/*@dependent@*/ /*@observer@*/ exprNode p_t1, /*@dependent@*/ /*@observer@*/ exprNode p_t2, fileloc p_sequencePoint);
+extern /*@only@*/ constraint
+constraint_makeEnsureMaxReadAtLeast (/*@observer@*/ exprNode p_t1, 
+				     /*@observer@*/ exprNode p_t2, fileloc p_sequencePoint);
 
-extern void constraint_overWrite (constraint p_c1, /*@observer@*/ constraint p_c2) /*@modifies p_c1 @*/;
+extern void constraint_overWrite (constraint p_c1, /*@observer@*/ constraint p_c2)
+     /*@modifies p_c1 @*/;
 
-extern /*@only@*/ constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint p_c);
+extern /*@only@*/ constraint constraint_copy (/*@temp@*/ constraint p_c);
 
-extern bool fileloc_closer (/*@observer@*/ fileloc  p_loc1, /*@observer@*/ fileloc  p_loc2, /*@observer@*/ fileloc  p_loc3) /*@*/;
+extern bool fileloc_closer (/*@observer@*/ fileloc  p_loc1,
+			    /*@observer@*/ fileloc  p_loc2,
+			    /*@observer@*/ fileloc  p_loc3) /*@*/;
 
 extern /*@only@*/ cstring arithType_print (arithType p_ar) /*@*/;
 
 extern /*@only@*/ fileloc constraint_getFileloc (constraint p_c);
 
-extern /*@only@*/ cstring constraint_unparse (/*@temp@*/ /*@observer@*/ constraint p_c) /*@*/;
-# define constraint_unparse constraint_print
+extern /*@only@*/ cstring constraint_unparse (/*@temp@*/ constraint p_c) /*@*/;
+extern /*@only@*/ cstring constraint_unparseOr (/*@temp@*/ constraint p_c) /*@*/ ;
+extern /*@only@*/ cstring constraint_unparseDetailed (constraint p_c) /*@*/ ;
 
-extern /*@only@*/ cstring constraint_print (/*@temp@*/ /*@observer@*/ constraint p_c) /*@*/;
-
-extern /*@only@*/ constraint constraint_makeWriteSafeInt (/*@dependent@*/ /*@observer@*/ exprNode p_po, int p_ind);
+extern /*@only@*/ constraint 
+constraint_makeWriteSafeInt (/*@dependent@*/ /*@observer@*/ exprNode p_po, int p_ind);
 
 extern exprNode exprNode_copyConstraints (/*@returned@*/ exprNode p_dst, exprNode p_src) /*@modifies p_dst @*/;
 
@@ -72,8 +79,6 @@ extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostIncrement (/*@de
 extern constraint constraint_preserveOrig (/*@returned@*/ constraint p_c) /*@modifies p_c @*/;
 extern /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint p_precondition,
 							    exprNodeList p_arglist);
-extern /*@only@*/ cstring  constraint_printDetailed (constraint p_c);
-
 extern /*@only@*/ constraint constraint_makeEnsureLessThan (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
 extern /*@only@*/ constraint constraint_makeEnsureLessThanEqual (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
 
@@ -106,15 +111,16 @@ extern constraint constraint_addGeneratingExpr (/*@returned@*/ constraint p_c, /
 extern bool constraint_hasMaxSet(constraint p_c);
 
 /*from constraintGenreation.c*/
-extern void exprNode_exprTraverse (/*@dependent@*/  exprNode p_e, bool p_definatelv, bool p_definaterv, /*@temp@*/ /*@observer@*/ fileloc p_sequencePoint);
+extern void exprNode_exprTraverse (exprNode p_e, bool p_definatelv, bool p_definaterv, /*@temp@*/ /*@observer@*/ fileloc p_sequencePoint);
+
+extern /*@only@*/ constraintList 
+exprNode_traverseRequiresConstraints (exprNode p_e);
 
-extern /*@only@*/ constraintList exprNode_traversRequiresConstraints (/*@dependent@*/ exprNode p_e);
-extern /*@only@*/ constraintList exprNode_traversEnsuresConstraints (/*@dependent@*/ exprNode p_e);
+extern /*@only@*/ constraintList 
+exprNode_traverseEnsuresConstraints (exprNode p_e);
 
 extern constraint constraint_togglePost (/*@returned@*/ constraint p_c);
 extern bool constraint_same (constraint p_c1, constraint p_c2) ;
-
-/*@only@*/ cstring  constraint_printOr (constraint p_c) /*@*/;
 extern void constraint_printErrorPostCondition (constraint p_c, fileloc p_loc) ;
 
 extern cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint p_c) /*@*/; /*drl add 8-11-001*/
@@ -122,7 +128,7 @@ extern cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint p_
 extern constraint constraint_setFcnPre (/*@returned@*/ constraint p_c) ;
 extern constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint p_c, /*@dependent@*/ /*@observer@*/ exprNode p_e) ;
 
-extern bool /*@alt void@*/ exprNode_generateConstraints (/*@dependent@*/ exprNode p_e) ;
+extern bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode p_e) ;
 constraint constraint_togglePostOrig (/*@returned@*/ constraint p_c);
 
 bool constraint_hasOrig( /*@observer@*/ /*@temp@*/ constraint p_c);
@@ -148,7 +154,9 @@ void exprNode_findValue( exprNode p_e);
 /*drl 1/6/2001: I didn't think these functions were solid enough to include in the   stable  release of splint.*/
 /*drl added 12/30/01 */
 /* extern / *@only@* / constraint  constraint_doSRefFixInvarConstraint(constraint p_invar, sRef p_s, ctype p_ct ); */
-     
+
+/*drl added 12/19 */
+bool constraint_isConstantOnly (constraint p_c);
 /*@=czechfcns*/
 /* drl possible problem : warning take this out */