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