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