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