src/constraint.c

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