src/constraint.c

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