src/constraint.c

   1 /*
   2 ** constraintList.c
   3 */
   4
   5 //#define DEBUGPRINT 1
   6
   7 # include <ctype.h> /* for isdigit */
   8 # include "lclintMacros.nf"
   9 # include "basic.h"
  10 # include "cgrammar.h"
  11 # include "cgrammar_tokens.h"
  12
  13 # include "exprChecks.h"
  14 # include "aliasChecks.h"
  15 # include "exprNodeSList.h"
  16 //# include "exprData.i"
  17
  18 /*@i33*/
  19 /*@-fcnuse*/
  20 /*@-assignexpose*/
  21
  22 /*@access exprNode @*/
  23
  24 constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant)
  25
  26 {
  27   char *t;
  28   int c;
  29   constraint ret;
  30   ret = constraint_makeNew();
  31   llassert (sRef_isValid(x) );
  32   if (!sRef_isValid(x))
  33     return ret;
  34
  35
  36   ret->lexpr = constraintExpr_makeTermsRef (x);
  37   #warning fix abstraction
  38
  39   if (relOp.tok == GE_OP)
  40       ret->ar = GTE;
  41   else if (relOp.tok == LE_OP)
  42     ret->ar = LTE;
  43   else if (relOp.tok == EQ_OP)
  44     ret->ar = EQ;
  45   else
  46     llfatalbug(message ("Unsupported relational operator") );
  47
  48
  49   t =  cstring_toCharsSafe (exprNode_unparse(cconstant));
  50   c = atoi( t );
  51   ret->expr = constraintExpr_makeIntLiteral (c);
  52
  53   ret->post = TRUE;
  54   //  ret->orig = ret;
  55   DPRINTF(("GENERATED CONSTRAINT:"));
  56   DPRINTF( (message ("%s", constraint_print(ret) ) ) );
  57   return ret;
  58 }
  59
  60 constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
  61
  62 {
  63   char *t;
  64   int c;
  65   constraint ret;
  66   ret = constraint_makeNew();
  67   llassert (l!=NULL);
  68   if (!l)
  69     return ret;
  70
  71
  72   ret->lexpr = constraintExpr_copy (l);
  73   #warning fix abstraction
  74
  75   if (relOp.tok == GE_OP)
  76       ret->ar = GTE;
  77   else if (relOp.tok == LE_OP)
  78     ret->ar = LTE;
  79   else if (relOp.tok == EQ_OP)
  80     ret->ar = EQ;
  81   else
  82   llfatalbug(message("Unsupported relational operator") );
  83
  84
  85   t =  cstring_toCharsSafe (exprNode_unparse(cconstant));
  86   c = atoi( t );
  87   ret->expr = constraintExpr_makeIntLiteral (c);
  88
  89   ret->post = TRUE;
  90   //  ret->orig = ret;
  91   DPRINTF(("GENERATED CONSTRAINT:"));
  92   DPRINTF( (message ("%s", constraint_print(ret) ) ) );
  93   return ret;
  94 }
  95
  96 bool constraint_same (constraint c1, constraint c2)
  97 {
  98
  99   if (c1->ar != c2->ar)
 100     return FALSE;
 101
 102   if (!constraintExpr_similar (c1->lexpr, c2->lexpr) )
 103     return FALSE;
 104
 105   if (!constraintExpr_similar (c1->expr, c2->expr) )
 106     return FALSE;
 107
 108   return TRUE;
 109 }
 110
 111 constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)
 112 {
 113   constraint ret;
 114   ret = constraint_makeNew();
 115   llassert (l !=NULL);
 116   if (!l)
 117     return ret;
 118
 119
 120   ret->lexpr = constraintExpr_copy (l);
 121   #warning fix abstraction
 122
 123   if (relOp.tok == GE_OP)
 124       ret->ar = GTE;
 125   else if (relOp.tok == LE_OP)
 126     ret->ar = LTE;
 127   else if (relOp.tok == EQ_OP)
 128     ret->ar = EQ;
 129   else
 130   llfatalbug( message("Unsupported relational operator") );
 131
 132   ret->expr = constraintExpr_copy (r);
 133
 134   ret->post = TRUE;
 135
 136   ret->orig = constraint_copy(ret);
 137
 138   ret = constraint_simplify (ret);
 139
 140   //  ret->orig = ret;
 141   DPRINTF(("GENERATED CONSTRAINT:"));
 142   DPRINTF( (message ("%s", constraint_print(ret) ) ) );
 143   return ret;
 144 }
 145
 146 constraint constraint_copy (constraint c)
 147 {
 148   constraint ret;
 149
 150   llassert (constraint_isDefined(c) );
 151
 152   ret = constraint_makeNew();
 153   ret->lexpr = constraintExpr_copy (c->lexpr);
 154   ret->ar = c->ar;
 155   ret->expr =  constraintExpr_copy (c->expr);
 156   ret->post = c->post;
 157   ret->generatingExpr = exprNode_fakeCopy(c->generatingExpr);
 158
 159   /*@i33 fix this*/
 160   if (c->orig != NULL)
 161     ret->orig = constraint_copy (c->orig);
 162   else
 163     ret->orig = NULL;
 164
 165   if (c->or != NULL)
 166     ret->or = constraint_copy (c->or);
 167   else
 168     ret->or = NULL;
 169
 170   return ret;
 171 }
 172
 173 /*like copy expect it doesn't allocate memory for the constraint*/
 174
 175 void constraint_overWrite (constraint c1, constraint c2)
 176 {
 177   c1->lexpr = constraintExpr_copy (c2->lexpr);
 178   c1->ar = c2->ar;
 179   c1->expr =  constraintExpr_copy (c2->expr);
 180   c1->post = c2->post;
 181   /*@i33 fix this*/
 182   if (c2->orig != NULL)
 183     c1->orig = constraint_copy (c2->orig);
 184   else
 185     c1->orig = NULL;
 186
 187   if (c2->or != NULL)
 188     c1->or = constraint_copy (c2->or);
 189   else
 190     c1->or = NULL;
 191
 192   c1->generatingExpr = exprNode_fakeCopy (c2->generatingExpr );
 193 }
 194
 195 bool constraint_resolve (/*@unused@*/ constraint c)
 196 {
 197   return FALSE;
 198 }
 199
 200
 201
 202 /*@notnull@*/ constraint constraint_makeNew (void)
 203 {
 204   constraint ret;
 205   ret = dmalloc(sizeof (*ret) );
 206   ret->lexpr = NULL;
 207   ret->expr = NULL;
 208   ret->ar = LT;
 209   ret->post = FALSE;
 210   ret->orig = NULL;
 211   ret->or = NULL;
 212   ret->generatingExpr = NULL;
 213   return ret;
 214 }
 215
 216 constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
 217 {
 218
 219   if (c->generatingExpr == NULL)
 220     {
 221       c->generatingExpr = exprNode_fakeCopy(e);
 222       DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
 223     }
 224   else
 225     {
 226       DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
 227     }
 228   return c;
 229 }
 230
 231 fileloc constraint_getFileloc (constraint c)
 232 {
 233   if (exprNode_isDefined(c->generatingExpr) )
 234     return (exprNode_getfileloc (c->generatingExpr) );
 235
 236   return (constraintExpr_getFileloc (c->lexpr) );
 237
 238
 239 }
 240
 241 static bool checkForMaxSet (constraint c)
 242 {
 243   if (constraintExpr_hasMaxSet(c->lexpr) || constraintExpr_hasMaxSet(c->expr) )
 244     return TRUE;
 245
 246   return FALSE;
 247 }
 248
 249 bool constraint_hasMaxSet(constraint c)
 250 {
 251   if (c->orig != NULL)
 252     {
 253       if (checkForMaxSet(c->orig) )
 254         return TRUE;
 255     }
 256
 257   return (checkForMaxSet(c) );
 258 }
 259
 260 constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
 261 {
 262   constraint ret = constraint_makeNew();
 263   //  constraintTerm term;
 264   po = exprNode_fakeCopy(po);
 265   ind = exprNode_fakeCopy(ind);
 266   ret->lexpr = constraintExpr_makeMaxReadExpr(po);
 267   ret->ar    = GTE;
 268   ret->expr  = constraintExpr_makeValueExpr (ind);
 269   return ret;
 270 }
 271
 272 constraint constraint_makeWriteSafeInt (exprNode po, int ind)
 273 {
 274   constraint ret = constraint_makeNew();
 275
 276
 277   ret->lexpr =constraintExpr_makeMaxSetExpr(po);
 278   ret->ar = GTE;
 279   ret->expr =  constraintExpr_makeIntLiteral (ind);
 280   /*@i1*/return ret;
 281 }
 282
 283 constraint constraint_makeSRefSetBufferSize (sRef s, int size)
 284 {
 285  constraint ret = constraint_makeNew();
 286  ret->lexpr = constraintExpr_makeSRefMaxset (s);
 287  ret->ar = EQ;
 288  ret->expr =  constraintExpr_makeIntLiteral (size);
 289  ret->post = TRUE;
 290  /*@i1*/return ret;
 291 }
 292
 293 constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
 294 {
 295   constraint ret = constraint_makeNew();
 296
 297
 298   ret->lexpr = constraintExpr_makeSRefMaxset (s);
 299   ret->ar = GTE;
 300   ret->expr =  constraintExpr_makeIntLiteral (ind);
 301   ret->post = TRUE;
 302   /*@i1*/return ret;
 303 }
 304
 305 /* drl added 01/12/2000
 306
 307   makes the constraint: Ensures index <= MaxRead(buffer) */
 308
 309 constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer)
 310 {
 311   constraint ret = constraint_makeNew();
 312
 313   ret->lexpr = constraintExpr_makeValueExpr (index);
 314   ret->ar = LTE;
 315   ret->expr = constraintExpr_makeMaxReadExpr(buffer);
 316   ret->post = TRUE;
 317   return ret;
 318 }
 319
 320 constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
 321 {
 322   constraint ret = constraint_makeNew();
 323
 324
 325   ret->lexpr =constraintExpr_makeMaxSetExpr(po);
 326   ret->ar = GTE;
 327   ret->expr =  constraintExpr_makeValueExpr (ind);
 328   /*@i1*/return ret;
 329 }
 330
 331
 332 constraint constraint_makeReadSafeInt ( exprNode po, int ind)
 333 {
 334   constraint ret = constraint_makeNew();
 335
 336   po = exprNode_fakeCopy(po);
 337
 338   ret->lexpr = constraintExpr_makeMaxReadExpr(po);
 339   ret->ar    = GTE;
 340   ret->expr  = constraintExpr_makeIntLiteral (ind);
 341   return ret;
 342 }
 343
 344 constraint constraint_makeSRefReadSafeInt (sRef s, int ind)
 345 {
 346   constraint ret = constraint_makeNew();
 347
 348
 349   ret->lexpr = constraintExpr_makeSRefMaxRead (s);
 350   ret->ar = GTE;
 351   ret->expr =  constraintExpr_makeIntLiteral (ind);
 352   ret->post = TRUE;
 353   /*@i1*/return ret;
 354 }
 355
 356 constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
 357 {
 358   constraint ret = constraint_makeNew();
 359
 360
 361   e1 = exprNode_fakeCopy (e1);
 362   t2 = exprNode_fakeCopy (t2);
 363
 364   ret = constraint_makeReadSafeExprNode(e1, t2);
 365
 366   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 367
 368   ret->post = TRUE;
 369
 370   //  fileloc_incColumn (ret->lexpr->term->loc);
 371   return ret;
 372 }
 373
 374 static constraint constraint_makeEnsuresOpConstraintExpr (constraintExpr c1, constraintExpr c2, fileloc sequencePoint,  arithType  ar)
 375 {
 376
 377   constraint ret;
 378
 379   llassert(c1 && c2);
 380   //  llassert(sequencePoint);
 381
 382   ret = constraint_makeNew();
 383
 384   ret->lexpr = c1;
 385   ret->ar = ar;
 386   ret->post = TRUE;
 387   ret->expr =  c2;
 388   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 389   return ret;
 390 }
 391
 392 static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint,  arithType  ar)
 393 {
 394   constraintExpr c1, c2;
 395   constraint ret;
 396   exprNode e;
 397
 398   if (! (e1 && e2) )
 399     {
 400       llcontbug((message("null exprNode, Exprnodes are %s and %s",
 401                        exprNode_unparse(e1), exprNode_unparse(e2) )
 402                ));
 403     }
 404
 405   //  llassert (sequencePoint);
 406
 407   e  =  exprNode_fakeCopy(e1);
 408   c1 =  constraintExpr_makeValueExpr (e);
 409
 410   e  =  exprNode_fakeCopy(e2);
 411   c2 =  constraintExpr_makeValueExpr (e);
 412
 413   ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
 414
 415   return ret;
 416 }
 417
 418
 419 /* make constraint ensures e1 == e2 */
 420
 421 constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 422 {
 423   return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) );
 424 }
 425
 426 /*make constraint ensures e1 < e2 */
 427 constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 428 {
 429   constraintExpr t1, t2;
 430
 431   t1 = constraintExpr_makeValueExpr (e1);
 432   t2 = constraintExpr_makeValueExpr (e2);
 433
 434   /*change this to e1 <= (e2 -1) */
 435
 436   t2 = constraintExpr_makeDecConstraintExpr (t2);
 437
 438  return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE) );
 439 }
 440
 441 constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 442 {
 443  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) );
 444 }
 445
 446 constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 447 {
 448   constraintExpr t1, t2;
 449
 450   t1 = constraintExpr_makeValueExpr (e1);
 451   t2 = constraintExpr_makeValueExpr (e2);
 452
 453
 454   /* change this to e1 >= (e2 + 1) */
 455   t2 = constraintExpr_makeIncConstraintExpr (t2);
 456
 457
 458  return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE) );
 459 }
 460
 461 constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 462 {
 463  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) );
 464 }
 465
 466
 467 exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
 468 {
 469   dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
 470   dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
 471   dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
 472   dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints );
 473   return dst;
 474 }
 475
 476 constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
 477 {
 478   constraint ret = constraint_makeNew();
 479   //constraintTerm term;
 480
 481   e = exprNode_fakeCopy(e);
 482   ret->lexpr = constraintExpr_makeValueExpr (e);
 483   ret->ar = EQ;
 484   ret->post = TRUE;
 485   ret->expr =  constraintExpr_makeValueExpr (e);
 486   ret->expr =  constraintExpr_makeDecConstraintExpr (ret->expr);
 487
 488   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 489 //   fileloc_incColumn (  ret->lexpr->term->loc);
 490 //   fileloc_incColumn (  ret->lexpr->term->loc);
 491   return ret;
 492 }
 493 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 494 {
 495   constraint ret = constraint_makeNew();
 496   //constraintTerm term;
 497
 498   e = exprNode_fakeCopy(e);
 499   ret->lexpr = constraintExpr_makeValueExpr (e);
 500   ret->ar = EQ;
 501   ret->post = TRUE;
 502   ret->expr =  constraintExpr_makeValueExpr (e);
 503   ret->expr =  constraintExpr_makeIncConstraintExpr (ret->expr);
 504
 505   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 506 //   fileloc_incColumn (  ret->lexpr->term->loc);
 507 //   fileloc_incColumn (  ret->lexpr->term->loc);
 508   return ret;
 509 }
 510
 511
 512
 513 // constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 514 // {
 515 //   constraint ret = constraint_makeNew();
 516 //   //constraintTerm term;
 517
 518 //   e = exprNode_fakeCopy(e);
 519 //   ret->lexpr = constraintExpr_makeMaxReadExpr(e);
 520 //   ret->ar = EQ;
 521 //   ret->post = TRUE;
 522 //   ret->expr = constraintExpr_makeIncConstraintExpr (e);
 523 //   ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint);
 524 //   return ret;
 525 // }
 526
 527
 528 cstring arithType_print (arithType ar) /*@*/
 529 {
 530   cstring st = cstring_undefined;
 531   switch (ar)
 532     {
 533     case LT:
 534       st = cstring_makeLiteral (" < ");
 535       break;
 536     case        LTE:
 537       st = cstring_makeLiteral (" <= ");
 538       break;
 539     case        GT:
 540       st = cstring_makeLiteral (" > ");
 541       break;
 542     case        GTE:
 543       st = cstring_makeLiteral (" >= ");
 544       break;
 545     case        EQ:
 546       st = cstring_makeLiteral (" == ");
 547       break;
 548     case        NONNEGATIVE:
 549       st = cstring_makeLiteral (" NONNEGATIVE ");
 550       break;
 551     case        POSITIVE:
 552       st = cstring_makeLiteral (" POSITIVE ");
 553       break;
 554     default:
 555       llassert(FALSE);
 556       break;
 557     }
 558   return st;
 559 }
 560
 561 void constraint_printError (constraint c, fileloc loc)
 562 {
 563   cstring string;
 564   fileloc errorLoc;
 565
 566   string = constraint_printDetailed (c);
 567
 568   errorLoc = loc;
 569
 570   if (constraint_getFileloc(c) )
 571     /*@-branchstate@*/
 572       errorLoc = constraint_getFileloc(c);
 573   /*@=branchstate@*/
 574
 575   if (c->post)
 576     {
 577        voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
 578     }
 579   else
 580     {
 581       voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
 582     }
 583
 584 }
 585
 586 cstring  constraint_printDetailed (constraint c)
 587 {
 588   cstring st = cstring_undefined;
 589
 590
 591   if (!c->post)
 592     {
 593     if (c->orig != NULL)
 594       st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisfy %s", constraint_print (c), constraint_print(c->orig) );
 595     else
 596       st = message ("Unresolved constraint:\nLclint is unable to resolve %s", constraint_print (c));
 597
 598     }
 599   else
 600     {
 601       if (c->orig != NULL)
 602         st = message ("Block Post condition:\nThis function block has the post condition %s\n based on %s", constraint_print (c), constraint_print(c->orig) );
 603       else
 604         st = message ("Block Post condition:\nThis function block has the post condition %s", constraint_print (c));
 605     }
 606
 607   if (context_getFlag (FLG_CONSTRAINTLOCATION) )
 608     {
 609       cstring temp;
 610       // llassert (c->generatingExpr);
 611       temp = message ("\nOriginal Generating expression %s: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
 612                       exprNode_unparse(c->generatingExpr) );
 613       st = cstring_concat (st, temp);
 614
 615       if (constraint_hasMaxSet(c) )
 616         {
 617           cstring temp2;
 618           temp2 = message ("\nHas MaxSet\n");
 619           st = cstring_concat (st, temp2);
 620         }
 621     }
 622   return st;
 623 }
 624
 625 cstring  constraint_print (constraint c) /*@*/
 626 {
 627   cstring st = cstring_undefined;
 628   cstring type = cstring_undefined;
 629   llassert (c !=NULL);
 630   if (c->post)
 631     {
 632       type = cstring_makeLiteral ("Ensures: ");
 633     }
 634   else
 635     {
 636       type = cstring_makeLiteral ("Requires: ");
 637     }
 638   st = message ("%s: %s %s %s",
 639                 type,
 640                 constraintExpr_print (c->lexpr),
 641                 arithType_print(c->ar),
 642                 constraintExpr_print(c->expr)
 643                 );
 644   return st;
 645 }
 646
 647 cstring  constraint_printOr (constraint c) /*@*/
 648 {
 649   cstring ret;
 650   constraint temp;
 651
 652   ret = cstring_undefined;
 653   temp = c;
 654
 655   ret = cstring_concat (ret, constraint_print(temp) );
 656
 657   temp = temp->or;
 658
 659   while ( constraint_isDefined(temp) )
 660     {
 661       ret = cstring_concat (ret, cstring_makeLiteral (" OR ") );
 662       ret = cstring_concat (ret, constraint_print(temp) );
 663       temp = temp->or;
 664     }
 665
 666   return ret;
 667
 668 }
 669
 670 /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
 671                                                    exprNodeList arglist)
 672 {
 673   precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
 674                                                            arglist);
 675   precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
 676                                                            arglist);
 677
 678   return precondition;
 679 }
 680
 681
 682 constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall)
 683 {
 684   postcondition = constraint_copy (postcondition);
 685   postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
 686   postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
 687
 688   return postcondition;
 689 }
 690
 691 constraint constraint_doSRefFixConstraintParam (constraint precondition,
 692                                                    exprNodeList arglist)
 693 {
 694
 695   precondition = constraint_copy (precondition);
 696   precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
 697   precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
 698
 699   return precondition;
 700 }
 701
 702 // bool constraint_hasTerm (constraint c, constraintTerm term)
 703 // {
 704 //   DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );
 705
 706 //   if (constraintExpr_includesTerm (c->lexpr, term) )
 707 //     return TRUE;
 708
 709 //   if (constraintExpr_includesTerm (c->expr, term) )
 710 //     return TRUE;
 711
 712 //   return FALSE;
 713 // }
 714
 715 /*@only@*/ constraint constraint_preserveOrig (/*@returned@*/ /*@only@*/ constraint c) /*@modifies c @*/
 716 {
 717   c->orig = constraint_copy (c);
 718   return c;
 719 }
 720 /*@=fcnuse*/
 721 /*@=assignexpose*/
 722 /*@=czechfcns@*/