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 "aliasChecks.h"
  15 # include "exprNodeSList.h"
  16
  17 /*@i33*/
  18 /*@-fcnuse*/
  19 /*@-assignexpose*/
  20
  21 /*@access exprNode @*/
  22
  23
  24 static /*@only@*/ cstring  constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c);
  25
  26
  27 static /*@notnull@*/  /*@special@*/ constraint constraint_makeNew (void)
  28      /*@post:isnull result->or, result->orig,  result->generatingExpr, result->fcnPre @*/ /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/;
  29
  30 /*  constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant) */
  31
  32 /*  { */
  33 /*    char *t; */
  34 /*    int c; */
  35 /*    constraint ret; */
  36 /*    ret = constraint_makeNew(); */
  37 /*    llassert (sRef_isValid(x) ); */
  38 /*    if (!sRef_isValid(x)) */
  39 /*      return ret; */
  40
  41
  42 /*    ret->lexpr = constraintExpr_makeTermsRef (x); */
  43 /*    #warning fix abstraction */
  44
  45 /*    if (relOp.tok == GE_OP) */
  46 /*        ret->ar = GTE; */
  47 /*    else if (relOp.tok == LE_OP) */
  48 /*      ret->ar = LTE; */
  49 /*    else if (relOp.tok == EQ_OP) */
  50 /*      ret->ar = EQ; */
  51 /*    else */
  52 /*      llfatalbug(message ("Unsupported relational operator") ); */
  53
  54
  55 /*    t =  cstring_toCharsSafe (exprNode_unparse(cconstant)); */
  56 /*    c = atoi( t ); */
  57 /*    ret->expr = constraintExpr_makeIntLiteral (c); */
  58
  59 /*    ret->post = TRUE; */
  60 /*    //  ret->orig = ret; */
  61 /*    DPRINTF(("GENERATED CONSTRAINT:")); */
  62 /*    DPRINTF( (message ("%s", constraint_print(ret) ) ) ); */
  63 /*    return ret; */
  64 /*  } */
  65
  66 constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
  67 {
  68   char *t;
  69   int c;
  70   constraint ret;
  71   ret = constraint_makeNew();
  72   llassert (l!=NULL);
  73
  74   ret->lexpr = constraintExpr_copy (l);
  75
  76
  77   if (relOp.tok == GE_OP)
  78       ret->ar = GTE;
  79   else if (relOp.tok == LE_OP)
  80     ret->ar = LTE;
  81   else if (relOp.tok == EQ_OP)
  82     ret->ar = EQ;
  83   else
  84   llfatalbug(message("Unsupported relational operator") );
  85
  86
  87   t =  cstring_toCharsSafe (exprNode_unparse(cconstant));
  88   c = atoi( t );
  89   ret->expr = constraintExpr_makeIntLiteral (c);
  90
  91   ret->post = TRUE;
  92   //  ret->orig = ret;
  93   DPRINTF(("GENERATED CONSTRAINT:"));
  94   DPRINTF( (message ("%s", constraint_print(ret) ) ) );
  95   return ret;
  96 }
  97
  98 bool constraint_same (constraint c1, constraint c2)
  99 {
 100
 101   if (c1->ar != c2->ar)
 102     return FALSE;
 103
 104   if (!constraintExpr_similar (c1->lexpr, c2->lexpr) )
 105     return FALSE;
 106
 107   if (!constraintExpr_similar (c1->expr, c2->expr) )
 108     return FALSE;
 109
 110   return TRUE;
 111 }
 112
 113 constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)
 114 {
 115   constraint ret;
 116   ret = constraint_makeNew();
 117   llassert (l !=NULL);
 118
 119   ret->lexpr = constraintExpr_copy (l);
 120
 121   if (relOp.tok == GE_OP)
 122       ret->ar = GTE;
 123   else if (relOp.tok == LE_OP)
 124     ret->ar = LTE;
 125   else if (relOp.tok == EQ_OP)
 126     ret->ar = EQ;
 127   else
 128   llfatalbug( message("Unsupported relational operator") );
 129
 130   ret->expr = constraintExpr_copy (r);
 131
 132   ret->post = TRUE;
 133
 134   ret->orig = constraint_copy(ret);
 135
 136   ret = constraint_simplify (ret);
 137
 138   //  ret->orig = ret;
 139   DPRINTF(("GENERATED CONSTRAINT:"));
 140   DPRINTF( (message ("%s", constraint_print(ret) ) ) );
 141   return ret;
 142 }
 143
 144 constraint constraint_copy (constraint c)
 145 {
 146   constraint ret;
 147
 148   llassert (constraint_isDefined(c) );
 149   // TPRINTF((message("Copying constraint %q", constraint_print) ));
 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   ret->generatingExpr = exprNode_fakeCopy(c->generatingExpr);
 157
 158   /*@i33 fix this*/
 159   if (c->orig != NULL)
 160     ret->orig = constraint_copy (c->orig);
 161   else
 162     ret->orig = NULL;
 163
 164   if (c->or != NULL)
 165     ret->or = constraint_copy (c->or);
 166   else
 167     ret->or = NULL;
 168
 169   ret->fcnPre = c->fcnPre;
 170
 171   return ret;
 172 }
 173
 174 /*like copy expect it doesn't allocate memory for the constraint*/
 175
 176 void constraint_overWrite (constraint c1, constraint c2)
 177 {
 178   llassert (constraint_isDefined(c1) );
 179
 180   llassert (c1 != c2);
 181
 182   DPRINTF((message("OverWriteing constraint %q with %q", constraint_print(c1),
 183                    constraint_print(c2) ) ));
 184
 185   constraintExpr_free(c1->lexpr);
 186   constraintExpr_free(c1->expr);
 187
 188   c1->lexpr = constraintExpr_copy (c2->lexpr);
 189   c1->ar = c2->ar;
 190   c1->expr =  constraintExpr_copy (c2->expr);
 191   c1->post = c2->post;
 192
 193   if (c1->orig != NULL)
 194     constraint_free (c1->orig);
 195
 196   if (c2->orig != NULL)
 197     c1->orig = constraint_copy (c2->orig);
 198   else
 199     c1->orig = NULL;
 200
 201   /*@i33 make sure that the or is freed correctly*/
 202   if (c1->or != NULL)
 203     constraint_free (c1->or);
 204
 205   if (c2->or != NULL)
 206     c1->or = constraint_copy (c2->or);
 207   else
 208     c1->or = NULL;
 209
 210   c1->fcnPre = c2->fcnPre;
 211
 212   c1->generatingExpr = c2->generatingExpr;
 213 }
 214
 215
 216
 217 static /*@notnull@*/  /*@special@*/ constraint constraint_makeNew (void)
 218      /*@post:isnull result->or, result->orig,  result->generatingExpr, result->fcnPre @*/ /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/
 219 {
 220   constraint ret;
 221   ret = dmalloc(sizeof (*ret) );
 222   ret->lexpr = NULL;
 223   ret->expr = NULL;
 224   ret->ar = LT;
 225   ret->post = FALSE;
 226   ret->orig = NULL;
 227   ret->or = NULL;
 228   ret->generatingExpr = NULL;
 229   ret->fcnPre = NULL;
 230   return ret;
 231 }
 232
 233 constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
 234 {
 235
 236   if (c->generatingExpr == NULL)
 237     {
 238       c->generatingExpr = exprNode_fakeCopy(e);
 239       DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
 240     }
 241   else
 242     {
 243       DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
 244     }
 245   return c;
 246 }
 247
 248 constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
 249 {
 250
 251   if (c->orig != constraint_undefined)
 252     {
 253       c->orig = constraint_addGeneratingExpr(c->orig, e);
 254     }
 255   else
 256     {
 257       DPRINTF ((message ("constraint_origAddGeneratingExpr: Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
 258     }
 259   return c;
 260 }
 261
 262 constraint constraint_setFcnPre (/*@returned@*/ constraint c )
 263 {
 264
 265   if (c->orig != constraint_undefined)
 266     {
 267       c->orig->fcnPre = TRUE;
 268     }
 269   else
 270     {
 271       c->fcnPre = TRUE;
 272       TPRINTF(( message("Warning Setting fcnPre directly") ));
 273     }
 274   return c;
 275 }
 276
 277
 278
 279
 280 fileloc constraint_getFileloc (constraint c)
 281 {
 282   if (exprNode_isDefined(c->generatingExpr) )
 283     return (fileloc_copy (exprNode_getfileloc (c->generatingExpr) ) );
 284
 285   return (constraintExpr_getFileloc (c->lexpr) );
 286
 287
 288 }
 289
 290 static bool checkForMaxSet (constraint c)
 291 {
 292   if (constraintExpr_hasMaxSet(c->lexpr) || constraintExpr_hasMaxSet(c->expr) )
 293     return TRUE;
 294
 295   return FALSE;
 296 }
 297
 298 bool constraint_hasMaxSet(constraint c)
 299 {
 300   if (c->orig != NULL)
 301     {
 302       if (checkForMaxSet(c->orig) )
 303         return TRUE;
 304     }
 305
 306   return (checkForMaxSet(c) );
 307 }
 308
 309 constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
 310 {
 311   constraint ret = constraint_makeNew();
 312   //  constraintTerm term;
 313   po = exprNode_fakeCopy(po);
 314   ind = exprNode_fakeCopy(ind);
 315   ret->lexpr = constraintExpr_makeMaxReadExpr(po);
 316   ret->ar    = GTE;
 317   ret->expr  = constraintExpr_makeValueExpr (ind);
 318   ret->post = FALSE;
 319   return ret;
 320 }
 321
 322 constraint constraint_makeWriteSafeInt (exprNode po, int ind)
 323 {
 324   constraint ret = constraint_makeNew();
 325
 326
 327   ret->lexpr =constraintExpr_makeMaxSetExpr(po);
 328   ret->ar = GTE;
 329   ret->expr =  constraintExpr_makeIntLiteral (ind);
 330   /*@i1*/return ret;
 331 }
 332
 333 constraint constraint_makeSRefSetBufferSize (sRef s, long int size)
 334 {
 335  constraint ret = constraint_makeNew();
 336  ret->lexpr = constraintExpr_makeSRefMaxset (s);
 337  ret->ar = EQ;
 338  ret->expr =  constraintExpr_makeIntLiteral ((int)size);
 339  ret->post = TRUE;
 340  /*@i1*/return ret;
 341 }
 342
 343 constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
 344 {
 345   constraint ret = constraint_makeNew();
 346
 347
 348   ret->lexpr = constraintExpr_makeSRefMaxset ( s );
 349   ret->ar = GTE;
 350   ret->expr =  constraintExpr_makeIntLiteral (ind);
 351   ret->post = TRUE;
 352   /*@i1*/return ret;
 353 }
 354
 355 /* drl added 01/12/2000
 356
 357   makes the constraint: Ensures index <= MaxRead(buffer) */
 358
 359 constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer)
 360 {
 361   constraint ret = constraint_makeNew();
 362
 363   ret->lexpr = constraintExpr_makeValueExpr (index);
 364   ret->ar = LTE;
 365   ret->expr = constraintExpr_makeMaxReadExpr(buffer);
 366   ret->post = TRUE;
 367   return ret;
 368 }
 369
 370 constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
 371 {
 372   constraint ret = constraint_makeNew();
 373
 374
 375   ret->lexpr =constraintExpr_makeMaxSetExpr(po);
 376   ret->ar = GTE;
 377   ret->expr =  constraintExpr_makeValueExpr (ind);
 378   /*@i1*/return ret;
 379 }
 380
 381
 382 constraint constraint_makeReadSafeInt ( exprNode po, int ind)
 383 {
 384   constraint ret = constraint_makeNew();
 385
 386   po = exprNode_fakeCopy(po);
 387
 388   ret->lexpr = constraintExpr_makeMaxReadExpr(po);
 389   ret->ar    = GTE;
 390   ret->expr  = constraintExpr_makeIntLiteral (ind);
 391   ret->post = FALSE;
 392   return ret;
 393 }
 394
 395 constraint constraint_makeSRefReadSafeInt (sRef s, int ind)
 396 {
 397   constraint ret = constraint_makeNew();
 398
 399
 400   ret->lexpr = constraintExpr_makeSRefMaxRead (s );
 401   ret->ar = GTE;
 402   ret->expr =  constraintExpr_makeIntLiteral (ind);
 403   ret->post = TRUE;
 404   /*@i1*/return ret;
 405 }
 406
 407 constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
 408 {
 409   constraint ret;
 410
 411   e1 = exprNode_fakeCopy (e1);
 412   t2 = exprNode_fakeCopy (t2);
 413
 414   ret = constraint_makeReadSafeExprNode(e1, t2);
 415
 416   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 417
 418   ret->post = TRUE;
 419
 420   //  fileloc_incColumn (ret->lexpr->term->loc);
 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(c1 && c2);
 430   //  llassert(sequencePoint);
 431
 432   ret = constraint_makeNew();
 433
 434   ret->lexpr = c1;
 435   ret->ar = ar;
 436   ret->post = TRUE;
 437   ret->expr =  c2;
 438   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 439   return ret;
 440 }
 441
 442 static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint,  arithType  ar)
 443 {
 444   constraintExpr c1, c2;
 445   constraint ret;
 446   exprNode e;
 447
 448   if (! (e1 && e2) )
 449     {
 450       llcontbug((message("null exprNode, Exprnodes are %s and %s",
 451                        exprNode_unparse(e1), exprNode_unparse(e2) )
 452                ));
 453     }
 454
 455   //  llassert (sequencePoint);
 456
 457   e  =  exprNode_fakeCopy(e1);
 458   c1 =  constraintExpr_makeValueExpr (e);
 459
 460   e  =  exprNode_fakeCopy(e2);
 461   c2 =  constraintExpr_makeValueExpr (e);
 462
 463   ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
 464
 465   return ret;
 466 }
 467
 468
 469 /* make constraint ensures e1 == e2 */
 470
 471 constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 472 {
 473   return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) );
 474 }
 475
 476 /*make constraint ensures e1 < e2 */
 477 constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 478 {
 479   constraintExpr t1, t2;
 480
 481   t1 = constraintExpr_makeValueExpr (e1);
 482   t2 = constraintExpr_makeValueExpr (e2);
 483
 484   /*change this to e1 <= (e2 -1) */
 485
 486   t2 = constraintExpr_makeDecConstraintExpr (t2);
 487
 488  return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE) );
 489 }
 490
 491 constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 492 {
 493  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) );
 494 }
 495
 496 constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 497 {
 498   constraintExpr t1, t2;
 499
 500   t1 = constraintExpr_makeValueExpr (e1);
 501   t2 = constraintExpr_makeValueExpr (e2);
 502
 503
 504   /* change this to e1 >= (e2 + 1) */
 505   t2 = constraintExpr_makeIncConstraintExpr (t2);
 506
 507
 508  return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE) );
 509 }
 510
 511 constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 512 {
 513  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) );
 514 }
 515
 516
 517 exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
 518 {
 519   constraintList_free(dst->ensuresConstraints);
 520   constraintList_free(dst->requiresConstraints);
 521   constraintList_free(dst->trueEnsuresConstraints);
 522   constraintList_free(dst->falseEnsuresConstraints);
 523
 524   dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
 525   dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
 526   dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
 527   dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints );
 528   return dst;
 529 }
 530
 531 /* Makes the constraint e = e + f */
 532 constraint constraint_makeAddAssign (exprNode e, exprNode f, fileloc sequencePoint)
 533 {
 534   constraintExpr x1, x2, y;
 535   constraint ret;
 536
 537   ret = constraint_makeNew();
 538
 539   x1 =  constraintExpr_makeValueExpr (e);
 540   x2 =  constraintExpr_copy(x1);
 541   y  =  constraintExpr_makeValueExpr (f);
 542
 543   ret->lexpr = x1;
 544   ret->ar = EQ;
 545   ret->post = TRUE;
 546   ret->expr = constraintExpr_makeAddExpr (x2, y);
 547
 548   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 549
 550   return ret;
 551 }
 552
 553
 554 /* Makes the constraint e = e - f */
 555 constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequencePoint)
 556 {
 557   constraintExpr x1, x2, y;
 558   constraint ret;
 559
 560   ret = constraint_makeNew();
 561
 562   x1 =  constraintExpr_makeValueExpr (e);
 563   x2 =  constraintExpr_copy(x1);
 564   y  =  constraintExpr_makeValueExpr (f);
 565
 566   ret->lexpr = x1;
 567   ret->ar = EQ;
 568   ret->post = TRUE;
 569   ret->expr = constraintExpr_makeSubtractExpr (x2, y);
 570
 571   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 572
 573   return ret;
 574 }
 575
 576 constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
 577 {
 578   constraint ret = constraint_makeNew();
 579   //constraintTerm term;
 580
 581   e = exprNode_fakeCopy(e);
 582   ret->lexpr = constraintExpr_makeValueExpr (e);
 583   ret->ar = EQ;
 584   ret->post = TRUE;
 585   ret->expr =  constraintExpr_makeValueExpr (e);
 586   ret->expr =  constraintExpr_makeDecConstraintExpr (ret->expr);
 587
 588   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 589 //   fileloc_incColumn (  ret->lexpr->term->loc);
 590 //   fileloc_incColumn (  ret->lexpr->term->loc);
 591   return ret;
 592 }
 593 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 594 {
 595   constraint ret = constraint_makeNew();
 596   //constraintTerm term;
 597
 598   e = exprNode_fakeCopy(e);
 599   ret->lexpr = constraintExpr_makeValueExpr (e);
 600   ret->ar = EQ;
 601   ret->post = TRUE;
 602   ret->expr =  constraintExpr_makeValueExpr (e);
 603   ret->expr =  constraintExpr_makeIncConstraintExpr (ret->expr);
 604
 605   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 606 //   fileloc_incColumn (  ret->lexpr->term->loc);
 607 //   fileloc_incColumn (  ret->lexpr->term->loc);
 608   return ret;
 609 }
 610
 611
 612 void constraint_free (/*@only@*/ /*@notnull@*/ constraint c)
 613 {
 614   llassert(constraint_isDefined (c) );
 615
 616
 617   if (constraint_isDefined(c->orig) )
 618     constraint_free (c->orig);
 619   if ( constraint_isDefined(c->or) )
 620     constraint_free (c->or);
 621
 622
 623   constraintExpr_free(c->lexpr);
 624   constraintExpr_free(c->expr);
 625
 626   c->orig = NULL;
 627   c->or = NULL;
 628   c->lexpr = NULL;
 629   c->expr  = NULL;
 630
 631   free (c);
 632
 633 }
 634
 635
 636 // constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 637 // {
 638 //   constraint ret = constraint_makeNew();
 639 //   //constraintTerm term;
 640
 641 //   e = exprNode_fakeCopy(e);
 642 //   ret->lexpr = constraintExpr_makeMaxReadExpr(e);
 643 //   ret->ar = EQ;
 644 //   ret->post = TRUE;
 645 //   ret->expr = constraintExpr_makeIncConstraintExpr (e);
 646 //   ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint);
 647 //   return ret;
 648 // }
 649
 650
 651 cstring arithType_print (arithType ar) /*@*/
 652 {
 653   cstring st = cstring_undefined;
 654   switch (ar)
 655     {
 656     case LT:
 657       st = cstring_makeLiteral (" < ");
 658       break;
 659     case        LTE:
 660       st = cstring_makeLiteral (" <= ");
 661       break;
 662     case        GT:
 663       st = cstring_makeLiteral (" > ");
 664       break;
 665     case        GTE:
 666       st = cstring_makeLiteral (" >= ");
 667       break;
 668     case        EQ:
 669       st = cstring_makeLiteral (" == ");
 670       break;
 671     case        NONNEGATIVE:
 672       st = cstring_makeLiteral (" NONNEGATIVE ");
 673       break;
 674     case        POSITIVE:
 675       st = cstring_makeLiteral (" POSITIVE ");
 676       break;
 677     default:
 678       llassert(FALSE);
 679       break;
 680     }
 681   return st;
 682 }
 683
 684 void constraint_printErrorPostCondition (constraint c, fileloc loc)
 685 {
 686   cstring string;
 687   fileloc errorLoc, temp;
 688
 689   string = constraint_printDetailedPostCondition (c);
 690
 691   errorLoc = loc;
 692
 693   loc = NULL;
 694
 695   temp = constraint_getFileloc(c);
 696
 697   if (fileloc_isDefined(temp) )
 698     {
 699       errorLoc = temp;
 700       voptgenerror (  FLG_CHECKPOST, string, errorLoc);
 701       fileloc_free(temp);
 702     }
 703   else
 704     {
 705       voptgenerror (  FLG_CHECKPOST, string, errorLoc);
 706     }
 707 }
 708
 709
 710
 711
 712 void constraint_printError (constraint c, fileloc loc)
 713 {
 714   cstring string;
 715   fileloc errorLoc, temp;
 716
 717   string = constraint_printDetailed (c);
 718
 719   errorLoc = loc;
 720
 721   loc = NULL;
 722
 723   temp = constraint_getFileloc(c);
 724
 725   if (fileloc_isDefined(temp) )
 726     {
 727       errorLoc = temp;
 728
 729       if (c->post)
 730         {
 731           voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
 732         }
 733       else
 734         {
 735           voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
 736         }
 737       fileloc_free(temp);
 738     }
 739   else
 740     {
 741       if (c->post)
 742         {
 743           voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
 744         }
 745       else
 746         {
 747           voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
 748         }
 749     }
 750 }
 751
 752
 753 cstring constraint_printDeep (constraint c)
 754 {
 755   cstring st = cstring_undefined;
 756
 757   st = constraint_print(c);
 758
 759   if (c->orig != constraint_undefined)
 760     {
 761       if (!c->post)
 762         {
 763           if (c->orig->fcnPre)
 764             st = cstring_concatFree(st, (message(" derived from %s precondition: %q", exprNode_unparse(c->orig->generatingExpr), constraint_printDeep(c->orig) )
 765                                          ) );
 766           else
 767             st = cstring_concatFree(st,(message(" needed to satisfy %q",
 768                                                 constraint_printDeep(c->orig) )
 769                                         ) );
 770
 771         }
 772       else
 773         {
 774           st = cstring_concatFree(st,(message("derived from: %q",
 775                                               constraint_printDeep(c->orig) )
 776                                       ) );
 777         }
 778     }
 779
 780   return st;
 781
 782 }
 783
 784
 785 static /*@only@*/ cstring  constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c)
 786 {
 787   cstring st = cstring_undefined;
 788
 789   st = message ("Unsatisfied ensures constraint condition:\nLCLint is unable to verify the constraint %q", constraint_printDeep (c) );
 790
 791   if (context_getFlag (FLG_CONSTRAINTLOCATION) )
 792     {
 793       cstring temp;
 794       // llassert (c->generatingExpr);
 795       temp = message ("\nOriginal Generating expression %q: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
 796                       exprNode_unparse(c->generatingExpr) );
 797       st = cstring_concatFree (st, temp);
 798
 799       if (constraint_hasMaxSet(c) )
 800         {
 801           temp = message ("Has MaxSet\n");
 802           st = cstring_concatFree (st, temp);
 803         }
 804     }
 805   return st;
 806 }
 807
 808 cstring  constraint_printDetailed (constraint c)
 809 {
 810   cstring st = cstring_undefined;
 811
 812   if (!c->post)
 813     {
 814       st = message ("Unresolved constraint:\nLclint is unable to resolve %q", constraint_printDeep (c) );
 815     }
 816   else
 817     {
 818       st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_printDeep (c) );
 819     }
 820
 821   if (context_getFlag (FLG_CONSTRAINTLOCATION) )
 822     {
 823       cstring temp;
 824       // llassert (c->generatingExpr);
 825       temp = message ("\nOriginal Generating expression %q: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
 826                       exprNode_unparse(c->generatingExpr) );
 827       st = cstring_concatFree (st, temp);
 828
 829       if (constraint_hasMaxSet(c) )
 830         {
 831           temp = message ("Has MaxSet\n");
 832           st = cstring_concatFree (st, temp);
 833         }
 834     }
 835   return st;
 836 }
 837
 838 /*@only@*/ cstring  constraint_print (constraint c) /*@*/
 839 {
 840   cstring st = cstring_undefined;
 841   cstring type = cstring_undefined;
 842   llassert (c !=NULL);
 843   if (c->post)
 844     {
 845       type = cstring_makeLiteral ("Ensures: ");
 846     }
 847   else
 848     {
 849       type = cstring_makeLiteral ("Requires: ");
 850     }
 851   st = message ("%q: %q %q %q",
 852                 type,
 853                 constraintExpr_print (c->lexpr),
 854                 arithType_print(c->ar),
 855                 constraintExpr_print(c->expr)
 856                 );
 857   return st;
 858 }
 859
 860 cstring  constraint_printOr (constraint c) /*@*/
 861 {
 862   cstring ret;
 863   constraint temp;
 864
 865   ret = cstring_undefined;
 866   temp = c;
 867
 868   ret = cstring_concatFree (ret, constraint_print(temp) );
 869
 870   temp = temp->or;
 871
 872   while ( constraint_isDefined(temp) )
 873     {
 874       ret = cstring_concatFree (ret, cstring_makeLiteral (" OR ") );
 875       ret = cstring_concatFree (ret, constraint_print(temp) );
 876       temp = temp->or;
 877     }
 878
 879   return ret;
 880
 881 }
 882
 883 /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
 884                                                    exprNodeList arglist)
 885 {
 886   precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
 887                                                            arglist);
 888   precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
 889                                                            arglist);
 890
 891   return precondition;
 892 }
 893
 894
 895 constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall)
 896 {
 897   postcondition = constraint_copy (postcondition);
 898   postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
 899   postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
 900
 901   return postcondition;
 902 }
 903
 904 /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition,
 905                                                    exprNodeList arglist)
 906 {
 907
 908   precondition = constraint_copy (precondition);
 909   precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
 910   precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
 911
 912   precondition->fcnPre = FALSE;
 913   return precondition;
 914 }
 915
 916 // bool constraint_hasTerm (constraint c, constraintTerm term)
 917 // {
 918 //   DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );
 919
 920 //   if (constraintExpr_includesTerm (c->lexpr, term) )
 921 //     return TRUE;
 922
 923 //   if (constraintExpr_includesTerm (c->expr, term) )
 924 //     return TRUE;
 925
 926 //   return FALSE;
 927 // }
 928
 929 constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/
 930 {
 931
 932   DPRINTF( (message("Doing constraint_preserverOrig for %q ", constraint_printDetailed(c) ) ));
 933
 934   if (c->orig == constraint_undefined)
 935     c->orig = constraint_copy (c);
 936
 937   else if (c->orig->fcnPre)
 938     {
 939       constraint temp;
 940
 941       temp = c->orig;
 942
 943       /* avoid infinite loop */
 944       c->orig = NULL;
 945       c->orig = constraint_copy (c);
 946       if (c->orig->orig == NULL)
 947         c->orig->orig = temp;
 948       else
 949         llcontbug((message("Expected c->orig->orig to be null" ) ));
 950     }
 951   else
 952     {
 953       DPRINTF( (message("Not changing constraint") ));
 954     }
 955
 956   DPRINTF( (message("After Doing constraint_preserverOrig for %q ", constraint_printDetailed(c) ) ));
 957
 958   return c;
 959 }
 960 /*@=fcnuse*/
 961 /*@=assignexpose*/
 962 /*@=czechfcns@*/
 963
 964
 965 constraint constraint_togglePost (/*@returned@*/ constraint c)
 966 {
 967   c->post = !c->post;
 968   return c;
 969 }
 970
 971 constraint constraint_togglePostOrig (/*@returned@*/ constraint c)
 972 {
 973   if (c->orig != NULL)
 974     c->orig = constraint_togglePost(c->orig);
 975   return c;
 976 }
 977
 978 bool constraint_hasOrig( /*@observer@*/ /*@temp@*/ constraint c)
 979 {
 980   if (c->orig == NULL)
 981     return FALSE;
 982   else
 983     return TRUE;
 984 }