src/constraint.c

   1 /*
   2 ** constraint.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
  25 static /*@notnull@*/  /*@special@*/ constraint constraint_makeNew (void)
  26      /*@post:isnull result->or, result->orig,  result->generatingExpr, result->fcnPre @*/ /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/;
  27
  28 /*  constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant) */
  29
  30 /*  { */
  31 /*    char *t; */
  32 /*    int c; */
  33 /*    constraint ret; */
  34 /*    ret = constraint_makeNew(); */
  35 /*    llassert (sRef_isValid(x) ); */
  36 /*    if (!sRef_isValid(x)) */
  37 /*      return ret; */
  38
  39
  40 /*    ret->lexpr = constraintExpr_makeTermsRef (x); */
  41 /*    #warning fix abstraction */
  42
  43 /*    if (relOp.tok == GE_OP) */
  44 /*        ret->ar = GTE; */
  45 /*    else if (relOp.tok == LE_OP) */
  46 /*      ret->ar = LTE; */
  47 /*    else if (relOp.tok == EQ_OP) */
  48 /*      ret->ar = EQ; */
  49 /*    else */
  50 /*      llfatalbug(message ("Unsupported relational operator") ); */
  51
  52
  53 /*    t =  cstring_toCharsSafe (exprNode_unparse(cconstant)); */
  54 /*    c = atoi( t ); */
  55 /*    ret->expr = constraintExpr_makeIntLiteral (c); */
  56
  57 /*    ret->post = TRUE; */
  58 /*    //  ret->orig = ret; */
  59 /*    DPRINTF(("GENERATED CONSTRAINT:")); */
  60 /*    DPRINTF( (message ("%s", constraint_print(ret) ) ) ); */
  61 /*    return ret; */
  62 /*  } */
  63
  64 constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
  65 {
  66   char *t;
  67   int c;
  68   constraint ret;
  69   ret = constraint_makeNew();
  70   llassert (l!=NULL);
  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
 117   ret->lexpr = constraintExpr_copy (l);
 118   #warning fix abstraction
 119
 120   if (relOp.tok == GE_OP)
 121       ret->ar = GTE;
 122   else if (relOp.tok == LE_OP)
 123     ret->ar = LTE;
 124   else if (relOp.tok == EQ_OP)
 125     ret->ar = EQ;
 126   else
 127   llfatalbug( message("Unsupported relational operator") );
 128
 129   ret->expr = constraintExpr_copy (r);
 130
 131   ret->post = TRUE;
 132
 133   ret->orig = constraint_copy(ret);
 134
 135   ret = constraint_simplify (ret);
 136
 137   //  ret->orig = ret;
 138   DPRINTF(("GENERATED CONSTRAINT:"));
 139   DPRINTF( (message ("%s", constraint_print(ret) ) ) );
 140   return ret;
 141 }
 142
 143 constraint constraint_copy (constraint c)
 144 {
 145   constraint ret;
 146
 147   llassert (constraint_isDefined(c) );
 148   // TPRINTF((message("Copying constraint %q", constraint_print) ));
 149
 150   ret = constraint_makeNew();
 151   ret->lexpr = constraintExpr_copy (c->lexpr);
 152   ret->ar = c->ar;
 153   ret->expr =  constraintExpr_copy (c->expr);
 154   ret->post = c->post;
 155   ret->generatingExpr = exprNode_fakeCopy(c->generatingExpr);
 156
 157   /*@i33 fix this*/
 158   if (c->orig != NULL)
 159     ret->orig = constraint_copy (c->orig);
 160   else
 161     ret->orig = NULL;
 162
 163   if (c->or != NULL)
 164     ret->or = constraint_copy (c->or);
 165   else
 166     ret->or = NULL;
 167
 168   ret->fcnPre = c->fcnPre;
 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   llassert (constraint_isDefined(c1) );
 178
 179   llassert (c1 != c2);
 180
 181   DPRINTF((message("OverWriteing constraint %q with %q", constraint_print(c1),
 182                    constraint_print(c2) ) ));
 183
 184   constraintExpr_free(c1->lexpr);
 185   constraintExpr_free(c1->expr);
 186
 187   c1->lexpr = constraintExpr_copy (c2->lexpr);
 188   c1->ar = c2->ar;
 189   c1->expr =  constraintExpr_copy (c2->expr);
 190   c1->post = c2->post;
 191
 192   if (c1->orig != NULL)
 193     constraint_free (c1->orig);
 194
 195   if (c2->orig != NULL)
 196     c1->orig = constraint_copy (c2->orig);
 197   else
 198     c1->orig = NULL;
 199
 200   /*@i33 make sure that the or is freed correctly*/
 201   if (c1->or != NULL)
 202     constraint_free (c1->or);
 203
 204   if (c2->or != NULL)
 205     c1->or = constraint_copy (c2->or);
 206   else
 207     c1->or = NULL;
 208
 209   c1->fcnPre = c2->fcnPre;
 210
 211   c1->generatingExpr = c2->generatingExpr;
 212 }
 213
 214
 215
 216 static /*@notnull@*/  /*@special@*/ constraint constraint_makeNew (void)
 217      /*@post:isnull result->or, result->orig,  result->generatingExpr, result->fcnPre @*/ /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/
 218 {
 219   constraint ret;
 220   ret = dmalloc(sizeof (*ret) );
 221   ret->lexpr = NULL;
 222   ret->expr = NULL;
 223   ret->ar = LT;
 224   ret->post = FALSE;
 225   ret->orig = NULL;
 226   ret->or = NULL;
 227   ret->generatingExpr = NULL;
 228   ret->fcnPre = NULL;
 229   return ret;
 230 }
 231
 232 constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
 233 {
 234
 235   if (c->generatingExpr == NULL)
 236     {
 237       c->generatingExpr = exprNode_fakeCopy(e);
 238       DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
 239     }
 240   else
 241     {
 242       DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
 243     }
 244   return c;
 245 }
 246
 247 constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
 248 {
 249
 250   if (c->orig != constraint_undefined)
 251     {
 252       c->orig = constraint_addGeneratingExpr(c->orig, e);
 253     }
 254   else
 255     {
 256       DPRINTF ((message ("constraint_origAddGeneratingExpr: Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
 257     }
 258   return c;
 259 }
 260
 261
 262
 263 constraint constraint_setFcnPre (/*@returned@*/ constraint c )
 264 {
 265
 266   if (c->orig != constraint_undefined)
 267     {
 268       c->orig->fcnPre = TRUE;
 269     }
 270   else
 271     {
 272       c->fcnPre = TRUE;
 273       TPRINTF(( message("Warning Setting fcnPre directly") ));
 274     }
 275   return c;
 276 }
 277
 278
 279
 280
 281 fileloc constraint_getFileloc (constraint c)
 282 {
 283   if (exprNode_isDefined(c->generatingExpr) )
 284     return (fileloc_copy (exprNode_getfileloc (c->generatingExpr) ) );
 285
 286   return (constraintExpr_getFileloc (c->lexpr) );
 287
 288
 289 }
 290
 291 static bool checkForMaxSet (constraint c)
 292 {
 293   if (constraintExpr_hasMaxSet(c->lexpr) || constraintExpr_hasMaxSet(c->expr) )
 294     return TRUE;
 295
 296   return FALSE;
 297 }
 298
 299 bool constraint_hasMaxSet(constraint c)
 300 {
 301   if (c->orig != NULL)
 302     {
 303       if (checkForMaxSet(c->orig) )
 304         return TRUE;
 305     }
 306
 307   return (checkForMaxSet(c) );
 308 }
 309
 310 constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
 311 {
 312   constraint ret = constraint_makeNew();
 313   //  constraintTerm term;
 314   po = exprNode_fakeCopy(po);
 315   ind = exprNode_fakeCopy(ind);
 316   ret->lexpr = constraintExpr_makeMaxReadExpr(po);
 317   ret->ar    = GTE;
 318   ret->expr  = constraintExpr_makeValueExpr (ind);
 319   ret->post = FALSE;
 320   return ret;
 321 }
 322
 323 constraint constraint_makeWriteSafeInt (exprNode po, int ind)
 324 {
 325   constraint ret = constraint_makeNew();
 326
 327
 328   ret->lexpr =constraintExpr_makeMaxSetExpr(po);
 329   ret->ar = GTE;
 330   ret->expr =  constraintExpr_makeIntLiteral (ind);
 331   /*@i1*/return ret;
 332 }
 333
 334 constraint constraint_makeSRefSetBufferSize (sRef s, long int size)
 335 {
 336  constraint ret = constraint_makeNew();
 337  ret->lexpr = constraintExpr_makeSRefMaxset (s);
 338  ret->ar = EQ;
 339  ret->expr =  constraintExpr_makeIntLiteral ((int)size);
 340  ret->post = TRUE;
 341  /*@i1*/return ret;
 342 }
 343
 344 constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
 345 {
 346   constraint ret = constraint_makeNew();
 347
 348
 349   ret->lexpr = constraintExpr_makeSRefMaxset ( s );
 350   ret->ar = GTE;
 351   ret->expr =  constraintExpr_makeIntLiteral (ind);
 352   ret->post = TRUE;
 353   /*@i1*/return ret;
 354 }
 355
 356 /* drl added 01/12/2000
 357
 358   makes the constraint: Ensures index <= MaxRead(buffer) */
 359
 360 constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer)
 361 {
 362   constraint ret = constraint_makeNew();
 363
 364   ret->lexpr = constraintExpr_makeValueExpr (index);
 365   ret->ar = LTE;
 366   ret->expr = constraintExpr_makeMaxReadExpr(buffer);
 367   ret->post = TRUE;
 368   return ret;
 369 }
 370
 371 constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
 372 {
 373   constraint ret = constraint_makeNew();
 374
 375
 376   ret->lexpr =constraintExpr_makeMaxSetExpr(po);
 377   ret->ar = GTE;
 378   ret->expr =  constraintExpr_makeValueExpr (ind);
 379   /*@i1*/return ret;
 380 }
 381
 382
 383 constraint constraint_makeReadSafeInt ( exprNode po, int ind)
 384 {
 385   constraint ret = constraint_makeNew();
 386
 387   po = exprNode_fakeCopy(po);
 388
 389   ret->lexpr = constraintExpr_makeMaxReadExpr(po);
 390   ret->ar    = GTE;
 391   ret->expr  = constraintExpr_makeIntLiteral (ind);
 392   ret->post = FALSE;
 393   return ret;
 394 }
 395
 396 constraint constraint_makeSRefReadSafeInt (sRef s, int ind)
 397 {
 398   constraint ret = constraint_makeNew();
 399
 400
 401   ret->lexpr = constraintExpr_makeSRefMaxRead (s );
 402   ret->ar = GTE;
 403   ret->expr =  constraintExpr_makeIntLiteral (ind);
 404   ret->post = TRUE;
 405   /*@i1*/return ret;
 406 }
 407
 408 constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
 409 {
 410   constraint ret;
 411
 412   e1 = exprNode_fakeCopy (e1);
 413   t2 = exprNode_fakeCopy (t2);
 414
 415   ret = constraint_makeReadSafeExprNode(e1, t2);
 416
 417   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 418
 419   ret->post = TRUE;
 420
 421   //  fileloc_incColumn (ret->lexpr->term->loc);
 422   return ret;
 423 }
 424
 425 static constraint constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintExpr c1, /*@only@*/ constraintExpr c2, fileloc sequencePoint,  arithType  ar)
 426 {
 427
 428   constraint ret;
 429
 430   llassert(c1 && c2);
 431   //  llassert(sequencePoint);
 432
 433   ret = constraint_makeNew();
 434
 435   ret->lexpr = c1;
 436   ret->ar = ar;
 437   ret->post = TRUE;
 438   ret->expr =  c2;
 439   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 440   return ret;
 441 }
 442
 443 static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint,  arithType  ar)
 444 {
 445   constraintExpr c1, c2;
 446   constraint ret;
 447   exprNode e;
 448
 449   if (! (e1 && e2) )
 450     {
 451       llcontbug((message("null exprNode, Exprnodes are %s and %s",
 452                        exprNode_unparse(e1), exprNode_unparse(e2) )
 453                ));
 454     }
 455
 456   //  llassert (sequencePoint);
 457
 458   e  =  exprNode_fakeCopy(e1);
 459   c1 =  constraintExpr_makeValueExpr (e);
 460
 461   e  =  exprNode_fakeCopy(e2);
 462   c2 =  constraintExpr_makeValueExpr (e);
 463
 464   ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
 465
 466   return ret;
 467 }
 468
 469
 470 /* make constraint ensures e1 == e2 */
 471
 472 constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 473 {
 474   return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) );
 475 }
 476
 477 /*make constraint ensures e1 < e2 */
 478 constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 479 {
 480   constraintExpr t1, t2;
 481
 482   t1 = constraintExpr_makeValueExpr (e1);
 483   t2 = constraintExpr_makeValueExpr (e2);
 484
 485   /*change this to e1 <= (e2 -1) */
 486
 487   t2 = constraintExpr_makeDecConstraintExpr (t2);
 488
 489  return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE) );
 490 }
 491
 492 constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 493 {
 494  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) );
 495 }
 496
 497 constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 498 {
 499   constraintExpr t1, t2;
 500
 501   t1 = constraintExpr_makeValueExpr (e1);
 502   t2 = constraintExpr_makeValueExpr (e2);
 503
 504
 505   /* change this to e1 >= (e2 + 1) */
 506   t2 = constraintExpr_makeIncConstraintExpr (t2);
 507
 508
 509  return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE) );
 510 }
 511
 512 constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 513 {
 514  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) );
 515 }
 516
 517
 518 exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
 519 {
 520   constraintList_free(dst->ensuresConstraints);
 521   constraintList_free(dst->requiresConstraints);
 522   constraintList_free(dst->trueEnsuresConstraints);
 523   constraintList_free(dst->falseEnsuresConstraints);
 524
 525   dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
 526   dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
 527   dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
 528   dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints );
 529   return dst;
 530 }
 531
 532 constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
 533 {
 534   constraint ret = constraint_makeNew();
 535   //constraintTerm term;
 536
 537   e = exprNode_fakeCopy(e);
 538   ret->lexpr = constraintExpr_makeValueExpr (e);
 539   ret->ar = EQ;
 540   ret->post = TRUE;
 541   ret->expr =  constraintExpr_makeValueExpr (e);
 542   ret->expr =  constraintExpr_makeDecConstraintExpr (ret->expr);
 543
 544   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 545 //   fileloc_incColumn (  ret->lexpr->term->loc);
 546 //   fileloc_incColumn (  ret->lexpr->term->loc);
 547   return ret;
 548 }
 549 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 550 {
 551   constraint ret = constraint_makeNew();
 552   //constraintTerm term;
 553
 554   e = exprNode_fakeCopy(e);
 555   ret->lexpr = constraintExpr_makeValueExpr (e);
 556   ret->ar = EQ;
 557   ret->post = TRUE;
 558   ret->expr =  constraintExpr_makeValueExpr (e);
 559   ret->expr =  constraintExpr_makeIncConstraintExpr (ret->expr);
 560
 561   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 562 //   fileloc_incColumn (  ret->lexpr->term->loc);
 563 //   fileloc_incColumn (  ret->lexpr->term->loc);
 564   return ret;
 565 }
 566
 567
 568 void constraint_free (/*@only@*/ /*@notnull@*/ constraint c)
 569 {
 570   llassert(constraint_isDefined (c) );
 571
 572
 573   if (constraint_isDefined(c->orig) )
 574     constraint_free (c->orig);
 575   if ( constraint_isDefined(c->or) )
 576     constraint_free (c->or);
 577
 578
 579   constraintExpr_free(c->lexpr);
 580   constraintExpr_free(c->expr);
 581
 582   c->orig = NULL;
 583   c->or = NULL;
 584   c->lexpr = NULL;
 585   c->expr  = NULL;
 586
 587   free (c);
 588
 589 }
 590
 591
 592 // constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 593 // {
 594 //   constraint ret = constraint_makeNew();
 595 //   //constraintTerm term;
 596
 597 //   e = exprNode_fakeCopy(e);
 598 //   ret->lexpr = constraintExpr_makeMaxReadExpr(e);
 599 //   ret->ar = EQ;
 600 //   ret->post = TRUE;
 601 //   ret->expr = constraintExpr_makeIncConstraintExpr (e);
 602 //   ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint);
 603 //   return ret;
 604 // }
 605
 606
 607 cstring arithType_print (arithType ar) /*@*/
 608 {
 609   cstring st = cstring_undefined;
 610   switch (ar)
 611     {
 612     case LT:
 613       st = cstring_makeLiteral (" < ");
 614       break;
 615     case        LTE:
 616       st = cstring_makeLiteral (" <= ");
 617       break;
 618     case        GT:
 619       st = cstring_makeLiteral (" > ");
 620       break;
 621     case        GTE:
 622       st = cstring_makeLiteral (" >= ");
 623       break;
 624     case        EQ:
 625       st = cstring_makeLiteral (" == ");
 626       break;
 627     case        NONNEGATIVE:
 628       st = cstring_makeLiteral (" NONNEGATIVE ");
 629       break;
 630     case        POSITIVE:
 631       st = cstring_makeLiteral (" POSITIVE ");
 632       break;
 633     default:
 634       llassert(FALSE);
 635       break;
 636     }
 637   return st;
 638 }
 639
 640
 641 void constraint_printErrorPostCondition (constraint c, fileloc loc)
 642 {
 643   cstring string;
 644   fileloc errorLoc, temp;
 645
 646   string = constraint_printDetailedPostCondition (c);
 647
 648   errorLoc = loc;
 649
 650   loc = NULL;
 651
 652   temp = constraint_getFileloc(c);
 653
 654   if (fileloc_isDefined(temp) )
 655     {
 656       errorLoc = temp;
 657       voptgenerror (  FLG_CHECKPOST, string, errorLoc);
 658       fileloc_free(temp);
 659     }
 660   else
 661     {
 662       voptgenerror (  FLG_CHECKPOST, string, errorLoc);
 663     }
 664 }
 665
 666
 667
 668
 669 void constraint_printError (constraint c, fileloc loc)
 670 {
 671   cstring string;
 672   fileloc errorLoc, temp;
 673
 674   string = constraint_printDetailed (c);
 675
 676   errorLoc = loc;
 677
 678   loc = NULL;
 679
 680   temp = constraint_getFileloc(c);
 681
 682   if (fileloc_isDefined(temp) )
 683     {
 684       errorLoc = temp;
 685
 686       if (c->post)
 687         {
 688           voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
 689         }
 690       else
 691         {
 692           voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
 693         }
 694       fileloc_free(temp);
 695     }
 696   else
 697     {
 698       if (c->post)
 699         {
 700           voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
 701         }
 702       else
 703         {
 704           voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
 705         }
 706     }
 707 }
 708
 709
 710 cstring constraint_printDeep (constraint c)
 711 {
 712   cstring st = cstring_undefined;
 713
 714   st = constraint_print(c);
 715
 716   if (c->orig != constraint_undefined)
 717     {
 718       if (!c->post)
 719         {
 720           if (c->orig->fcnPre)
 721             st = cstring_concatFree(st, (message(" derived from %s precondition: %q", exprNode_unparse(c->orig->generatingExpr), constraint_printDeep(c->orig) )
 722                                          ) );
 723           else
 724             st = cstring_concatFree(st,(message(" needed to satisfy %q",
 725                                                 constraint_printDeep(c->orig) )
 726                                         ) );
 727
 728         }
 729       else
 730         {
 731           st = cstring_concatFree(st,(message("derived from: %q",
 732                                               constraint_printDeep(c->orig) )
 733                                       ) );
 734         }
 735     }
 736
 737   return st;
 738
 739 }
 740
 741 cstring  constraint_printDetailedPostCondition (constraint c)
 742 {
 743   cstring st = cstring_undefined;
 744
 745   st = message ("Unsatisfied ensures constraint condition:\nLCLint is unable to verify the constraint %q", constraint_printDeep (c) );
 746
 747   if (context_getFlag (FLG_CONSTRAINTLOCATION) )
 748     {
 749       cstring temp;
 750       // llassert (c->generatingExpr);
 751       temp = message ("\nOriginal Generating expression %q: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
 752                       exprNode_unparse(c->generatingExpr) );
 753       st = cstring_concatFree (st, temp);
 754
 755       if (constraint_hasMaxSet(c) )
 756         {
 757           temp = message ("Has MaxSet\n");
 758           st = cstring_concatFree (st, temp);
 759         }
 760     }
 761   return st;
 762 }
 763
 764 cstring  constraint_printDetailed (constraint c)
 765 {
 766   cstring st = cstring_undefined;
 767
 768   if (!c->post)
 769     {
 770       st = message ("Unresolved constraint:\nLclint is unable to resolve %q", constraint_printDeep (c) );
 771     }
 772   else
 773     {
 774       st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_printDeep (c) );
 775     }
 776
 777   if (context_getFlag (FLG_CONSTRAINTLOCATION) )
 778     {
 779       cstring temp;
 780       // llassert (c->generatingExpr);
 781       temp = message ("\nOriginal Generating expression %q: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
 782                       exprNode_unparse(c->generatingExpr) );
 783       st = cstring_concatFree (st, temp);
 784
 785       if (constraint_hasMaxSet(c) )
 786         {
 787           temp = message ("Has MaxSet\n");
 788           st = cstring_concatFree (st, temp);
 789         }
 790     }
 791   return st;
 792 }
 793
 794 /*@only@*/ cstring  constraint_print (constraint c) /*@*/
 795 {
 796   cstring st = cstring_undefined;
 797   cstring type = cstring_undefined;
 798   llassert (c !=NULL);
 799   if (c->post)
 800     {
 801       type = cstring_makeLiteral ("Ensures: ");
 802     }
 803   else
 804     {
 805       type = cstring_makeLiteral ("Requires: ");
 806     }
 807   st = message ("%q: %q %q %q",
 808                 type,
 809                 constraintExpr_print (c->lexpr),
 810                 arithType_print(c->ar),
 811                 constraintExpr_print(c->expr)
 812                 );
 813   return st;
 814 }
 815
 816 cstring  constraint_printOr (constraint c) /*@*/
 817 {
 818   cstring ret;
 819   constraint temp;
 820
 821   ret = cstring_undefined;
 822   temp = c;
 823
 824   ret = cstring_concatFree (ret, constraint_print(temp) );
 825
 826   temp = temp->or;
 827
 828   while ( constraint_isDefined(temp) )
 829     {
 830       ret = cstring_concatFree (ret, cstring_makeLiteral (" OR ") );
 831       ret = cstring_concatFree (ret, constraint_print(temp) );
 832       temp = temp->or;
 833     }
 834
 835   return ret;
 836
 837 }
 838
 839 /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
 840                                                    exprNodeList arglist)
 841 {
 842   precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
 843                                                            arglist);
 844   precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
 845                                                            arglist);
 846
 847   return precondition;
 848 }
 849
 850
 851 constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall)
 852 {
 853   postcondition = constraint_copy (postcondition);
 854   postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
 855   postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
 856
 857   return postcondition;
 858 }
 859
 860 /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition,
 861                                                    exprNodeList arglist)
 862 {
 863
 864   precondition = constraint_copy (precondition);
 865   precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
 866   precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
 867
 868   precondition->fcnPre = FALSE;
 869   return precondition;
 870 }
 871
 872 // bool constraint_hasTerm (constraint c, constraintTerm term)
 873 // {
 874 //   DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );
 875
 876 //   if (constraintExpr_includesTerm (c->lexpr, term) )
 877 //     return TRUE;
 878
 879 //   if (constraintExpr_includesTerm (c->expr, term) )
 880 //     return TRUE;
 881
 882 //   return FALSE;
 883 // }
 884
 885 constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/
 886 {
 887
 888   DPRINTF( (message("Doing constraint_preserverOrig for %q ", constraint_printDetailed(c) ) ));
 889
 890   if (c->orig == constraint_undefined)
 891     c->orig = constraint_copy (c);
 892
 893   else if (c->orig->fcnPre)
 894     {
 895       constraint temp;
 896
 897       temp = c->orig;
 898
 899       /* avoid infinite loop */
 900       c->orig = NULL;
 901       c->orig = constraint_copy (c);
 902       if (c->orig->orig == NULL)
 903         c->orig->orig = temp;
 904       else
 905         llcontbug((message("Expected c->orig->orig to be null" ) ));
 906     }
 907   else
 908     {
 909       DPRINTF( (message("Not changing constraint") ));
 910     }
 911
 912   DPRINTF( (message("After Doing constraint_preserverOrig for %q ", constraint_printDetailed(c) ) ));
 913
 914   return c;
 915 }
 916 /*@=fcnuse*/
 917 /*@=assignexpose*/
 918 /*@=czechfcns@*/
 919
 920 constraint constraint_togglePost (/*@returned@*/ constraint c)
 921 {
 922   c->post = !c->post;
 923   return c;
 924 }