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