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