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 s_constraint {
  12   constraint     orig;
  13   constraint     or;
  14   bool           fcnPre;
  15   constraintExpr lexpr;
  16   arithType       ar;
  17   constraintExpr  expr;
  18   bool post;
  19   /*@observer@*/ /*@exposed@*/ /*@dependent@*/ exprNode generatingExpr;
  20 } ;
  21
  22 /*@constant null constraint constraint_undefined; @*/
  23
  24 # define constraint_undefined ((constraint)NULL)
  25
  26 extern /*@falsewhennull@*/ bool constraint_isDefined (constraint p_e) /*@*/ ;
  27 extern /*@unused@*/ /*@nullwhentrue@*/ bool constraint_isUndefined (constraint p_e) /*@*/ ;
  28 extern /*@nullwhentrue@*/ /*@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 extern void constraint_free (/*@only@*/  constraint p_c);
  35
  36 /* constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant); */
  37
  38 /*@i22*/
  39 /*@-czechfcns*/
  40
  41 extern constraint constraint_makeReadSafeExprNode ( /*@dependent@*/ /*@observer@*/ exprNode p_po, /*@dependent@*/ /*@observer@*/ exprNode p_ind);
  42
  43 extern /*@only@*/ constraint constraint_makeWriteSafeExprNode (/*@dependent@*/ /*@observer@*/ exprNode p_po, /*@dependent@*/ /*@observer@*/ exprNode p_ind);
  44
  45 extern /*@only@*/ constraint constraint_makeReadSafeInt (/*@dependent@*/ /*@observer@*/ exprNode p_t1, int p_index);
  46
  47 extern /*@only@*/ constraint constraint_makeEnsureMaxReadAtLeast (/*@dependent@*/ /*@observer@*/ exprNode p_t1, /*@dependent@*/ /*@observer@*/ exprNode p_t2, fileloc p_sequencePoint);
  48
  49 extern void constraint_overWrite (constraint p_c1, /*@observer@*/ constraint p_c2) /*@modifies p_c1 @*/;
  50
  51 extern /*@only@*/ constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint p_c);
  52
  53 extern bool fileloc_closer (/*@observer@*/ fileloc  p_loc1, /*@observer@*/ fileloc  p_loc2, /*@observer@*/ fileloc  p_loc3) /*@*/;
  54
  55 extern /*@only@*/ cstring arithType_print (arithType p_ar) /*@*/;
  56
  57 extern /*@only@*/ fileloc constraint_getFileloc (constraint p_c);
  58
  59 extern /*@only@*/ cstring constraint_unparse (/*@temp@*/ /*@observer@*/ constraint p_c) /*@*/;
  60 # define constraint_unparse constraint_print
  61
  62 extern /*@only@*/ cstring constraint_print (/*@temp@*/ /*@observer@*/ constraint p_c) /*@*/;
  63
  64 extern /*@only@*/ constraint constraint_makeWriteSafeInt (/*@dependent@*/ /*@observer@*/ exprNode p_po, int p_ind);
  65
  66 extern exprNode exprNode_copyConstraints (/*@returned@*/ exprNode p_dst, exprNode p_src) /*@modifies p_dst @*/;
  67
  68 extern /*@only@*/ constraint constraint_makeEnsureEqual (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
  69
  70 extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostIncrement (/*@dependent@*/ /*@observer@*/ exprNode p_e, fileloc p_sequencePoint);
  71
  72 extern constraint constraint_preserveOrig (/*@returned@*/ constraint p_c) /*@modifies p_c @*/;
  73 extern /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint p_precondition,
  74                                                             exprNodeList p_arglist);
  75 extern /*@only@*/ cstring  constraint_printDetailed (constraint p_c);
  76
  77 extern /*@only@*/ constraint constraint_makeEnsureLessThan (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
  78 extern /*@only@*/ constraint constraint_makeEnsureLessThanEqual (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
  79
  80 extern /*@only@*/ constraint constraint_makeEnsureGreaterThan (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
  81 extern /*@only@*/ constraint constraint_makeEnsureGreaterThanEqual (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
  82
  83 /*drl add 11/28/2000 */
  84 extern /*@only@*/ constraint constraint_makeSRefWriteSafeInt (sRef p_s, int p_ind);
  85 extern /*@unused@*/ /*@only@*/ constraint constraint_makeSRefReadSafeInt (sRef p_s, int p_ind);
  86 /*drl add 11/26/2000 */
  87 extern void constraint_printError (/*@observer@*/ /*@temp@*/ constraint p_c, /*@temp@*/ /*@observer@*/ fileloc p_loc);
  88
  89 extern /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint p_precondition,
  90         /*@temp@*/ /*@observer@*/ exprNodeList p_arglist);
  91
  92 extern /*@only@*/ constraint constraint_makeSRefSetBufferSize (sRef p_s, long int p_size);
  93
  94 extern /*@only@*/ constraint constraint_doFixResult (constraint p_postcondition, /*@dependent@*/ /*@observer@*/ exprNode p_fcnCall);
  95
  96 extern /*@only@*/ constraint constraint_makeEnsureLteMaxRead(/*@dependent@*/ /*@observer@*/ exprNode p_index, /*@dependent@*/ /*@observer@*/ exprNode p_buffer);
  97
  98 extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostDecrement (/*@dependent@*/ /*@observer@*/ exprNode p_e, fileloc p_sequencePoint);
  99
 100 extern bool constraint_search (constraint p_c, constraintExpr p_old);
 101
 102 extern /*@only@*/ constraint makeConstraintParse3 (constraintExpr p_l, lltok p_relOp, constraintExpr p_r);
 103
 104 extern constraint constraint_addGeneratingExpr (/*@returned@*/ constraint p_c, /*@dependent@*/ /*@exposed@*/ exprNode p_e);
 105
 106 extern bool constraint_hasMaxSet(constraint p_c);
 107
 108 /*from constraintGenreation.c*/
 109 extern void exprNode_exprTraverse (/*@dependent@*/  exprNode p_e, bool p_definatelv, bool p_definaterv, /*@temp@*/ /*@observer@*/ fileloc p_sequencePoint);
 110
 111 extern /*@only@*/ constraintList exprNode_traversRequiresConstraints (/*@dependent@*/ exprNode p_e);
 112 extern /*@only@*/ constraintList exprNode_traversEnsuresConstraints (/*@dependent@*/ exprNode p_e);
 113
 114 extern constraint constraint_togglePost (/*@returned@*/ constraint p_c);
 115 extern bool constraint_same (constraint p_c1, constraint p_c2) ;
 116
 117 /*@only@*/ cstring  constraint_printOr (constraint p_c) /*@*/;
 118 extern void constraint_printErrorPostCondition (constraint p_c, fileloc p_loc) ;
 119
 120 extern cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint p_c) /*@*/; /*drl add 8-11-001*/
 121
 122 extern constraint constraint_setFcnPre (/*@returned@*/ constraint p_c) ;
 123 extern constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint p_c, /*@dependent@*/ /*@observer@*/ exprNode p_e) ;
 124
 125 extern bool /*@alt void@*/ exprNode_generateConstraints (/*@dependent@*/ exprNode p_e) ;
 126 constraint constraint_togglePostOrig (/*@returned@*/ constraint p_c);
 127
 128 bool constraint_hasOrig( /*@observer@*/ /*@temp@*/ constraint p_c);
 129
 130 constraint constraint_makeAddAssign (/*@dependent@*/ /*@observer@*/ exprNode p_e, /*@dependent@*/ /*@observer@*/ exprNode p_f, fileloc p_sequencePoint);
 131
 132 constraint constraint_makeSubtractAssign (/*@dependent@*/ /*@observer@*/ exprNode p_e, /*@dependent@*/ /*@observer@*/ exprNode p_f, fileloc p_sequencePoint);
 133
 134 /*@only@*/ constraint constraint_undump (FILE * p_f);
 135
 136 void constraint_dump (/*@observer@*/ constraint p_c,  FILE * p_f);
 137
 138 extern void exprNode_forLoopHeuristics( /*@dependent@*/ exprNode p_e, /*@dependent@*/ exprNode p_forPred, /*@dependent@*/ exprNode p_forBody);
 139
 140 int constraint_compare (/*@observer@*/ /*@temp@*/ const constraint * p_c1, /*@observer@*/ /*@temp@*/ const constraint * p_c2) /*@*/;
 141
 142 bool constraint_isPost  (/*@observer@*/ /*@temp@*/ constraint p_c);
 143
 144 bool constraint_tooDeep (/*@observer@*/ /*@temp@*/ constraint p_c);
 145
 146 void exprNode_findValue( exprNode p_e);
 147
 148 /*@=czechfcns*/
 149 /* drl possible problem : warning take this out */
 150
 151 #include "constraintResolve.h"
 152 #include "constraintOutput.h"
 153
 154 #else
 155
 156 #error Multiple include
 157
 158 #endif
 159