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