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