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 "exprNodeSList.h"
  15
  16 /*@i33*/
  17
  18 /*@access exprNode @*/
  19
  20
  21 static /*@only@*/ cstring  constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c);
  22
  23
  24 static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
  25      /*@post:isnull result->or, result->orig,  result->generatingExpr, result->fcnPre @*/
  26      /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/;
  27
  28 static void
  29 advanceField (char **s)
  30 {
  31   reader_checkChar (s, '@');
  32 }
  33
  34 # if 0
  35 static constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
  36 {
  37   char *t;
  38   int c;
  39   constraint ret;
  40   ret = constraint_makeNew ();
  41   llassert (constraintExpr_isDefined(l) );
  42
  43   ret->lexpr = constraintExpr_copy (l);
  44
  45
  46   if (relOp.tok == GE_OP)
  47       ret->ar = GTE;
  48   else if (relOp.tok == LE_OP)
  49     ret->ar = LTE;
  50   else if (relOp.tok == EQ_OP)
  51     ret->ar = EQ;
  52   else
  53   llfatalbug(message("Unsupported relational operator") );
  54
  55
  56   t =  cstring_toCharsSafe (exprNode_unparse(cconstant));
  57   c = atoi( t );
  58   ret->expr = constraintExpr_makeIntLiteral (c);
  59
  60   ret->post = TRUE;
  61   DPRINTF(("GENERATED CONSTRAINT:"));
  62   DPRINTF( (message ("%s", constraint_print(ret) ) ) );
  63   return ret;
  64 }
  65 # endif
  66
  67 bool constraint_same (constraint c1, constraint c2)
  68 {
  69   llassert (c1 != NULL);
  70   llassert (c2 != NULL);
  71
  72   if (c1->ar != c2->ar)
  73     {
  74       return FALSE;
  75     }
  76
  77   if (!constraintExpr_similar (c1->lexpr, c2->lexpr) )
  78     {
  79       return FALSE;
  80     }
  81
  82   if (!constraintExpr_similar (c1->expr, c2->expr) )
  83     {
  84       return FALSE;
  85     }
  86
  87   return TRUE;
  88 }
  89
  90 constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)
  91 {
  92   constraint ret;
  93   ret = constraint_makeNew();
  94   llassert (constraintExpr_isDefined(l) );
  95
  96   ret->lexpr = constraintExpr_copy (l);
  97
  98   if (relOp.tok == GE_OP)
  99       ret->ar = GTE;
 100   else if (relOp.tok == LE_OP)
 101     ret->ar = LTE;
 102   else if (relOp.tok == EQ_OP)
 103     ret->ar = EQ;
 104   else
 105   llfatalbug( message("Unsupported relational operator") );
 106
 107   ret->expr = constraintExpr_copy (r);
 108
 109   ret->post = TRUE;
 110
 111   ret->orig = constraint_copy(ret);
 112
 113   ret = constraint_simplify (ret);
 114   /* ret->orig = ret; */
 115
 116   DPRINTF(("GENERATED CONSTRAINT:"));
 117   DPRINTF( (message ("%s", constraint_print(ret) ) ) );
 118   return ret;
 119 }
 120
 121 constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint c)
 122 {
 123   constraint ret;
 124
 125   llassert (constraint_isDefined(c) );
 126
 127   ret = constraint_makeNew();
 128   ret->lexpr = constraintExpr_copy (c->lexpr);
 129   ret->ar = c->ar;
 130   ret->expr =  constraintExpr_copy (c->expr);
 131   ret->post = c->post;
 132   /*@-assignexpose@*/
 133   ret->generatingExpr = c->generatingExpr;
 134   /*@=assignexpose@*/
 135
 136   /*@i33 fix this*/
 137   if (c->orig != NULL)
 138     ret->orig = constraint_copy (c->orig);
 139   else
 140     ret->orig = NULL;
 141
 142   if (c->or != NULL)
 143     ret->or = constraint_copy (c->or);
 144   else
 145     ret->or = NULL;
 146
 147   ret->fcnPre = c->fcnPre;
 148
 149   return ret;
 150 }
 151
 152 /*like copy expect it doesn't allocate memory for the constraint*/
 153
 154 void constraint_overWrite (constraint c1, constraint c2)
 155 {
 156   llassert (constraint_isDefined(c1) );
 157
 158   llassert (c1 != c2);
 159
 160   DPRINTF((message("OverWriteing constraint %q with %q", constraint_print(c1),
 161                    constraint_print(c2) ) ));
 162
 163   constraintExpr_free(c1->lexpr);
 164   constraintExpr_free(c1->expr);
 165
 166   c1->lexpr = constraintExpr_copy (c2->lexpr);
 167   c1->ar = c2->ar;
 168   c1->expr =  constraintExpr_copy (c2->expr);
 169   c1->post = c2->post;
 170
 171   if (c1->orig != NULL)
 172     constraint_free (c1->orig);
 173
 174   if (c2->orig != NULL)
 175     c1->orig = constraint_copy (c2->orig);
 176   else
 177     c1->orig = NULL;
 178
 179   /*@i33 make sure that the or is freed correctly*/
 180   if (c1->or != NULL)
 181     constraint_free (c1->or);
 182
 183   if (c2->or != NULL)
 184     c1->or = constraint_copy (c2->or);
 185   else
 186     c1->or = NULL;
 187
 188   c1->fcnPre = c2->fcnPre;
 189
 190   /*@-assignexpose@*/
 191   c1->generatingExpr = c2->generatingExpr;
 192   /*@=assignexpose@*/
 193 }
 194
 195
 196
 197 static /*@notnull@*/  /*@special@*/ constraint constraint_makeNew (void)
 198      /*@post:isnull result->or, result->orig,  result->generatingExpr, result->fcnPre @*/
 199      /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/
 200 {
 201   constraint ret;
 202   ret = dmalloc(sizeof (*ret) );
 203   ret->lexpr = NULL;
 204   ret->expr = NULL;
 205   ret->ar = LT;
 206   ret->post = FALSE;
 207   ret->orig = NULL;
 208   ret->or = NULL;
 209   ret->generatingExpr = NULL;
 210   ret->fcnPre = NULL;
 211   return ret;
 212 }
 213
 214 constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, /*@exposed@*/ exprNode e)
 215 {
 216
 217   if (c->generatingExpr == NULL)
 218     {
 219       c->generatingExpr = e;
 220       DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
 221     }
 222   else
 223     {
 224       DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
 225     }
 226   return c;
 227 }
 228
 229 constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
 230 {
 231
 232   if (c->orig != constraint_undefined)
 233     {
 234       c->orig = constraint_addGeneratingExpr(c->orig, e);
 235     }
 236   else
 237     {
 238       DPRINTF ((message ("constraint_origAddGeneratingExpr: Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
 239     }
 240   return c;
 241 }
 242
 243 constraint constraint_setFcnPre (/*@returned@*/ constraint c )
 244 {
 245
 246   if (c->orig != constraint_undefined)
 247     {
 248       c->orig->fcnPre = TRUE;
 249     }
 250   else
 251     {
 252       c->fcnPre = TRUE;
 253       DPRINTF(( message("Warning Setting fcnPre directly") ));
 254     }
 255   return c;
 256 }
 257
 258
 259
 260
 261 fileloc constraint_getFileloc (constraint c)
 262 {
 263   if (exprNode_isDefined(c->generatingExpr) )
 264     return (fileloc_copy (exprNode_getfileloc (c->generatingExpr) ) );
 265
 266   return (constraintExpr_getFileloc (c->lexpr) );
 267
 268
 269 }
 270
 271 static bool checkForMaxSet (constraint c)
 272 {
 273   if (constraintExpr_hasMaxSet(c->lexpr) || constraintExpr_hasMaxSet(c->expr) )
 274     return TRUE;
 275
 276   return FALSE;
 277 }
 278
 279 bool constraint_hasMaxSet(constraint c)
 280 {
 281   if (checkForMaxSet(c) )
 282     return TRUE;
 283
 284   if (c->orig != NULL)
 285     {
 286       if (checkForMaxSet(c->orig) )
 287         return TRUE;
 288     }
 289
 290   return FALSE;
 291 }
 292
 293 constraint constraint_makeReadSafeExprNode (  exprNode po, exprNode ind)
 294 {
 295   constraint ret = constraint_makeNew();
 296
 297   po = po;
 298   ind = ind;
 299   ret->lexpr = constraintExpr_makeMaxReadExpr(po);
 300   ret->ar    = GTE;
 301   ret->expr  = constraintExpr_makeValueExpr (ind);
 302   ret->post = FALSE;
 303   return ret;
 304 }
 305
 306 constraint constraint_makeWriteSafeInt (   exprNode po, int ind)
 307 {
 308   constraint ret = constraint_makeNew();
 309
 310
 311   ret->lexpr =constraintExpr_makeMaxSetExpr(po);
 312   ret->ar = GTE;
 313   ret->expr =  constraintExpr_makeIntLiteral (ind);
 314   /*@i1*/return ret;
 315 }
 316
 317 constraint constraint_makeSRefSetBufferSize (sRef s, long int size)
 318 {
 319  constraint ret = constraint_makeNew();
 320  ret->lexpr = constraintExpr_makeSRefMaxset (s);
 321  ret->ar = EQ;
 322  ret->expr =  constraintExpr_makeIntLiteral ((int)size);
 323  ret->post = TRUE;
 324  /*@i1*/return ret;
 325 }
 326
 327 constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
 328 {
 329   constraint ret = constraint_makeNew();
 330
 331
 332   ret->lexpr = constraintExpr_makeSRefMaxset ( s );
 333   ret->ar = GTE;
 334   ret->expr =  constraintExpr_makeIntLiteral (ind);
 335   ret->post = TRUE;
 336   /*@i1*/return ret;
 337 }
 338
 339 /* drl added 01/12/2000
 340
 341   makes the constraint: Ensures index <= MaxRead(buffer) */
 342
 343 constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer)
 344 {
 345   constraint ret = constraint_makeNew();
 346
 347   ret->lexpr = constraintExpr_makeValueExpr (index);
 348   ret->ar = LTE;
 349   ret->expr = constraintExpr_makeMaxReadExpr(buffer);
 350   ret->post = TRUE;
 351   return ret;
 352 }
 353
 354 constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
 355 {
 356   constraint ret = constraint_makeNew();
 357
 358
 359   ret->lexpr =constraintExpr_makeMaxSetExpr(po);
 360   ret->ar = GTE;
 361   ret->expr =  constraintExpr_makeValueExpr (ind);
 362   /*@i1*/return ret;
 363 }
 364
 365
 366 constraint constraint_makeReadSafeInt ( exprNode t1, int index)
 367 {
 368   constraint ret = constraint_makeNew();
 369
 370   ret->lexpr = constraintExpr_makeMaxReadExpr(t1);
 371   ret->ar    = GTE;
 372   ret->expr  = constraintExpr_makeIntLiteral (index);
 373   ret->post = FALSE;
 374   return ret;
 375 }
 376
 377 constraint constraint_makeSRefReadSafeInt (sRef s, int ind)
 378 {
 379   constraint ret = constraint_makeNew();
 380
 381
 382   ret->lexpr = constraintExpr_makeSRefMaxRead (s );
 383   ret->ar = GTE;
 384   ret->expr =  constraintExpr_makeIntLiteral (ind);
 385   ret->post = TRUE;
 386   /*@i1*/return ret;
 387 }
 388
 389 constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, fileloc sequencePoint)
 390 {
 391   constraint ret;
 392
 393   ret = constraint_makeReadSafeExprNode(t1, t2);
 394   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 395   ret->post = TRUE;
 396
 397   return ret;
 398 }
 399
 400 static constraint constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintExpr c1, /*@only@*/ constraintExpr c2, fileloc sequencePoint,  arithType  ar)
 401 {
 402
 403   constraint ret;
 404
 405   llassert(constraintExpr_isDefined(c1) && constraintExpr_isDefined(c2) );
 406
 407   ret = constraint_makeNew();
 408
 409   ret->lexpr = c1;
 410   ret->ar = ar;
 411   ret->post = TRUE;
 412   ret->expr =  c2;
 413   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 414   return ret;
 415 }
 416
 417 static constraint constraint_makeEnsuresOp (/*@dependent@*/ exprNode e1, /*@dependent@*/ exprNode e2, fileloc sequencePoint,  arithType  ar)
 418 {
 419   constraintExpr c1, c2;
 420   constraint ret;
 421   exprNode e;
 422
 423   if (! (exprNode_isDefined(e1) && exprNode_isDefined(e2) ) )
 424     {
 425       llcontbug((message("null exprNode, Exprnodes are %s and %s",
 426                        exprNode_unparse(e1), exprNode_unparse(e2) )
 427                  ));
 428     }
 429
 430   e  =  e1;
 431   c1 =  constraintExpr_makeValueExpr (e);
 432
 433   e  =  e2;
 434   c2 =  constraintExpr_makeValueExpr (e);
 435
 436   ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
 437
 438   return ret;
 439 }
 440
 441
 442 /* make constraint ensures e1 == e2 */
 443
 444 constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 445 {
 446   return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) );
 447 }
 448
 449 /*make constraint ensures e1 < e2 */
 450 constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 451 {
 452   constraintExpr t1, t2;
 453
 454   t1 = constraintExpr_makeValueExpr (e1);
 455   t2 = constraintExpr_makeValueExpr (e2);
 456
 457   /*change this to e1 <= (e2 -1) */
 458
 459   t2 = constraintExpr_makeDecConstraintExpr (t2);
 460
 461  return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE) );
 462 }
 463
 464 constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 465 {
 466  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) );
 467 }
 468
 469 constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 470 {
 471   constraintExpr t1, t2;
 472
 473   t1 = constraintExpr_makeValueExpr (e1);
 474   t2 = constraintExpr_makeValueExpr (e2);
 475
 476
 477   /* change this to e1 >= (e2 + 1) */
 478   t2 = constraintExpr_makeIncConstraintExpr (t2);
 479
 480
 481  return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE) );
 482 }
 483
 484 constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 485 {
 486  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) );
 487 }
 488
 489
 490 exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
 491 {
 492   constraintList_free(dst->ensuresConstraints);
 493   constraintList_free(dst->requiresConstraints);
 494   constraintList_free(dst->trueEnsuresConstraints);
 495   constraintList_free(dst->falseEnsuresConstraints);
 496
 497   dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
 498   dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
 499   dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
 500   dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints );
 501   return dst;
 502 }
 503
 504 /* Makes the constraint e = e + f */
 505 constraint constraint_makeAddAssign (exprNode e, exprNode f, fileloc sequencePoint)
 506 {
 507   constraintExpr x1, x2, y;
 508   constraint ret;
 509
 510   ret = constraint_makeNew();
 511
 512   x1 =  constraintExpr_makeValueExpr (e);
 513   x2 =  constraintExpr_copy(x1);
 514   y  =  constraintExpr_makeValueExpr (f);
 515
 516   ret->lexpr = x1;
 517   ret->ar = EQ;
 518   ret->post = TRUE;
 519   ret->expr = constraintExpr_makeAddExpr (x2, y);
 520
 521   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 522
 523   return ret;
 524 }
 525
 526
 527 /* Makes the constraint e = e - f */
 528 constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequencePoint)
 529 {
 530   constraintExpr x1, x2, y;
 531   constraint ret;
 532
 533   ret = constraint_makeNew();
 534
 535   x1 =  constraintExpr_makeValueExpr (e);
 536   x2 =  constraintExpr_copy(x1);
 537   y  =  constraintExpr_makeValueExpr (f);
 538
 539   ret->lexpr = x1;
 540   ret->ar = EQ;
 541   ret->post = TRUE;
 542   ret->expr = constraintExpr_makeSubtractExpr (x2, y);
 543
 544   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 545
 546   return ret;
 547 }
 548
 549 constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
 550 {
 551   constraint ret = constraint_makeNew();
 552
 553   ret->lexpr = constraintExpr_makeValueExpr (e);
 554   ret->ar = EQ;
 555   ret->post = TRUE;
 556   ret->expr =  constraintExpr_makeValueExpr (e);
 557   ret->expr =  constraintExpr_makeDecConstraintExpr (ret->expr);
 558   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 559   return ret;
 560 }
 561 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 562 {
 563   constraint ret = constraint_makeNew();
 564
 565   ret->lexpr = constraintExpr_makeValueExpr (e);
 566   ret->ar = EQ;
 567   ret->post = TRUE;
 568   ret->expr =  constraintExpr_makeValueExpr (e);
 569   ret->expr =  constraintExpr_makeIncConstraintExpr (ret->expr);
 570
 571   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 572   return ret;
 573 }
 574
 575
 576 void constraint_free (/*@only@*/ constraint c)
 577 {
 578   llassert(constraint_isDefined (c) );
 579
 580
 581   if (constraint_isDefined(c->orig) )
 582     constraint_free (c->orig);
 583   if ( constraint_isDefined(c->or) )
 584     constraint_free (c->or);
 585
 586
 587   constraintExpr_free(c->lexpr);
 588   constraintExpr_free(c->expr);
 589
 590   c->orig = NULL;
 591   c->or = NULL;
 592   c->lexpr = NULL;
 593   c->expr  = NULL;
 594
 595   free (c);
 596
 597 }
 598
 599 cstring arithType_print (arithType ar) /*@*/
 600 {
 601   cstring st = cstring_undefined;
 602   switch (ar)
 603     {
 604     case LT:
 605       st = cstring_makeLiteral ("<");
 606       break;
 607     case        LTE:
 608       st = cstring_makeLiteral ("<=");
 609       break;
 610     case        GT:
 611       st = cstring_makeLiteral (">");
 612       break;
 613     case        GTE:
 614       st = cstring_makeLiteral (">=");
 615       break;
 616     case        EQ:
 617       st = cstring_makeLiteral ("==");
 618       break;
 619     case        NONNEGATIVE:
 620       st = cstring_makeLiteral ("NONNEGATIVE");
 621       break;
 622     case        POSITIVE:
 623       st = cstring_makeLiteral ("POSITIVE");
 624       break;
 625     default:
 626       llassert(FALSE);
 627       break;
 628     }
 629   return st;
 630 }
 631
 632 void constraint_printErrorPostCondition (constraint c, fileloc loc)
 633 {
 634   cstring string;
 635   fileloc errorLoc, temp;
 636
 637   string = constraint_printDetailedPostCondition (c);
 638
 639   errorLoc = loc;
 640
 641   loc = NULL;
 642
 643   temp = constraint_getFileloc(c);
 644
 645   if (fileloc_isDefined(temp) )
 646     {
 647       errorLoc = temp;
 648       voptgenerror (  FLG_CHECKPOST, string, errorLoc);
 649       fileloc_free(temp);
 650     }
 651   else
 652     {
 653       voptgenerror (  FLG_CHECKPOST, string, errorLoc);
 654     }
 655 }
 656
 657  /*drl added 8-11-001*/
 658 cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint c) /*@*/
 659 {
 660   cstring string, ret;
 661   fileloc errorLoc;
 662
 663   string = constraint_print(c);
 664
 665   errorLoc = constraint_getFileloc(c);
 666
 667   ret = message ("constraint: %q @ %q", string, fileloc_unparse(errorLoc) );
 668
 669   fileloc_free(errorLoc);
 670   return ret;
 671
 672 }
 673
 674
 675
 676 void constraint_printError (constraint c, fileloc loc)
 677 {
 678   cstring string;
 679   fileloc errorLoc, temp;
 680
 681   string = constraint_printDetailed (c);
 682
 683   errorLoc = loc;
 684
 685   temp = constraint_getFileloc(c);
 686
 687   if (fileloc_isDefined(temp) )
 688     {
 689       errorLoc = temp;
 690     }
 691   else
 692     {
 693       llassert(FALSE);
 694       DPRINTF (("constraint %s had undefined fileloc %s", constraint_print(c), fileloc_unparse(temp)));
 695       fileloc_free(temp);
 696       errorLoc = fileloc_copy(errorLoc);
 697     }
 698
 699   if (c->post)
 700     {
 701       voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
 702     }
 703   else
 704     {
 705       if (constraint_hasMaxSet (c) )
 706         voptgenerror (FLG_ARRAYBOUNDS, string, errorLoc);
 707       else
 708         voptgenerror (FLG_ARRAYBOUNDSREAD, string, errorLoc);
 709     }
 710
 711   fileloc_free(errorLoc);
 712
 713 }
 714
 715
 716 static cstring constraint_printDeep (constraint c)
 717 {
 718   cstring genExpr;
 719   cstring st = cstring_undefined;
 720
 721   st = constraint_print(c);
 722
 723
 724   if (c->orig != constraint_undefined)
 725     {
 726       st = cstring_appendChar(st, '\n');
 727       genExpr =  exprNode_unparse(c->orig->generatingExpr);
 728       if (!c->post)
 729         {
 730           if (c->orig->fcnPre)
 731             st = cstring_concatFree(st, (message(" derived from %s precondition: %q", genExpr, constraint_printDeep(c->orig) )
 732                                          ) );
 733           else
 734             st = cstring_concatFree(st,(message(" needed to satisfy precondition:\n%q",
 735                                                 constraint_printDeep(c->orig) )
 736                                         ) );
 737
 738         }
 739       else
 740         {
 741           st = cstring_concatFree(st,(message("derived from: %q",
 742                                               constraint_printDeep(c->orig) )
 743                                       ) );
 744         }
 745     }
 746
 747   return st;
 748
 749 }
 750
 751
 752 static /*@only@*/ cstring  constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c)
 753 {
 754   cstring st = cstring_undefined;
 755   cstring genExpr;
 756
 757   st = message ("Unsatisfied ensures constraint condition:\nLCLint is unable to verify the constraint %q", constraint_printDeep (c) );
 758
 759   genExpr = exprNode_unparse (c->generatingExpr);
 760
 761   if (context_getFlag (FLG_CONSTRAINTLOCATION) )
 762     {
 763       cstring temp;
 764
 765       temp = message ("\nOriginal Generating expression %q: %s\n",
 766                       fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
 767                       genExpr );
 768       st = cstring_concatFree (st, temp);
 769
 770       if (constraint_hasMaxSet(c) )
 771         {
 772           temp = message ("Has MaxSet\n");
 773           st = cstring_concatFree (st, temp);
 774         }
 775     }
 776   return st;
 777 }
 778
 779 cstring  constraint_printDetailed (constraint c)
 780 {
 781   cstring st = cstring_undefined;
 782   cstring temp = cstring_undefined;
 783     cstring genExpr;
 784
 785   if (!c->post)
 786     {
 787       st = message ("Unable to resolve constraint:\n%q", constraint_printDeep (c) );
 788     }
 789   else
 790     {
 791       st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_printDeep (c) );
 792     }
 793
 794   if (constraint_hasMaxSet(c) )
 795     {
 796       temp = cstring_makeLiteral("Possible out-of-bounds store:\n");
 797     }
 798   else
 799     {
 800       temp = cstring_makeLiteral("Possible out-of-bounds read:\n");
 801     }
 802
 803   genExpr = exprNode_unparse (c->generatingExpr);
 804
 805   if (context_getFlag (FLG_CONSTRAINTLOCATION) )
 806     {
 807       cstring temp2;
 808       temp2 = message ("%s\n", genExpr );
 809       temp = cstring_concatFree (temp, temp2);
 810     }
 811
 812   st  = cstring_concatFree(temp,st);
 813
 814   return st;
 815 }
 816
 817 /*@only@*/ cstring  constraint_print (constraint c) /*@*/
 818 {
 819   cstring st = cstring_undefined;
 820   cstring type = cstring_undefined;
 821   llassert (c !=NULL);
 822   if (c->post)
 823     {
 824       if (context_getFlag (FLG_PARENCONSTRAINT) )
 825         {
 826           type = cstring_makeLiteral ("ensures: ");
 827         }
 828       else
 829         {
 830            type = cstring_makeLiteral ("ensures");
 831         }
 832     }
 833   else
 834     {
 835       if (context_getFlag (FLG_PARENCONSTRAINT) )
 836         {
 837           type = cstring_makeLiteral ("requires: ");
 838         }
 839       else
 840         {
 841           type = cstring_makeLiteral ("requires");
 842         }
 843
 844     }
 845       if (context_getFlag (FLG_PARENCONSTRAINT) )
 846         {
 847           st = message ("%q: %q %q %q",
 848                         type,
 849                         constraintExpr_print (c->lexpr),
 850                         arithType_print(c->ar),
 851                         constraintExpr_print(c->expr)
 852                         );
 853         }
 854       else
 855         {
 856           st = message ("%q %q %q %q",
 857                         type,
 858                         constraintExpr_print (c->lexpr),
 859                         arithType_print(c->ar),
 860                         constraintExpr_print(c->expr)
 861                 );
 862         }
 863   return st;
 864 }
 865
 866 cstring  constraint_printOr (constraint c) /*@*/
 867 {
 868   cstring ret;
 869   constraint temp;
 870
 871   ret = cstring_undefined;
 872   temp = c;
 873
 874   ret = cstring_concatFree (ret, constraint_print(temp) );
 875
 876   temp = temp->or;
 877
 878   while ( constraint_isDefined(temp) )
 879     {
 880       ret = cstring_concatFree (ret, cstring_makeLiteral (" OR ") );
 881       ret = cstring_concatFree (ret, constraint_print(temp) );
 882       temp = temp->or;
 883     }
 884
 885   return ret;
 886
 887 }
 888
 889 /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
 890                                                    exprNodeList arglist)
 891 {
 892   precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
 893                                                            arglist);
 894   precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
 895                                                            arglist);
 896
 897   return precondition;
 898 }
 899
 900
 901 constraint constraint_doFixResult (constraint postcondition, /*@dependent@*/ exprNode fcnCall)
 902 {
 903   postcondition = constraint_copy (postcondition);
 904   postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
 905   postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
 906
 907   return postcondition;
 908 }
 909
 910 /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition,
 911                                                    exprNodeList arglist)
 912 {
 913
 914   precondition = constraint_copy (precondition);
 915   precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
 916   precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
 917
 918   precondition->fcnPre = FALSE;
 919   return precondition;
 920 }
 921
 922 constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/
 923 {
 924
 925   DPRINTF( (message("Doing constraint_preserverOrig for %q ", constraint_printDetailed(c) ) ));
 926
 927   if (c->orig == constraint_undefined)
 928     c->orig = constraint_copy (c);
 929
 930   else if (c->orig->fcnPre)
 931     {
 932       constraint temp;
 933
 934       temp = c->orig;
 935
 936       /* avoid infinite loop */
 937       c->orig = NULL;
 938       c->orig = constraint_copy (c);
 939       if (c->orig->orig == NULL)
 940         {
 941           c->orig->orig = temp;
 942           temp = NULL;
 943         }
 944       else
 945         {
 946           llcontbug((message("Expected c->orig->orig to be null" ) ));
 947           constraint_free(c->orig->orig);
 948           c->orig->orig = temp;
 949           temp = NULL;
 950         }
 951     }
 952   else
 953     {
 954       DPRINTF( (message("Not changing constraint") ));
 955     }
 956
 957   DPRINTF( (message("After Doing constraint_preserverOrig for %q ", constraint_printDetailed(c) ) ));
 958
 959   return c;
 960 }
 961 /*@=fcnuse*/
 962 /*@=assignexpose*/
 963 /*@=czechfcns@*/
 964
 965
 966 constraint constraint_togglePost (/*@returned@*/ constraint c)
 967 {
 968   c->post = !c->post;
 969   return c;
 970 }
 971
 972 constraint constraint_togglePostOrig (/*@returned@*/ constraint c)
 973 {
 974   if (c->orig != NULL)
 975     c->orig = constraint_togglePost(c->orig);
 976   return c;
 977 }
 978
 979 bool constraint_hasOrig( /*@observer@*/ /*@temp@*/ constraint c)
 980 {
 981   if (c->orig == NULL)
 982     return FALSE;
 983   else
 984     return TRUE;
 985 }
 986
 987
 988 constraint constraint_undump (FILE *f)
 989 {
 990   constraint c;
 991   bool           fcnPre;
 992   bool post;
 993   arithType       ar;
 994
 995   constraintExpr lexpr;
 996   constraintExpr  expr;
 997
 998
 999   char * s;
1000
1001   char *os;
1002
1003   s = mstring_create (MAX_DUMP_LINE_LENGTH);
1004
1005   os = s;
1006
1007   s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
1008
1009   /*@i33*/ /*this should probably be wrappered...*/
1010
1011   fcnPre = (bool) reader_getInt (&s);
1012   advanceField(&s);
1013   post = (bool) reader_getInt (&s);
1014   advanceField(&s);
1015   ar = (arithType) reader_getInt (&s);
1016
1017   s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
1018
1019   reader_checkChar (&s, 'l');
1020
1021   lexpr = constraintExpr_undump (f);
1022
1023   s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
1024
1025   reader_checkChar (&s, 'r');
1026   expr = constraintExpr_undump (f);
1027
1028   c = constraint_makeNew();
1029
1030   c->fcnPre = fcnPre;
1031   c->post = post;
1032   c->ar = ar;
1033
1034   c->lexpr = lexpr;
1035   c->expr =  expr;
1036
1037   free(os);
1038   c = constraint_preserveOrig(c);
1039   return c;
1040 }
1041
1042
1043 void constraint_dump (/*@observer@*/ constraint c,  FILE *f)
1044 {
1045   bool           fcnPre;
1046   bool post;
1047   arithType       ar;
1048
1049   constraintExpr lexpr;
1050   constraintExpr  expr;
1051
1052
1053   fcnPre = c->fcnPre;
1054   post   = c->post;
1055   ar     = c->ar;
1056   lexpr = c->lexpr;
1057   expr = c->expr;
1058
1059   fprintf(f, "%d@%d@%d\n", (int) fcnPre, (int) post, (int) ar);
1060   fprintf(f,"l\n");
1061   constraintExpr_dump (lexpr, f);
1062   fprintf(f,"r\n");
1063   constraintExpr_dump (expr, f);
1064 }
1065
1066
1067 int constraint_compare (/*@observer@*/ /*@temp@*/ const constraint * c1, /*@observer@*/ /*@temp@*/ const constraint * c2) /*@*/
1068 {
1069   fileloc loc1, loc2;
1070
1071   int ret;
1072
1073   llassert(constraint_isDefined(*c1) );
1074   llassert(constraint_isDefined(*c2) );
1075
1076   if (constraint_isUndefined(*c1) )
1077     {
1078         if (constraint_isUndefined(*c2) )
1079           return 0;
1080         else
1081           return 1;
1082     }
1083
1084   if (constraint_isUndefined(*c2) )
1085     {
1086       return -1;
1087     }
1088
1089   loc1 = constraint_getFileloc(*c1);
1090   loc2 = constraint_getFileloc(*c2);
1091
1092   ret = fileloc_compare(loc1, loc2);
1093
1094   fileloc_free(loc1);
1095   fileloc_free(loc2);
1096
1097   return ret;
1098 }
1099
1100
1101 bool constraint_isPost  (/*@observer@*/ /*@temp@*/ constraint c)
1102 {
1103   llassert(constraint_isDefined(c) );
1104
1105   if (constraint_isUndefined(c) )
1106     return FALSE;
1107
1108   return (c->post);
1109 }
1110
1111
1112 static int constraint_getDepth(/*@observer@*/ /*@temp@*/ constraint c)
1113 {
1114   int l , r;
1115
1116   l = constraintExpr_getDepth(c->lexpr);
1117   r = constraintExpr_getDepth(c->expr);
1118
1119   if (l > r)
1120     {
1121       DPRINTF(( message("constraint depth returning %d for %s", l, constraint_print(c) ) ));
1122       return l;
1123     }
1124   else
1125     {
1126       DPRINTF(( message("constraint depth returning %d for %s", r, constraint_print(c) ) ));
1127       return r;
1128     }
1129 }
1130
1131
1132 bool constraint_tooDeep (/*@observer@*/ /*@temp@*/ constraint c)
1133 {
1134   int temp;
1135
1136   temp = constraint_getDepth(c);
1137
1138   if (temp >= 20 )
1139     {
1140       return TRUE;
1141     }
1142
1143   return FALSE;
1144
1145 }