typedef enum
{
- LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE
+ LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE, CASTEQ
}
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; @*/
# define constraint_undefined ((constraint)NULL)
-extern /*@falsenull@*/ bool constraint_isDefined (constraint p_e) /*@*/ ;
-extern /*@unused@*/ /*@truenull@*/ bool constraint_isUndefined (constraint p_e) /*@*/ ;
-extern /*@truenull@*/ /*@unused@*/ bool constraint_isError (constraint p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool constraint_isDefined (constraint p_e) /*@*/ ;
+extern /*@unused@*/ /*@nullwhentrue@*/ bool constraint_isUndefined (constraint p_e) /*@*/ ;
+extern /*@nullwhentrue@*/ /*@unused@*/ bool constraint_isError (constraint p_e) /*@*/ ;
# define constraint_isDefined(e) ((e) != constraint_undefined)
# define constraint_isUndefined(e) ((e) == constraint_undefined)
/* 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 @*/;
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);
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*/
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);
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 */