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