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
 260   llassert (constraint_isDefined (c) );
 261
 262   if (exprNode_isDefined (c->generatingExpr))
 263     return (fileloc_copy (exprNode_getfileloc (c->generatingExpr)));
 264
 265   return (constraintExpr_getFileloc (c->lexpr));
 266
 267
 268 }
 269
 270 static bool checkForMaxSet (constraint c)
 271 {
 272
 273   llassert (constraint_isDefined (c) );
 274
 275   if (constraintExpr_hasMaxSet (c->lexpr) || constraintExpr_hasMaxSet (c->expr))
 276     return TRUE;
 277
 278   return FALSE;
 279 }
 280
 281 bool constraint_hasMaxSet (constraint c)
 282 {
 283
 284   llassert (constraint_isDefined (c) );
 285
 286   if (checkForMaxSet (c))
 287     return TRUE;
 288
 289   if (c->orig != NULL)
 290     {
 291       if (checkForMaxSet (c->orig))
 292         return TRUE;
 293     }
 294
 295   return FALSE;
 296 }
 297
 298 constraint constraint_makeReadSafeExprNode (exprNode po, exprNode ind)
 299 {
 300   constraint ret = constraint_makeNew ();
 301
 302   po = po;
 303   ind = ind;
 304   ret->lexpr = constraintExpr_makeMaxReadExpr (po);
 305   ret->ar    = GTE;
 306   ret->expr  = constraintExpr_makeValueExpr (ind);
 307   ret->post = FALSE;
 308   return ret;
 309 }
 310
 311 constraint constraint_makeWriteSafeInt (   exprNode po, int ind)
 312 {
 313   constraint ret = constraint_makeNew ();
 314
 315   ret->lexpr =constraintExpr_makeMaxSetExpr (po);
 316   ret->ar = GTE;
 317   ret->expr =  constraintExpr_makeIntLiteral (ind);
 318   /*@i1*/return ret;
 319 }
 320
 321 constraint constraint_makeSRefSetBufferSize (sRef s, long int size)
 322 {
 323  constraint ret = constraint_makeNew ();
 324  ret->lexpr = constraintExpr_makeSRefMaxset (s);
 325  ret->ar = EQ;
 326  ret->expr =  constraintExpr_makeIntLiteral ((int)size);
 327  ret->post = TRUE;
 328  return ret;
 329 }
 330
 331 constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
 332 {
 333   constraint ret = constraint_makeNew ();
 334
 335
 336   ret->lexpr = constraintExpr_makeSRefMaxset ( s);
 337   ret->ar = GTE;
 338   ret->expr =  constraintExpr_makeIntLiteral (ind);
 339   ret->post = TRUE;
 340   return ret;
 341 }
 342
 343 /* drl added 01/12/2000
 344
 345   makes the constraint: Ensures index <= MaxRead (buffer) */
 346
 347 constraint constraint_makeEnsureLteMaxRead (exprNode index, exprNode buffer)
 348 {
 349   constraint ret = constraint_makeNew ();
 350
 351   ret->lexpr = constraintExpr_makeValueExpr (index);
 352   ret->ar = LTE;
 353   ret->expr = constraintExpr_makeMaxReadExpr (buffer);
 354   ret->post = TRUE;
 355   return ret;
 356 }
 357
 358 constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
 359 {
 360   constraint ret = constraint_makeNew ();
 361
 362
 363   ret->lexpr =constraintExpr_makeMaxSetExpr (po);
 364   ret->ar = GTE;
 365   ret->expr =  constraintExpr_makeValueExpr (ind);
 366   /*@i1*/return ret;
 367 }
 368
 369
 370 constraint constraint_makeReadSafeInt ( exprNode t1, int index)
 371 {
 372   constraint ret = constraint_makeNew ();
 373
 374   ret->lexpr = constraintExpr_makeMaxReadExpr (t1);
 375   ret->ar    = GTE;
 376   ret->expr  = constraintExpr_makeIntLiteral (index);
 377   ret->post = FALSE;
 378   return ret;
 379 }
 380
 381 constraint constraint_makeSRefReadSafeInt (sRef s, int ind)
 382 {
 383   constraint ret = constraint_makeNew ();
 384
 385
 386   ret->lexpr = constraintExpr_makeSRefMaxRead (s);
 387   ret->ar = GTE;
 388   ret->expr =  constraintExpr_makeIntLiteral (ind);
 389   ret->post = TRUE;
 390   return ret;
 391 }
 392
 393 constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, fileloc sequencePoint)
 394 {
 395   constraint ret;
 396
 397   ret = constraint_makeReadSafeExprNode (t1, t2);
 398   llassert (constraint_isDefined (ret) );
 399
 400   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 401   ret->post = TRUE;
 402
 403   return ret;
 404 }
 405
 406 static constraint constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintExpr c1, /*@only@*/ constraintExpr c2, fileloc sequencePoint,  arithType  ar)
 407 {
 408
 409   constraint ret;
 410
 411   llassert (constraintExpr_isDefined (c1) && constraintExpr_isDefined (c2));
 412
 413   ret = constraint_makeNew ();
 414
 415   ret->lexpr = c1;
 416   ret->ar = ar;
 417   ret->post = TRUE;
 418   ret->expr =  c2;
 419   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 420   return ret;
 421 }
 422
 423 static constraint constraint_makeEnsuresOp (/*@dependent@*/ exprNode e1, /*@dependent@*/ exprNode e2, fileloc sequencePoint,  arithType  ar)
 424 {
 425   constraintExpr c1, c2;
 426   constraint ret;
 427   exprNode e;
 428
 429   if (! (exprNode_isDefined (e1) && exprNode_isDefined (e2)))
 430     {
 431       llcontbug ((message ("null exprNode, Exprnodes are %s and %s",
 432                        exprNode_unparse (e1), exprNode_unparse (e2))
 433                 ));
 434     }
 435
 436   e  =  e1;
 437   c1 =  constraintExpr_makeValueExpr (e);
 438
 439   e  =  e2;
 440   c2 =  constraintExpr_makeValueExpr (e);
 441
 442   ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
 443
 444   return ret;
 445 }
 446
 447
 448 /* make constraint ensures e1 == e2 */
 449
 450 constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 451 {
 452   return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ));
 453 }
 454
 455 /*make constraint ensures e1 < e2 */
 456 constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 457 {
 458   constraintExpr t1, t2;
 459   constraint t3;
 460
 461   t1 = constraintExpr_makeValueExpr (e1);
 462   t2 = constraintExpr_makeValueExpr (e2);
 463
 464   /*change this to e1 <= (e2 -1) */
 465
 466   t2 = constraintExpr_makeDecConstraintExpr (t2);
 467
 468   t3 =  constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE);
 469
 470   t3 = constraint_simplify(t3);
 471   return (t3);
 472 }
 473
 474 constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 475 {
 476  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE));
 477 }
 478
 479 constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 480 {
 481   constraintExpr t1, t2;
 482   constraint t3;
 483
 484   t1 = constraintExpr_makeValueExpr (e1);
 485   t2 = constraintExpr_makeValueExpr (e2);
 486
 487
 488   /* change this to e1 >= (e2 + 1) */
 489   t2 = constraintExpr_makeIncConstraintExpr (t2);
 490
 491   t3 =  constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE);
 492
 493   t3 = constraint_simplify(t3);
 494
 495   return t3;
 496 }
 497
 498 constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 499 {
 500  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE));
 501 }
 502
 503
 504
 505 /* Makes the constraint e = e + f */
 506 constraint constraint_makeAddAssign (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_makeAddExpr (x2, y);
 521
 522   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 523
 524   return ret;
 525 }
 526
 527
 528 /* Makes the constraint e = e - f */
 529 constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequencePoint)
 530 {
 531   constraintExpr x1, x2, y;
 532   constraint ret;
 533
 534   ret = constraint_makeNew ();
 535
 536   x1 =  constraintExpr_makeValueExpr (e);
 537   x2 =  constraintExpr_copy (x1);
 538   y  =  constraintExpr_makeValueExpr (f);
 539
 540   ret->lexpr = x1;
 541   ret->ar = EQ;
 542   ret->post = TRUE;
 543   ret->expr = constraintExpr_makeSubtractExpr (x2, y);
 544
 545   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 546
 547   return ret;
 548 }
 549
 550 constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
 551 {
 552   constraint ret = constraint_makeNew ();
 553
 554   ret->lexpr = constraintExpr_makeValueExpr (e);
 555   ret->ar = EQ;
 556   ret->post = TRUE;
 557   ret->expr =  constraintExpr_makeValueExpr (e);
 558   ret->expr =  constraintExpr_makeDecConstraintExpr (ret->expr);
 559   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 560   return ret;
 561 }
 562 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 563 {
 564   constraint ret = constraint_makeNew ();
 565
 566   ret->lexpr = constraintExpr_makeValueExpr (e);
 567   ret->ar = EQ;
 568   ret->post = TRUE;
 569   ret->expr =  constraintExpr_makeValueExpr (e);
 570   ret->expr =  constraintExpr_makeIncConstraintExpr (ret->expr);
 571
 572   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 573   return ret;
 574 }
 575
 576
 577 void constraint_free (/*@only@*/ constraint c)
 578 {
 579   llassert (constraint_isDefined (c));
 580
 581
 582   if (constraint_isDefined (c->orig))
 583     constraint_free (c->orig);
 584   if ( constraint_isDefined (c->or))
 585     constraint_free (c->or);
 586
 587
 588   constraintExpr_free (c->lexpr);
 589   constraintExpr_free (c->expr);
 590
 591   c->orig = NULL;
 592   c->or = NULL;
 593   c->lexpr = NULL;
 594   c->expr  = NULL;
 595
 596   free (c);
 597
 598 }
 599
 600 cstring arithType_print (arithType ar) /*@*/
 601 {
 602   cstring st = cstring_undefined;
 603   switch (ar)
 604     {
 605     case LT:
 606       st = cstring_makeLiteral ("<");
 607       break;
 608     case        LTE:
 609       st = cstring_makeLiteral ("<=");
 610       break;
 611     case        GT:
 612       st = cstring_makeLiteral (">");
 613       break;
 614     case        GTE:
 615       st = cstring_makeLiteral (">=");
 616       break;
 617     case        EQ:
 618       st = cstring_makeLiteral ("==");
 619       break;
 620     case        NONNEGATIVE:
 621       st = cstring_makeLiteral ("NONNEGATIVE");
 622       break;
 623     case        POSITIVE:
 624       st = cstring_makeLiteral ("POSITIVE");
 625       break;
 626     default:
 627       llassert (FALSE);
 628       break;
 629     }
 630   return st;
 631 }
 632
 633 void constraint_printErrorPostCondition (constraint c, fileloc loc)
 634 {
 635   cstring string;
 636   fileloc errorLoc, temp;
 637
 638   string = constraint_unparseDetailedPostCondition (c);
 639
 640   errorLoc = loc;
 641
 642   loc = NULL;
 643
 644   temp = constraint_getFileloc (c);
 645
 646
 647   if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES ) )
 648     {
 649       string = cstring_replaceChar(string, '\n', ' ');
 650     }
 651
 652   if (fileloc_isDefined (temp))
 653     {
 654       errorLoc = temp;
 655       voptgenerror (  FLG_CHECKPOST, string, errorLoc);
 656       fileloc_free (temp);
 657     }
 658   else
 659     {
 660       voptgenerror (  FLG_CHECKPOST, string, errorLoc);
 661     }
 662 }
 663
 664  /*drl added 8-11-001*/
 665 cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint c) /*@*/
 666 {
 667   cstring string, ret;
 668   fileloc errorLoc;
 669
 670   string = constraint_unparse (c);
 671
 672   errorLoc = constraint_getFileloc (c);
 673
 674   ret = message ("constraint: %q @ %q", string, fileloc_unparse (errorLoc));
 675
 676   fileloc_free (errorLoc);
 677   return ret;
 678
 679 }
 680
 681
 682
 683 void constraint_printError (constraint c, fileloc loc)
 684 {
 685   cstring string;
 686   fileloc errorLoc, temp;
 687
 688   bool isLikely;
 689
 690
 691   llassert (constraint_isDefined (c) );
 692
 693   /*drl 11/26/2001 avoid printing tautological constraints */
 694   if (constraint_isAlwaysTrue (c))
 695     {
 696       return;
 697     }
 698
 699
 700   string = constraint_unparseDetailed (c);
 701
 702   errorLoc = loc;
 703
 704   temp = constraint_getFileloc (c);
 705
 706   if (fileloc_isDefined (temp))
 707     {
 708       errorLoc = temp;
 709     }
 710   else
 711     {
 712       llassert (FALSE);
 713       DPRINTF (("constraint %s had undefined fileloc %s", constraint_unparse (c), fileloc_unparse (temp)));
 714       fileloc_free (temp);
 715       errorLoc = fileloc_copy (errorLoc);
 716     }
 717
 718
 719   if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES ) )
 720     {
 721       string = cstring_replaceChar(string, '\n', ' ');
 722     }
 723
 724   /*drl added 12/19/2002 print
 725     a different error fro "likely" bounds-errors*/
 726
 727   isLikely = constraint_isConstantOnly(c);
 728
 729   if (isLikely)
 730     {
 731       if (c->post)
 732         {
 733           voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
 734         }
 735       else
 736         {
 737           if (constraint_hasMaxSet (c))
 738             {
 739               voptgenerror (FLG_LIKELYBOUNDSWRITE, string, errorLoc);
 740             }
 741           else
 742             {
 743               voptgenerror (FLG_LIKELYBOUNDSREAD, string, errorLoc);
 744             }
 745         }
 746     }
 747   else if (c->post)
 748     {
 749       voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
 750     }
 751   else
 752     {
 753       if (constraint_hasMaxSet (c))
 754         {
 755           voptgenerror (FLG_BOUNDSWRITE, string, errorLoc);
 756         }
 757       else
 758         {
 759           voptgenerror (FLG_BOUNDSREAD, string, errorLoc);
 760         }
 761     }
 762
 763   fileloc_free(errorLoc);
 764 }
 765
 766 static cstring constraint_unparseDeep (constraint c)
 767 {
 768   cstring genExpr;
 769   cstring st;
 770
 771   llassert (constraint_isDefined (c));
 772   st = constraint_unparse (c);
 773
 774   if (c->orig != constraint_undefined)
 775     {
 776       st = cstring_appendChar (st, '\n');
 777       genExpr =  exprNode_unparse (c->orig->generatingExpr);
 778
 779       if (!c->post)
 780         {
 781           if (c->orig->fcnPre)
 782             {
 783               st = cstring_concatFree (st, message (" derived from %s precondition: %q",
 784                                                     genExpr, constraint_unparseDeep (c->orig)));
 785             }
 786           else
 787             {
 788               st = cstring_concatFree (st, message (" needed to satisfy precondition:\n%q",
 789                                                     constraint_unparseDeep (c->orig)));
 790             }
 791         }
 792       else
 793         {
 794           st = cstring_concatFree (st, message ("derived from: %q",
 795                                                constraint_unparseDeep (c->orig)));
 796         }
 797     }
 798
 799   return st;
 800 }
 801
 802
 803 static /*@only@*/ cstring  constraint_unparseDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c)
 804 {
 805   cstring st = cstring_undefined;
 806   cstring genExpr;
 807
 808   llassert (constraint_isDefined (c) );
 809
 810   st = message ("Unsatisfied ensures constraint condition:\nSplint is unable to verify the constraint %q",
 811                 constraint_unparseDeep (c));
 812
 813   genExpr = exprNode_unparse (c->generatingExpr);
 814
 815   if (context_getFlag (FLG_CONSTRAINTLOCATION))
 816     {
 817       cstring temp;
 818
 819       temp = message ("\nOriginal Generating expression %q: %s\n",
 820                       fileloc_unparse ( exprNode_getfileloc (c->generatingExpr)),
 821                       genExpr);
 822       st = cstring_concatFree (st, temp);
 823
 824       if (constraint_hasMaxSet (c))
 825         {
 826           temp = message ("Has MaxSet\n");
 827           st = cstring_concatFree (st, temp);
 828         }
 829     }
 830   return st;
 831 }
 832
 833 cstring  constraint_unparseDetailed (constraint c)
 834 {
 835   cstring st = cstring_undefined;
 836   cstring temp = cstring_undefined;
 837   cstring genExpr;
 838   bool isLikely;
 839
 840   llassert (constraint_isDefined (c) );
 841
 842   if (!c->post)
 843     {
 844       st = message ("Unable to resolve constraint:\n%q", constraint_unparseDeep (c));
 845     }
 846   else
 847     {
 848       st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_unparseDeep (c));
 849     }
 850
 851   isLikely = constraint_isConstantOnly(c);
 852
 853   if (isLikely)
 854     {
 855       if (constraint_hasMaxSet (c))
 856         {
 857           temp = cstring_makeLiteral ("Likely out-of-bounds store:\n");
 858         }
 859       else
 860         {
 861           temp = cstring_makeLiteral ("Likely out-of-bounds read:\n");
 862         }
 863     }
 864   else
 865     {
 866
 867       if (constraint_hasMaxSet (c))
 868         {
 869           temp = cstring_makeLiteral ("Possible out-of-bounds store:\n");
 870         }
 871       else
 872         {
 873           temp = cstring_makeLiteral ("Possible out-of-bounds read:\n");
 874         }
 875     }
 876
 877   genExpr = exprNode_unparse (c->generatingExpr);
 878
 879   if (context_getFlag (FLG_CONSTRAINTLOCATION))
 880     {
 881       cstring temp2;
 882       temp2 = message ("%s\n", genExpr);
 883       temp = cstring_concatFree (temp, temp2);
 884     }
 885
 886   st  = cstring_concatFree (temp,st);
 887
 888   return st;
 889 }
 890
 891 /*@only@*/ cstring  constraint_unparse (constraint c) /*@*/
 892 {
 893   cstring st = cstring_undefined;
 894   cstring type = cstring_undefined;
 895   llassert (c !=NULL);
 896   if (c->post)
 897     {
 898       if (context_getFlag (FLG_PARENCONSTRAINT))
 899         {
 900           type = cstring_makeLiteral ("ensures: ");
 901         }
 902       else
 903         {
 904            type = cstring_makeLiteral ("ensures");
 905         }
 906     }
 907   else
 908     {
 909       if (context_getFlag (FLG_PARENCONSTRAINT))
 910         {
 911           type = cstring_makeLiteral ("requires: ");
 912         }
 913       else
 914         {
 915           type = cstring_makeLiteral ("requires");
 916         }
 917
 918     }
 919       if (context_getFlag (FLG_PARENCONSTRAINT))
 920         {
 921           st = message ("%q: %q %q %q",
 922                         type,
 923                         constraintExpr_print (c->lexpr),
 924                         arithType_print (c->ar),
 925                         constraintExpr_print (c->expr));
 926         }
 927       else
 928         {
 929           st = message ("%q %q %q %q",
 930                         type,
 931                         constraintExpr_print (c->lexpr),
 932                         arithType_print (c->ar),
 933                         constraintExpr_print (c->expr));
 934         }
 935   return st;
 936 }
 937
 938 cstring  constraint_unparseOr (constraint c) /*@*/
 939 {
 940   cstring ret;
 941   constraint temp;
 942
 943   ret = cstring_undefined;
 944
 945   llassert (constraint_isDefined (c) );
 946
 947   temp = c;
 948
 949   ret = cstring_concatFree (ret, constraint_unparse (temp));
 950
 951   temp = temp->or;
 952
 953   while ( constraint_isDefined (temp))
 954     {
 955       ret = cstring_concatFree (ret, cstring_makeLiteral (" OR "));
 956       ret = cstring_concatFree (ret, constraint_unparse (temp));
 957       temp = temp->or;
 958     }
 959
 960   return ret;
 961
 962 }
 963
 964 /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
 965                                                    exprNodeList arglist)
 966 {
 967
 968   llassert (constraint_isDefined (precondition) );
 969
 970   precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
 971                                                            arglist);
 972   precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
 973                                                            arglist);
 974
 975   return precondition;
 976 }
 977
 978
 979 constraint constraint_doFixResult (constraint postcondition, /*@dependent@*/ exprNode fcnCall)
 980 {
 981   postcondition = constraint_copy (postcondition);
 982
 983   llassert (constraint_isDefined (postcondition) );
 984
 985
 986   postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
 987   postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
 988
 989   return postcondition;
 990 }
 991 /*Commenting out temporally
 992
 993 / *@only@* /constraint  constraint_doSRefFixInvarConstraint(constraint invar, sRef s, ctype ct )
 994 {
 995
 996   invar = constraint_copy (invar);
 997   invar->lexpr = constraintExpr_doSRefFixInvarConstraint (invar->lexpr, s, ct);
 998   invar->expr = constraintExpr_doSRefFixInvarConstraint (invar->expr, s, ct);
 999
1000   return invar;
1001 }
1002 */
1003
1004 /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition,
1005                                                    exprNodeList arglist)
1006 {
1007
1008   precondition = constraint_copy (precondition);
1009
1010   llassert (constraint_isDefined (precondition) );
1011
1012   precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
1013   precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
1014
1015   precondition->fcnPre = FALSE;
1016   return constraint_simplify(precondition);
1017 }
1018
1019 constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/
1020 {
1021   DPRINTF (("Doing constraint_preserverOrig for %q", constraint_printDetailed (c)));
1022   llassert (constraint_isDefined (c));
1023
1024   if (c->orig == constraint_undefined)
1025     {
1026       c->orig = constraint_copy (c);
1027     }
1028   else if (c->orig->fcnPre)
1029     {
1030       constraint temp = c->orig;
1031
1032       /* avoid infinite loop */
1033       c->orig = NULL;
1034       c->orig = constraint_copy (c);
1035       /*drl 03/2/2003 if c != NULL then the copy of c will != null*/
1036       llassert (constraint_isDefined (c->orig) );
1037
1038       if (c->orig->orig == NULL)
1039         {
1040           c->orig->orig = temp;
1041           temp = NULL;
1042         }
1043       else
1044         {
1045           llcontbug ((message ("Expected c->orig->orig to be null")));
1046           constraint_free (c->orig->orig);
1047           c->orig->orig = temp;
1048           temp = NULL;
1049         }
1050     }
1051   else
1052     {
1053       DPRINTF (("Not changing constraint"));
1054     }
1055
1056   DPRINTF ((message ("After Doing constraint_preserverOrig for %q ", constraint_unparseDetailed (c))));
1057   return c;
1058 }
1059
1060 constraint constraint_togglePost (/*@returned@*/ constraint c)
1061 {
1062   llassert (constraint_isDefined (c));
1063   c->post = !c->post;
1064   return c;
1065 }
1066
1067 constraint constraint_togglePostOrig (/*@returned@*/ constraint c)
1068 {
1069   llassert (constraint_isDefined (c));
1070
1071   if (c->orig != NULL)
1072     {
1073       c->orig = constraint_togglePost (c->orig);
1074     }
1075
1076   return c;
1077 }
1078
1079 bool constraint_hasOrig ( /*@observer@*/ /*@temp@*/ constraint c)
1080 {
1081   llassert (constraint_isDefined (c));
1082   return (c->orig != NULL);
1083 }
1084
1085
1086 constraint constraint_undump (FILE *f)
1087 {
1088   constraint c;
1089   bool fcnPre, post;
1090   arithType ar;
1091   constraintExpr lexpr, expr;
1092   char *s, *os;
1093
1094   os = mstring_create (MAX_DUMP_LINE_LENGTH);
1095   s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
1096
1097   if (!mstring_isDefined (s))
1098     {
1099       llfatalbug (message ("Library file is corrupted") );
1100     }
1101
1102   fcnPre = (bool) reader_getInt (&s);
1103   advanceField (&s);
1104   post = (bool) reader_getInt (&s);
1105   advanceField (&s);
1106   ar = (arithType) reader_getInt (&s);
1107
1108   s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
1109
1110   if (! mstring_isDefined(s) )
1111     {
1112       llfatalbug(message("Library file is corrupted") );
1113     }
1114
1115   reader_checkChar (&s, 'l');
1116
1117   lexpr = constraintExpr_undump (f);
1118
1119   s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
1120
1121   reader_checkChar (&s, 'r');
1122
1123   if (! mstring_isDefined(s) )
1124     {
1125       llfatalbug(message("Library file is corrupted") );
1126     }
1127
1128   expr = constraintExpr_undump (f);
1129
1130   c = constraint_makeNew ();
1131
1132   c->fcnPre = fcnPre;
1133   c->post = post;
1134   c->ar = ar;
1135
1136   c->lexpr = lexpr;
1137   c->expr =  expr;
1138
1139   free (os);
1140   c = constraint_preserveOrig (c);
1141   return c;
1142 }
1143
1144
1145 void constraint_dump (/*@observer@*/ constraint c,  FILE *f)
1146 {
1147   bool           fcnPre;
1148   bool post;
1149   arithType       ar;
1150
1151   constraintExpr lexpr;
1152   constraintExpr  expr;
1153
1154   llassert (constraint_isDefined (c) );
1155
1156   fcnPre = c->fcnPre;
1157   post   = c->post;
1158   ar     = c->ar;
1159   lexpr = c->lexpr;
1160   expr = c->expr;
1161
1162   fprintf (f, "%d@%d@%d\n", (int) fcnPre, (int) post, (int) ar);
1163   fprintf (f,"l\n");
1164   constraintExpr_dump (lexpr, f);
1165   fprintf (f,"r\n");
1166   constraintExpr_dump (expr, f);
1167 }
1168
1169
1170 int constraint_compare (/*@observer@*/ /*@temp@*/ const constraint * c1, /*@observer@*/ /*@temp@*/ const constraint * c2) /*@*/
1171 {
1172   fileloc loc1, loc2;
1173
1174   int ret;
1175
1176   llassert (constraint_isDefined (*c1));
1177   llassert (constraint_isDefined (*c2));
1178
1179   if (constraint_isUndefined (*c1))
1180     {
1181         if (constraint_isUndefined (*c2))
1182           return 0;
1183         else
1184           return 1;
1185     }
1186
1187   if (constraint_isUndefined (*c2))
1188     {
1189       return -1;
1190     }
1191
1192   loc1 = constraint_getFileloc (*c1);
1193   loc2 = constraint_getFileloc (*c2);
1194
1195   ret = fileloc_compare (loc1, loc2);
1196
1197   fileloc_free (loc1);
1198   fileloc_free (loc2);
1199
1200   return ret;
1201 }
1202
1203
1204 bool constraint_isPost  (/*@observer@*/ /*@temp@*/ constraint c)
1205 {
1206   llassert (constraint_isDefined (c));
1207
1208   if (constraint_isUndefined (c))
1209     return FALSE;
1210
1211   return (c->post);
1212 }
1213
1214
1215 static int constraint_getDepth (/*@observer@*/ /*@temp@*/ constraint c)
1216 {
1217   int l , r;
1218
1219   llassert (constraint_isDefined (c) );
1220
1221   l = constraintExpr_getDepth (c->lexpr);
1222   r = constraintExpr_getDepth (c->expr);
1223
1224   if (l > r)
1225     {
1226       DPRINTF (( message ("constraint depth returning %d for %s", l, constraint_unparse (c))));
1227       return l;
1228     }
1229   else
1230     {
1231       DPRINTF (( message ("constraint depth returning %d for %s", r, constraint_unparse (c))));
1232       return r;
1233     }
1234 }
1235
1236
1237 bool constraint_tooDeep (/*@observer@*/ /*@temp@*/ constraint c)
1238 {
1239   int temp;
1240
1241   temp = constraint_getDepth (c);
1242
1243   if (temp >= 20)
1244     {
1245       return TRUE;
1246     }
1247
1248   return FALSE;
1249
1250 }
1251
1252 /*drl added 12/19/2002*/
1253 /*whether constraints consist only of
1254   terms which are constants*/
1255 bool constraint_isConstantOnly (constraint c)
1256 {
1257   bool l, r;
1258
1259   llassert (constraint_isDefined (c) );
1260
1261   l = constraintExpr_isConstantOnly(c->lexpr);
1262   r = constraintExpr_isConstantOnly(c->expr);
1263
1264   if (l && r)
1265     {
1266       return TRUE;
1267     }
1268
1269   else
1270     {
1271       return FALSE;
1272     }
1273
1274 }