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