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