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