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