src/constraint.c

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