src/Headers/constraint.h

   1 #ifndef __constraint_h__
   2
   3 #define __constraint_h__
   4
   5 typedef enum
   6 {
   7   LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE
   8 }
   9 arithType;
  10
  11 struct _constraint {
  12   constraint     orig;
  13   constraint     or;
  14   bool           fcnPre;
  15   constraintExpr lexpr;
  16   arithType       ar;
  17   constraintExpr  expr;
  18   bool post;
  19   /*@kept@*/ exprNode generatingExpr;
  20 } ;
  21
  22 /*@constant null constraint constraint_undefined; @*/
  23
  24 # define constraint_undefined ((constraint)NULL)
  25
  26 extern /*@falsenull@*/ bool constraint_isDefined (constraint p_e) /*@*/ ;
  27 extern /*@unused@*/ /*@truenull@*/ bool constraint_isUndefined (constraint p_e) /*@*/ ;
  28 extern /*@truenull@*/ /*@unused@*/ bool constraint_isError (constraint p_e) /*@*/ ;
  29
  30 # define constraint_isDefined(e)        ((e) != constraint_undefined)
  31 # define constraint_isUndefined(e)      ((e) == constraint_undefined)
  32 # define constraint_isError(e)          ((e) == constraint_undefined)
  33
  34 void constraint_free (/*@only@*/ /*@notnull@*/ constraint c);
  35
  36 //constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant);
  37
  38 /*@i22*/
  39 /*@-czechfcns*/
  40
  41 ///*@special@*/ constraintExpr makeConstraintExpr (/*@only@*/ /*@notnull@*/ constraintTerm term)
  42 // /*@post:isnull result->expr@*/
  43 //     /*@post:notnull result->t1@*/
  44 //     /*@defines result->expr, result->t1, result->c1@, result->op*/;
  45
  46 //constraintExpr makeConstraintExprIntlit (int p_i);
  47
  48 /*@relnull@*/ constraint constraint_makeReadSafeExprNode ( exprNode p_po, exprNode p_ind);
  49
  50 /*@only@*/ constraint constraint_makeWriteSafeExprNode (exprNode p_po, exprNode p_ind);
  51
  52 /*@only@*/ constraint constraint_makeReadSafeInt (exprNode p_t1, int p_index);
  53
  54 /*@only@*/ constraint constraint_makeEnsureMaxReadAtLeast (exprNode p_t1, exprNode p_t2, fileloc p_sequencePoint);
  55
  56 void constraint_overWrite (constraint c1, /*@observer@*/ constraint c2) /*@modifies c1 @*/;
  57
  58 /*@only@*/ constraint constraint_copy (/*@observer@*/ constraint c);
  59
  60 //constraintExpr makePostOpInc (exprNode t1);
  61
  62
  63 bool fileloc_closer (/*@observer@*/ fileloc  loc1,/*@observer@*/ fileloc  loc2,/*@observer@*/ fileloc  loc3) /*@*/;
  64
  65
  66 /*@only@*/ cstring arithType_print (arithType ar) /*@*/;
  67
  68
  69 /*@only@*/fileloc constraint_getFileloc (constraint c);
  70 /*@only@*/ cstring constraint_print (constraint c) /*@*/;
  71
  72 /*@only@*/constraint constraint_makeWriteSafeInt (exprNode po, int ind);
  73
  74 exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src) /*@modifies dst @*/;
  75
  76 /*@only@*/ constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
  77
  78 /*@only@*/ constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint);
  79
  80 constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/;
  81 /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
  82                                                      exprNodeList arglist);
  83
  84 /*@only@*/ cstring  constraint_printDetailed (constraint c);
  85
  86 /*@only@*/ constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint);
  87
  88 /*@only@*/ constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
  89
  90 /*@only@*/ constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint);
  91 /*@only@*/ constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
  92
  93 /*drl add 11/28/2000 */
  94 /*@only@*/ constraint constraint_makeSRefWriteSafeInt (sRef s, int ind);
  95 /*@unused@*/ /*@only@*/ constraint constraint_makeSRefReadSafeInt (sRef s, int ind);
  96 /*drl add 11/26/2000 */
  97 void constraint_printError (/*@observer@*/ constraint c, /*@observer@*/ fileloc loc);
  98
  99 /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition,
 100                                                 exprNodeList arglist);
 101
 102 /*@only@*/ constraint constraint_makeSRefSetBufferSize (sRef s, long int size);
 103
 104 /*@only@*/ constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall);
 105
 106 /*@only@*/ constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer);
 107
 108 /*@only@*/ constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint);
 109
 110 bool constraint_search (constraint c, constraintExpr old);
 111
 112 /*@only@*/ constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r);
 113
 114 constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e);
 115
 116 bool constraint_hasMaxSet(constraint c);
 117
 118 /*from constraintGenreation.c*/
 119 void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@observer@*/  fileloc sequencePoint);
 120
 121 /*@only@*/ constraintList exprNode_traversRequiresConstraints (exprNode e);
 122 /*@only@*/ constraintList exprNode_traversEnsuresConstraints (exprNode e);
 123
 124 constraint constraint_togglePost (/*@returned@*/ constraint c);
 125
 126 /*@only@*/ cstring  constraint_printOr (constraint c) /*@*/;
 127
 128 /*@=czechfcns*/
 129 //#warning take this out
 130
 131 #include "constraintResolve.h"
 132 #include "constraintOutput.h"
 133
 134 #else
 135
 136 #error Multiple include
 137
 138 #endif
 139