src/constraintGeneration.c

   1
   2 /*
   3 ** constraintGeneration.c
   4 */
   5
   6 //#define DEBUGPRINT 1
   7
   8 # include <ctype.h> /* for isdigit */
   9 # include "lclintMacros.nf"
  10 # include "basic.h"
  11 # include "cgrammar.h"
  12 # include "cgrammar_tokens.h"
  13
  14 # include "exprChecks.h"
  15 # include "aliasChecks.h"
  16 # include "exprNodeSList.h"
  17
  18 # include "exprData.i"
  19 # include "exprDataQuite.i"
  20
  21 bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e);
  22 static bool exprNode_handleError( exprNode p_e);
  23
  24 //static cstring exprNode_findConstraints ( exprNode p_e);
  25 static bool exprNode_isMultiStatement(exprNode p_e);
  26 static bool exprNode_multiStatement (exprNode p_e);
  27 bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv,  fileloc sequencePoint);
  28 //static void exprNode_constraintPropagateUp (exprNode p_e);
  29 constraintList exprNode_traversRequiresConstraints (exprNode e);
  30 constraintList exprNode_traversEnsuresConstraints (exprNode e);
  31
  32 constraintList exprNode_traversTrueEnsuresConstraints (exprNode e);
  33
  34 extern constraintList reflectChanges (constraintList pre2, constraintList post1);
  35
  36 void mergeResolve (exprNode parent, exprNode child1, exprNode child2);
  37 exprNode makeDataTypeConstraints (exprNode e);
  38 constraintList constraintList_makeFixedArrayConstraints (sRefSet s);
  39 constraintList checkCall (exprNode fcn, exprNodeList arglist);
  40
  41 //bool exprNode_testd()
  42 //{
  43   /*        if ( ( (exprNode_isError  ) ) )
  44           {
  45           }
  46         if ( ( (e_1  ) ) )
  47           {
  48           }
  49   */
  50 //}
  51
  52 bool exprNode_isUnhandled (exprNode e)
  53 {
  54   llassert( exprNode_isDefined(e) );
  55   switch (e->kind)
  56     {
  57     case XPR_INITBLOCK:
  58     case XPR_EMPTY:
  59     case XPR_LABEL:
  60     case XPR_CONST:
  61     case XPR_VAR:
  62     case XPR_BODY:
  63     case XPR_OFFSETOF:
  64     case XPR_ALIGNOFT:
  65     case XPR_ALIGNOF:
  66     case XPR_VAARG:
  67     case XPR_ITERCALL:
  68     case XPR_ITER:
  69     case XPR_CAST:
  70     case XPR_GOTO:
  71     case XPR_CONTINUE:
  72     case XPR_BREAK:
  73     case XPR_COMMA:
  74     case XPR_COND:
  75     case XPR_TOK:
  76     case XPR_FTDEFAULT:
  77     case XPR_DEFAULT:
  78     case XPR_SWITCH:
  79     case XPR_FTCASE:
  80     case XPR_CASE:
  81       //    case XPR_INIT:
  82     case XPR_NODE:
  83       DPRINTF((message ("Warning current constraint generation does not handle expression %s", exprNode_unparse(e)) ) );
  84       return TRUE;
  85       /*@notreached@*/
  86       break;
  87     default:
  88       return FALSE;
  89
  90     }
  91   /*not reached*/
  92   return FALSE;
  93 }
  94
  95 bool exprNode_handleError( exprNode e)
  96 {
  97    if (exprNode_isError (e) || exprNode_isUnhandled(e) )
  98     {
  99       static /*@only@*/ cstring error = cstring_undefined;
 100
 101       if (!cstring_isDefined (error))
 102         {
 103           error = cstring_makeLiteral ("<error>");
 104         }
 105
 106       /*@-unqualifiedtrans*/ return TRUE; /*@=unqualifiedtrans*/
 107     }
 108    return FALSE;
 109 }
 110
 111 bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e)
 112 {
 113   if (exprNode_isError (e) )
 114     return FALSE;
 115
 116   if (exprNode_isUnhandled (e) )
 117     {
 118       DPRINTF( (message("Warning ignoring %s", exprNode_unparse (e) ) ) );
 119       e->requiresConstraints = constraintList_new();
 120       e->ensuresConstraints = constraintList_new();
 121       e->trueEnsuresConstraints = constraintList_new();
 122       e->falseEnsuresConstraints = constraintList_new();
 123       //  llassert(FALSE);
 124       return FALSE;
 125     }
 126
 127
 128   //  e = makeDataTypeConstraints (e);
 129
 130   DPRINTF((message ("exprNode_generateConstraints Analysising %s at %s", exprNode_unparse( e),
 131                     fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
 132
 133   if (exprNode_isMultiStatement ( e) )
 134     {
 135       exprNode_multiStatement(e);
 136     }
 137   else
 138     {
 139       //    llassert(FALSE);
 140       return FALSE;
 141     }
 142
 143   {
 144     constraintList c;
 145
 146     c = constraintList_makeFixedArrayConstraints (e->uses);
 147   e->requiresConstraints = reflectChanges (e->requiresConstraints, c);
 148
 149   //  e->ensuresConstraints = constraintList_mergeEnsures(c, e->ensuresConstraints);
 150
 151   }
 152
 153   /*  printf ("%s", (message ("%s", constraintList_printDetailed (e->requiresConstraints) ) ) );
 154       printf ("%s", (message ("%s", constraintList_printDetailed (e->ensuresConstraints) ) ) ); */
 155   return FALSE;
 156 }
 157
 158
 159 /* handles multiple statements */
 160
 161 bool exprNode_isMultiStatement(exprNode e)
 162 {
 163 if (exprNode_handleError (e) != NULL)
 164   return FALSE;
 165
 166   switch (e->kind)
 167     {
 168     case XPR_FOR:
 169     case XPR_FORPRED:
 170     case XPR_IF:
 171     case XPR_IFELSE:
 172     case XPR_WHILE:
 173     case XPR_WHILEPRED:
 174     case XPR_DOWHILE:
 175     case XPR_BLOCK:
 176     case XPR_STMT:
 177     case XPR_STMTLIST:
 178       return TRUE;
 179     default:
 180       return FALSE;
 181     }
 182
 183 }
 184
 185 bool exprNode_stmt (exprNode e)
 186 {
 187   exprNode snode;
 188   fileloc loc;
 189   bool notError;
 190
 191   if (exprNode_isError(e) )
 192     {
 193       return FALSE;
 194     }
 195   e->requiresConstraints = constraintList_new();
 196   e->ensuresConstraints  = constraintList_new();
 197   //  e = makeDataTypeConstraints(e);
 198
 199
 200   DPRINTF(( "STMT:") );
 201   DPRINTF ( ( cstring_toCharsSafe ( exprNode_unparse(e)) )
 202            );
 203   if (e->kind == XPR_INIT)
 204     {
 205       DPRINTF (("Init") );
 206       DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
 207       loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
 208       notError = exprNode_exprTraverse (e, FALSE, FALSE, loc);
 209       e->requiresConstraints = exprNode_traversRequiresConstraints(e);
 210       e->ensuresConstraints  = exprNode_traversEnsuresConstraints(e);
 211       return notError;
 212     }
 213
 214   if (e->kind != XPR_STMT)
 215     {
 216
 217       DPRINTF (("Not Stmt") );
 218       DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
 219       if (exprNode_isMultiStatement (e) )
 220         {
 221           return exprNode_multiStatement (e );
 222         }
 223       BPRINTF( (message ("Ignoring non-statement %s", exprNode_unparse(e) ) ) );
 224       return TRUE;
 225       //      llassert(FALSE);
 226     }
 227
 228   DPRINTF (("Stmt") );
 229   DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
 230
 231   snode = exprData_getUopNode (e->edata);
 232
 233   /* could be stmt involving multiple statements:
 234      i.e. if, while for ect.
 235   */
 236
 237   if (exprNode_isMultiStatement (snode))
 238     {
 239       //      llassert(FALSE);
 240       return exprNode_multiStatement (snode);
 241     }
 242
 243   loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
 244   notError = exprNode_exprTraverse (snode, FALSE, FALSE, loc);
 245   e->requiresConstraints = exprNode_traversRequiresConstraints(snode);
 246   //  printf ("For: %s \n", exprNode_unparse (e) );
 247   // printf ("%s\n", constraintList_print(e->requiresConstraints) );
 248   e->ensuresConstraints  = exprNode_traversEnsuresConstraints(snode);
 249   // printf ("Ensures that:\n %s\n", constraintList_print(e->ensuresConstraints) );
 250   //  llassert(notError);
 251   return notError;
 252
 253 }
 254
 255
 256 bool exprNode_stmtList  (exprNode e)
 257 {
 258   exprNode stmt1, stmt2;
 259   if (exprNode_isError (e) )
 260     {
 261       return FALSE;
 262     }
 263
 264   e->requiresConstraints = constraintList_new();
 265   e->ensuresConstraints  = constraintList_new();
 266   //  e = makeDataTypeConstraints(e);
 267
 268   /*Handle case of stmtList with only one statement:
 269    The parse tree stores this as stmt instead of stmtList*/
 270   if (e->kind != XPR_STMTLIST)
 271     {
 272       return exprNode_stmt(e);
 273     }
 274   llassert (e->kind == XPR_STMTLIST);
 275   DPRINTF(( "STMTLIST:") );
 276   DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)) ) );
 277   stmt1 = exprData_getPairA (e->edata);
 278   stmt2 = exprData_getPairB (e->edata);
 279
 280
 281   DPRINTF(("        stmtlist       ") );
 282   DPRINTF ((message("XW%s    |        %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2) ) ) );
 283
 284   exprNode_stmt (stmt1);
 285   DPRINTF(("\nstmt after stmtList call " ));
 286
 287   exprNode_stmt (stmt2);
 288   mergeResolve (e, stmt1, stmt2 );
 289
 290   DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n",
 291                       constraintList_print(e->requiresConstraints),
 292                       constraintList_print(e->ensuresConstraints) ) ) );
 293   return TRUE;
 294 }
 295
 296
 297 exprNode doIf (exprNode e, exprNode test, exprNode body)
 298 {
 299   DPRINTF ((message ("doIf: %s ", exprNode_unparse(e) ) ) );
 300
 301   test->ensuresConstraints = exprNode_traversEnsuresConstraints (test);
 302   test->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(test);
 303
 304   e->requiresConstraints = reflectChanges (body->requiresConstraints, test->trueEnsuresConstraints);
 305   e->requiresConstraints = reflectChanges (e->requiresConstraints,
 306                                            test->ensuresConstraints);
 307 #warning bad
 308   e->ensuresConstraints = constraintList_copy (test->ensuresConstraints);
 309   return e;
 310 }
 311
 312 constraintList constraintList_makeFixedArrayConstraints (sRefSet s)
 313 {
 314   constraintList ret;
 315   ret = constraintList_new();
 316
 317   sRefSet_elements (s, el)
 318     {
 319       //    llassert (el);
 320     if (sRef_isFixedArray(el) )
 321       {
 322         int s;
 323         constraint con;
 324         s = sRef_getArraySize(el);
 325         DPRINTF( (message("%s is a fixed array with size %d",
 326                           sRef_unparse(el), s) ) );
 327         con = constraint_makeSRefSetBufferSize (el, (s - 1));
 328         //con = constraint_makeSRefWriteSafeInt (el, (s - 1));
 329         ret = constraintList_add(ret, con);
 330       }
 331     else
 332       {
 333         DPRINTF( (message("%s is not a fixed array",
 334                           sRef_unparse(el)) ) );
 335       }
 336     }
 337   end_sRefSet_elements
 338
 339     return ret;
 340 }
 341
 342 exprNode makeDataTypeConstraints (exprNode e)
 343 {
 344   constraintList c;
 345   DPRINTF(("makeDataTypeConstraints"));
 346
 347   c = constraintList_makeFixedArrayConstraints (e->uses);
 348
 349   e->ensuresConstraints = constraintList_addList (e->ensuresConstraints, c);
 350
 351  return e;
 352 }
 353
 354 void doFor (exprNode e, exprNode forPred, exprNode forBody)
 355 {
 356   exprNode init, test, inc;
 357   //merge the constraints: modle as if statement
 358       /* init
 359         if (test)
 360            for body
 361            inc        */
 362       init  =  exprData_getTripleInit (forPred->edata);
 363       test =   exprData_getTripleTest (forPred->edata);
 364       inc  =   exprData_getTripleInc (forPred->edata);
 365
 366       if ( ( (exprNode_isError (test) /*|| (exprNode_isError(init) )*/ ) || (exprNode_isError (inc) ) ) )
 367         {
 368           DPRINTF ((message ("strange for statement:%s, ignoring it", exprNode_unparse(e) ) ) );
 369           return;
 370         }
 371
 372       forLoopHeuristics(e, forPred, forBody);
 373
 374       e->requiresConstraints = reflectChanges (forBody->requiresConstraints, test->ensuresConstraints);
 375       e->requiresConstraints = reflectChanges (e->requiresConstraints, test->trueEnsuresConstraints);
 376       e->requiresConstraints = reflectChanges (e->requiresConstraints, forPred->ensuresConstraints);
 377
 378       if (!forBody->canBreak)
 379         {
 380           e->ensuresConstraints = constraintList_addList(e->ensuresConstraints, forPred->ensuresConstraints);
 381           e->ensuresConstraints = constraintList_addList(e->ensuresConstraints, test->falseEnsuresConstraints);
 382         }
 383       else
 384         {
 385           DPRINTF(("Can break") );
 386         }
 387
 388 }
 389
 390 bool exprNode_multiStatement (exprNode e)
 391 {
 392
 393   bool ret;
 394   exprData data;
 395   exprNode e1, e2;
 396   exprNode p, trueBranch, falseBranch;
 397   exprNode forPred, forBody;
 398   exprNode init, test, inc;
 399   constraintList cons;
 400   constraintList t, f;
 401   e->requiresConstraints = constraintList_new();
 402   e->ensuresConstraints = constraintList_new();
 403   e->trueEnsuresConstraints = constraintList_new();
 404   e->falseEnsuresConstraints = constraintList_new();
 405
 406   //  e = makeDataTypeConstraints(e);
 407
 408   DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse( e),
 409                     fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
 410
 411   if (exprNode_handleError (e))
 412     {
 413       return FALSE;
 414     }
 415
 416   data = e->edata;
 417
 418   ret = TRUE;
 419
 420   switch (e->kind)
 421     {
 422
 423     case XPR_FOR:
 424       // ret = message ("%s %s",
 425       forPred = exprData_getPairA (data);
 426       forBody = exprData_getPairB (data);
 427
 428       //first generate the constraints
 429       exprNode_generateConstraints (forPred);
 430       exprNode_generateConstraints (forBody);
 431
 432
 433       doFor (e, forPred, forBody);
 434
 435       break;
 436
 437     case XPR_FORPRED:
 438       //            ret = message ("for (%s; %s; %s)",
 439       exprNode_generateConstraints (exprData_getTripleInit (data) );
 440       test = exprData_getTripleTest (data);
 441       exprNode_exprTraverse (test,FALSE, FALSE, exprNode_loc(e));
 442       if (!exprNode_isError(test) )
 443         test->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(test);
 444
 445       exprNode_generateConstraints (exprData_getTripleInc (data));
 446       break;
 447     case XPR_IF:
 448       DPRINTF(( "IF:") );
 449       DPRINTF ((exprNode_unparse(e) ) );
 450       //      ret = message ("if (%s) %s",
 451       e1 = exprData_getPairA (data);
 452       e2 = exprData_getPairB (data);
 453
 454       exprNode_exprTraverse (e1,
 455                              FALSE, FALSE, exprNode_loc(e1));
 456
 457       exprNode_generateConstraints (e2);
 458
 459       e = doIf (e, e1, e2);
 460
 461
 462       //      e->constraints = constraintList_exprNodemerge (exprData_getPairA (data),exprData_getPairB(data));
 463       break;
 464
 465     case XPR_IFELSE:
 466       DPRINTF(("Starting IFELSE"));
 467       //      ret = message ("if (%s) %s else %s",
 468       p = exprData_getTriplePred (data);
 469       trueBranch = exprData_getTripleTrue (data);
 470       falseBranch = exprData_getTripleFalse (data);
 471
 472       exprNode_exprTraverse (p,
 473                              FALSE, FALSE, exprNode_loc(p));
 474       exprNode_generateConstraints (trueBranch);
 475       exprNode_generateConstraints (falseBranch);
 476
 477       // do requires clauses
 478
 479       cons = reflectChanges (trueBranch->requiresConstraints, p->trueEnsuresConstraints);
 480       cons  = reflectChanges (cons,
 481                               p->ensuresConstraints);
 482       e->requiresConstraints = constraintList_copy (cons);
 483
 484       cons = reflectChanges (falseBranch->requiresConstraints, p->falseEnsuresConstraints);
 485       cons  = reflectChanges (cons,
 486                               p->ensuresConstraints);
 487       e->requiresConstraints = constraintList_addList (e->requiresConstraints,
 488                                                        cons);
 489       e->requiresConstraints = constraintList_addList (e->requiresConstraints,
 490                                                        p->requiresConstraints);
 491
 492       // do ensures clauses
 493       // find the  the ensures lists for each subbranch
 494       t = constraintList_mergeEnsures (p->trueEnsuresConstraints, trueBranch->ensuresConstraints);
 495       t = constraintList_mergeEnsures (p->ensuresConstraints, t);
 496
 497       f = constraintList_mergeEnsures (p->falseEnsuresConstraints, falseBranch->ensuresConstraints);
 498       f = constraintList_mergeEnsures (p->ensuresConstraints, f);
 499
 500       // find ensures for whole if/else statement
 501
 502       e->ensuresConstraints = constraintList_logicalOr (t, f);
 503       DPRINTF( ("Done IFELSE") );
 504       break;
 505     case XPR_WHILE:
 506        e1 = exprData_getPairA (data);
 507        e2 = exprData_getPairB (data);
 508       exprNode_exprTraverse (e1,
 509                              FALSE, FALSE, exprNode_loc(e1));
 510
 511       exprNode_generateConstraints (e2);
 512
 513       e1->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(e1);
 514
 515       e->requiresConstraints = reflectChanges (e2->requiresConstraints, e1->trueEnsuresConstraints);
 516
 517       e->requiresConstraints = reflectChanges (e->requiresConstraints,
 518                                                e1->ensuresConstraints);
 519 #warning bad
 520       e->ensuresConstraints = constraintList_copy (e1->ensuresConstraints);
 521
 522       //      ret = message ("while (%s) %s",
 523                      exprNode_generateConstraints (exprData_getPairA (data));
 524                      exprNode_generateConstraints (exprData_getPairB (data));
 525                      //      e->constraints = constraintList_exprNodemerge (exprData_getPairA (data), exprData_getPairB (data) );
 526       break;
 527
 528     case XPR_DOWHILE:
 529       // ret = message ("do { %s } while (%s)",
 530                      exprNode_generateConstraints (exprData_getPairB (data));
 531                      exprNode_generateConstraints (exprData_getPairA (data));
 532       break;
 533
 534     case XPR_BLOCK:
 535       //      ret = message ("{ %s }",
 536                      exprNode_generateConstraints (exprData_getSingle (data));
 537                      e->requiresConstraints = constraintList_copy ( (exprData_getSingle (data))->requiresConstraints );
 538                      e->ensuresConstraints = constraintList_copy ( (exprData_getSingle (data))->ensuresConstraints );
 539                      //      e->constraints = (exprData_getSingle (data))->constraints;
 540       break;
 541
 542     case XPR_STMT:
 543     case XPR_STMTLIST:
 544       return exprNode_stmtList (e);
 545       /*@notreached@*/
 546       break;
 547     default:
 548       ret=FALSE;
 549     }
 550   return ret;
 551 }
 552
 553 bool lltok_isBoolean_Op (lltok tok)
 554 {
 555   /*this should really be a switch statement but
 556     I don't want to violate the abstraction
 557     maybe this should go in lltok.c */
 558
 559   if (lltok_isEq_Op (tok) )
 560         {
 561           return TRUE;
 562         }
 563       if (lltok_isAnd_Op (tok) )
 564
 565         {
 566
 567           return TRUE;
 568         }
 569    if (lltok_isOr_Op (tok) )
 570         {
 571           return TRUE;
 572         }
 573
 574    if (lltok_isGt_Op (tok) )
 575      {
 576        return TRUE;
 577      }
 578    if (lltok_isLt_Op (tok) )
 579      {
 580        return TRUE;
 581      }
 582
 583    if (lltok_isLe_Op (tok) )
 584      {
 585        return TRUE;
 586      }
 587
 588    if (lltok_isGe_Op (tok) )
 589      {
 590        return TRUE;
 591      }
 592
 593    return FALSE;
 594
 595 }
 596
 597
 598 void exprNode_booleanTraverse (exprNode e, bool definatelv, bool definaterv,  fileloc sequencePoint)
 599 {
 600  constraint cons;
 601 exprNode t1, t2;
 602 exprData data;
 603 lltok tok;
 604 constraintList tempList;
 605 data = e->edata;
 606
 607 tok = exprData_getOpTok (data);
 608
 609
 610 t1 = exprData_getOpA (data);
 611 t2 = exprData_getOpB (data);
 612
 613
 614 /* arithmetic tests */
 615
 616 if (lltok_isEq_Op (tok) )
 617 {
 618   cons =  constraint_makeEnsureEqual (t1, t2, sequencePoint);
 619   e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
 620 }
 621
 622
 623  if (lltok_isLt_Op (tok) )
 624    {
 625      cons =  constraint_makeEnsureLessThan (t1, t2, sequencePoint);
 626      e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
 627      cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
 628      e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
 629    }
 630
 631
 632 if (lltok_isGe_Op (tok) )
 633 {
 634
 635   cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
 636   e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
 637
 638   cons =  constraint_makeEnsureLessThan (t1, t2, sequencePoint);
 639   e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
 640
 641 }
 642
 643
 644   if (lltok_isGt_Op (tok) )
 645 {
 646   cons =  constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
 647   e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
 648   cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
 649   e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
 650 }
 651
 652 if (lltok_isLe_Op (tok) )
 653 {
 654    cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
 655   e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
 656
 657   cons =  constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
 658   e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
 659 }
 660
 661
 662
 663 /*Logical operations */
 664
 665  if (lltok_isAnd_Op (tok) )
 666
 667    {
 668      //true ensures
 669      tempList = constraintList_copy (t1->trueEnsuresConstraints);
 670      tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
 671      e->trueEnsuresConstraints = constraintList_addList(e->trueEnsuresConstraints, tempList);
 672
 673       //false ensures: fens t1 or tens t1 and fens t2
 674      tempList = constraintList_copy (t1->trueEnsuresConstraints);
 675      tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
 676      tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints);
 677       e->falseEnsuresConstraints =constraintList_addList(e->falseEnsuresConstraints, tempList);
 678
 679    }
 680
 681   if (lltok_isOr_Op (tok) )
 682     {
 683       //false ensures
 684       tempList = constraintList_copy (t1->falseEnsuresConstraints);
 685       tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
 686       e->falseEnsuresConstraints = constraintList_addList(e->falseEnsuresConstraints, tempList);
 687
 688       //true ensures: tens t1 or fens t1 and tens t2
 689       tempList = constraintList_copy (t1->falseEnsuresConstraints);
 690       tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
 691       tempList = constraintList_logicalOr (tempList, t1->trueEnsuresConstraints);
 692       e->trueEnsuresConstraints =constraintList_addList(e->trueEnsuresConstraints, tempList);
 693
 694     }
 695
 696 }
 697
 698 bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv,  fileloc sequencePoint)
 699 {
 700   exprNode t1, t2;
 701   lltok tok;
 702   bool handledExprNode;
 703   exprData data;
 704   constraint cons;
 705
 706      if (exprNode_isError(e) )
 707      {
 708        return FALSE;
 709      }
 710
 711    DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e),
 712                     fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
 713
 714    e->requiresConstraints = constraintList_new();
 715    e->ensuresConstraints = constraintList_new();
 716    e->trueEnsuresConstraints = constraintList_new();;
 717    e->falseEnsuresConstraints = constraintList_new();;
 718
 719    if (exprNode_isUnhandled (e) )
 720      {
 721        return FALSE;
 722      }
 723    //   e = makeDataTypeConstraints (e);
 724
 725    handledExprNode = TRUE;
 726
 727   data = e->edata;
 728
 729   switch (e->kind)
 730     {
 731
 732
 733     case XPR_WHILEPRED:
 734       t1 = exprData_getSingle (data);
 735       exprNode_exprTraverse (t1,  definatelv, definaterv, sequencePoint);
 736       e = exprNode_copyConstraints (e, t1);
 737       break;
 738
 739     case XPR_FETCH:
 740
 741       if (definatelv )
 742         {
 743           t1 =  (exprData_getPairA (data) );
 744           t2 =  (exprData_getPairB (data) );
 745           cons =  constraint_makeWriteSafeExprNode (t1, t2);
 746         }
 747       else
 748         {
 749           t1 =  (exprData_getPairA (data) );
 750           t2 =  (exprData_getPairB (data) );
 751           cons = constraint_makeReadSafeExprNode (t1, t2 );
 752         }
 753
 754       e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
 755       cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint);
 756       e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
 757
 758       cons = constraint_makeEnsureLteMaxRead (t1, t2);
 759       e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
 760
 761       //      cons = constraint_makeEnsureMinReadAtMost (t1, t2, sequencePoint);
 762       // e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
 763
 764       exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
 765       exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
 766
 767             /*@i325 Should check which is array/index. */
 768       break;
 769
 770     case XPR_PARENS:
 771       exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint);
 772       //    e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined);
 773       break;
 774     case XPR_INIT:
 775      /*   //t1 = exprData_getInitId (data); */
 776       t2 = exprData_getInitNode (data);
 777       //exprNode_exprTraverse (t1, TRUE, FALSE, sequencePoint );
 778
 779       exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
 780
 781       /* this test is nessecary because some expressions generate a null expression node.  function pointer do that -- drl */
 782         if ( (!exprNode_isError (e))  &&  (!exprNode_isError(t2)) )
 783         {
 784           cons =  constraint_makeEnsureEqual (e, t2, sequencePoint);
 785           e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
 786         }
 787
 788       break;
 789     case XPR_ASSIGN:
 790       t1 = exprData_getOpA (data);
 791       t2 = exprData_getOpB (data);
 792       exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
 793       lltok_unparse (exprData_getOpTok (data));
 794       exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
 795
 796       /* this test is nessecary because some expressions generate a null expression node.  function pointer do that -- drl */
 797       if ( (!exprNode_isError (t1))  &&  (!exprNode_isError(t2)) )
 798         {
 799           cons =  constraint_makeEnsureEqual (t1, t2, sequencePoint);
 800           e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
 801         }
 802       break;
 803     case XPR_OP:
 804       t1 = exprData_getOpA (data);
 805       t2 = exprData_getOpB (data);
 806
 807        exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
 808       tok = exprData_getOpTok (data);
 809       exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
 810
 811       if (lltok_isBoolean_Op (tok) )
 812         exprNode_booleanTraverse (e, definatelv, definaterv, sequencePoint);
 813
 814       //      e->constraints  = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data));
 815       break;
 816     case XPR_SIZEOFT:
 817       ctype_unparse (qtype_getType (exprData_getType (data) ) );
 818
 819       break;
 820
 821     case XPR_SIZEOF:
 822       exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
 823       //      e->constraints = constraintList_exprNodemerge (exprData_getSingle (e->edata), exprNode_undefined);
 824       break;
 825
 826     case XPR_CALL:
 827       exprNode_exprTraverse (exprData_getFcn (data), definatelv, definaterv, sequencePoint );
 828       exprNodeList_unparse (exprData_getArgs (data) );
 829       DPRINTF ( (message ("Got call that %s ( %s) ",  exprNode_unparse(exprData_getFcn(data) ),   exprNodeList_unparse (exprData_getArgs (data) ) ) ) );
 830
 831
 832
 833       e->requiresConstraints = constraintList_addList (e->requiresConstraints,
 834                                                  checkCall (exprData_getFcn (data), exprData_getArgs (data)  ) );
 835
 836       e->ensuresConstraints = constraintList_addList (e->ensuresConstraints,
 837                                                  getPostConditions(exprData_getFcn (data), exprData_getArgs (data),e  ) );
 838       //      e->constraints = constraintList_add (e->constraints, constraint_create (e,exprNode_undefined, GT,  CALLSAFE ) );
 839       break;
 840
 841     case XPR_RETURN:
 842       exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
 843       break;
 844
 845     case XPR_NULLRETURN:
 846       cstring_makeLiteral ("return");;
 847       break;
 848
 849
 850     case XPR_FACCESS:
 851       exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
 852       exprData_getFieldName (data) ;
 853       break;
 854
 855     case XPR_ARROW:
 856       exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
 857       exprData_getFieldName (data);
 858       break;
 859
 860     case XPR_STRINGLITERAL:
 861       cstring_copy (exprData_getLiteral (data));
 862       break;
 863
 864     case XPR_NUMLIT:
 865       cstring_copy (exprData_getLiteral (data));
 866       break;
 867
 868     case XPR_PREOP:
 869       t1 = exprData_getUopNode(data);
 870       tok = (exprData_getUopTok (data));
 871       //lltok_unparse (exprData_getUopTok (data));
 872       exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
 873       /*handle * pointer access */
 874       if (lltok_isInc_Op (tok) )
 875         {
 876           DPRINTF(("doing ++(var)"));
 877           t1 = exprData_getUopNode (data);
 878           cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
 879           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
 880         }
 881       else if (lltok_isDec_Op (tok) )
 882         {
 883           DPRINTF(("doing --(var)"));
 884           t1 = exprData_getUopNode (data);
 885           cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint );
 886           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
 887         }
 888
 889       if (lltok_isMult( exprData_getUopTok (data) ) )
 890         {
 891           if (definatelv)
 892             {
 893               cons = constraint_makeWriteSafeInt (t1, 0);
 894             }
 895           else
 896             {
 897               cons = constraint_makeReadSafeInt (t1, 0);
 898             }
 899               e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
 900         }
 901
 902       /* ! expr */
 903       if (lltok_isNot_Op (exprData_getUopTok (data) ) )
 904         {
 905           e->trueEnsuresConstraints  = constraintList_copy (t1->falseEnsuresConstraints);
 906           e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints);
 907         }
 908       break;
 909
 910     case XPR_POSTOP:
 911
 912       exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint );
 913       lltok_unparse (exprData_getUopTok (data));
 914       if (lltok_isInc_Op (exprData_getUopTok (data) ) )
 915         {
 916           DPRINTF(("doing ++"));
 917           t1 = exprData_getUopNode (data);
 918           cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
 919           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
 920         }
 921        if (lltok_isDec_Op (exprData_getUopTok (data) ) )
 922         {
 923           DPRINTF(("doing --"));
 924           t1 = exprData_getUopNode (data);
 925           cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint );
 926           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
 927         }
 928       break;
 929     default:
 930       handledExprNode = FALSE;
 931     }
 932
 933   e->requiresConstraints =  constraintList_preserveOrig ( e->requiresConstraints);
 934   e->ensuresConstraints  =  constraintList_preserveOrig ( e->ensuresConstraints);
 935   DPRINTF((message ("ensures constraint for %s are %s", exprNode_unparse(e), constraintList_print(e->ensuresConstraints) ) ));
 936
 937   return handledExprNode;
 938 }
 939
 940
 941 constraintList exprNode_traversTrueEnsuresConstraints (exprNode e)
 942 {
 943   //  exprNode t1, t2;
 944
 945   bool handledExprNode;
 946   //  char * mes;
 947   exprData data;
 948   constraintList ret;
 949
 950    if (exprNode_handleError (e))
 951      {
 952        ret = constraintList_new();
 953        return ret;
 954      }
 955   ret = constraintList_copy (e->trueEnsuresConstraints );
 956
 957    handledExprNode = TRUE;
 958
 959   data = e->edata;
 960
 961   switch (e->kind)
 962     {
 963
 964     case XPR_FETCH:
 965
 966       ret = constraintList_addList (ret,
 967                                     exprNode_traversTrueEnsuresConstraints
 968                                     (exprData_getPairA (data) ) );
 969
 970       ret = constraintList_addList (ret,
 971                                     exprNode_traversTrueEnsuresConstraints
 972                                     (exprData_getPairB (data) ) );
 973       break;
 974     case XPR_PREOP:
 975
 976       ret = constraintList_addList (ret,
 977                                     exprNode_traversTrueEnsuresConstraints
 978                                     (exprData_getUopNode (data) ) );
 979       break;
 980
 981     case XPR_PARENS:
 982       ret = constraintList_addList (ret, exprNode_traversTrueEnsuresConstraints
 983                                     (exprData_getUopNode (data) ) );
 984       break;
 985     case XPR_ASSIGN:
 986         ret = constraintList_addList (ret,
 987                                     exprNode_traversTrueEnsuresConstraints
 988                                     (exprData_getOpA (data) ) );
 989
 990        ret = constraintList_addList (ret,
 991                                     exprNode_traversTrueEnsuresConstraints
 992                                     (exprData_getOpB (data) ) );
 993        break;
 994     case XPR_OP:
 995        ret = constraintList_addList (ret,
 996                                     exprNode_traversTrueEnsuresConstraints
 997                                     (exprData_getOpA (data) ) );
 998
 999        ret = constraintList_addList (ret,
1000                                     exprNode_traversTrueEnsuresConstraints
1001                                     (exprData_getOpB (data) ) );
1002        break;
1003     case XPR_SIZEOFT:
1004
1005       //      ctype_unparse (qtype_getType (exprData_getType (data) ) );
1006
1007       break;
1008
1009     case XPR_SIZEOF:
1010
1011        ret = constraintList_addList (ret,
1012                                     exprNode_traversTrueEnsuresConstraints
1013                                      (exprData_getSingle (data) ) );
1014        break;
1015
1016     case XPR_CALL:
1017       ret = constraintList_addList (ret,
1018                                      exprNode_traversTrueEnsuresConstraints
1019                                     (exprData_getFcn (data) ) );
1020       /*@i11*/      //   exprNodeList_unparse (exprData_getArgs (data) );
1021          break;
1022
1023     case XPR_RETURN:
1024       ret = constraintList_addList (ret,
1025                                     exprNode_traversTrueEnsuresConstraints
1026                                     (exprData_getSingle (data) ) );
1027       break;
1028
1029     case XPR_NULLRETURN:
1030       //      cstring_makeLiteral ("return");;
1031       break;
1032
1033     case XPR_FACCESS:
1034           ret = constraintList_addList (ret,
1035                                     exprNode_traversTrueEnsuresConstraints
1036                                     (exprData_getFieldNode (data) ) );
1037        //exprData_getFieldName (data) ;
1038       break;
1039
1040     case XPR_ARROW:
1041         ret = constraintList_addList (ret,
1042                                     exprNode_traversTrueEnsuresConstraints
1043                                     (exprData_getFieldNode (data) ) );
1044         //      exprData_getFieldName (data);
1045       break;
1046
1047     case XPR_STRINGLITERAL:
1048       //      cstring_copy (exprData_getLiteral (data));
1049       break;
1050
1051     case XPR_NUMLIT:
1052       //      cstring_copy (exprData_getLiteral (data));
1053       break;
1054     case XPR_POSTOP:
1055
1056            ret = constraintList_addList (ret,
1057                                     exprNode_traversTrueEnsuresConstraints
1058                                     (exprData_getUopNode (data) ) );
1059            break;
1060     default:
1061       break;
1062     }
1063
1064   return ret;
1065 }
1066
1067
1068 /* walk down the tree and get all requires Constraints in each subexpression*/
1069 constraintList exprNode_traversRequiresConstraints (exprNode e)
1070 {
1071   //  exprNode t1, t2;
1072
1073   bool handledExprNode;
1074   //  char * mes;
1075   exprData data;
1076   constraintList ret;
1077
1078    if (exprNode_handleError (e))
1079      {
1080        ret = constraintList_new();
1081        return ret;
1082      }
1083   ret = constraintList_copy (e->requiresConstraints );
1084
1085    handledExprNode = TRUE;
1086
1087   data = e->edata;
1088
1089   switch (e->kind)
1090     {
1091
1092     case XPR_FETCH:
1093
1094       ret = constraintList_addList (ret,
1095                                     exprNode_traversRequiresConstraints
1096                                     (exprData_getPairA (data) ) );
1097
1098       ret = constraintList_addList (ret,
1099                                     exprNode_traversRequiresConstraints
1100                                     (exprData_getPairB (data) ) );
1101       break;
1102     case XPR_PREOP:
1103
1104       ret = constraintList_addList (ret,
1105                                     exprNode_traversRequiresConstraints
1106                                     (exprData_getUopNode (data) ) );
1107       break;
1108
1109     case XPR_PARENS:
1110       ret = constraintList_addList (ret, exprNode_traversRequiresConstraints
1111                                     (exprData_getUopNode (data) ) );
1112       break;
1113     case XPR_ASSIGN:
1114         ret = constraintList_addList (ret,
1115                                     exprNode_traversRequiresConstraints
1116                                     (exprData_getOpA (data) ) );
1117
1118        ret = constraintList_addList (ret,
1119                                     exprNode_traversRequiresConstraints
1120                                     (exprData_getOpB (data) ) );
1121        break;
1122     case XPR_OP:
1123        ret = constraintList_addList (ret,
1124                                     exprNode_traversRequiresConstraints
1125                                     (exprData_getOpA (data) ) );
1126
1127        ret = constraintList_addList (ret,
1128                                     exprNode_traversRequiresConstraints
1129                                     (exprData_getOpB (data) ) );
1130        break;
1131     case XPR_SIZEOFT:
1132
1133       //      ctype_unparse (qtype_getType (exprData_getType (data) ) );
1134
1135       break;
1136
1137     case XPR_SIZEOF:
1138
1139        ret = constraintList_addList (ret,
1140                                     exprNode_traversRequiresConstraints
1141                                      (exprData_getSingle (data) ) );
1142        break;
1143
1144     case XPR_CALL:
1145       ret = constraintList_addList (ret,
1146                                      exprNode_traversRequiresConstraints
1147                                     (exprData_getFcn (data) ) );
1148       /*@i11*/      //   exprNodeList_unparse (exprData_getArgs (data) );
1149          break;
1150
1151     case XPR_RETURN:
1152       ret = constraintList_addList (ret,
1153                                     exprNode_traversRequiresConstraints
1154                                     (exprData_getSingle (data) ) );
1155       break;
1156
1157     case XPR_NULLRETURN:
1158       //      cstring_makeLiteral ("return");;
1159       break;
1160
1161     case XPR_FACCESS:
1162           ret = constraintList_addList (ret,
1163                                     exprNode_traversRequiresConstraints
1164                                     (exprData_getFieldNode (data) ) );
1165        //exprData_getFieldName (data) ;
1166       break;
1167
1168     case XPR_ARROW:
1169         ret = constraintList_addList (ret,
1170                                     exprNode_traversRequiresConstraints
1171                                     (exprData_getFieldNode (data) ) );
1172         //      exprData_getFieldName (data);
1173       break;
1174
1175     case XPR_STRINGLITERAL:
1176       //      cstring_copy (exprData_getLiteral (data));
1177       break;
1178
1179     case XPR_NUMLIT:
1180       //      cstring_copy (exprData_getLiteral (data));
1181       break;
1182     case XPR_POSTOP:
1183
1184            ret = constraintList_addList (ret,
1185                                     exprNode_traversRequiresConstraints
1186                                     (exprData_getUopNode (data) ) );
1187            break;
1188     default:
1189       break;
1190     }
1191
1192   return ret;
1193 }
1194
1195
1196 /* walk down the tree and get all Ensures Constraints in each subexpression*/
1197 constraintList exprNode_traversEnsuresConstraints (exprNode e)
1198 {
1199   //  exprNode t1, t2;
1200
1201   bool handledExprNode;
1202   //  char * mes;
1203   exprData data;
1204   //  constraintExpr tmp;
1205   //  constraint cons;
1206   constraintList ret;
1207
1208
1209    if (exprNode_handleError (e))
1210      {
1211        ret = constraintList_new();
1212        return ret;
1213      }
1214
1215   ret = constraintList_copy (e->ensuresConstraints );
1216    handledExprNode = TRUE;
1217
1218   data = e->edata;
1219
1220   DPRINTF( (message (
1221                      "exprnode_traversEnsuresConstraints call for %s with constraintList of %s",
1222                      exprNode_unparse (e),
1223                      constraintList_print(e->ensuresConstraints)
1224                      )
1225             ));
1226
1227
1228   switch (e->kind)
1229     {
1230
1231     case XPR_FETCH:
1232
1233       ret = constraintList_addList (ret,
1234                                     exprNode_traversEnsuresConstraints
1235                                     (exprData_getPairA (data) ) );
1236
1237       ret = constraintList_addList (ret,
1238                                     exprNode_traversEnsuresConstraints
1239                                     (exprData_getPairB (data) ) );
1240       break;
1241     case XPR_PREOP:
1242
1243       ret = constraintList_addList (ret,
1244                                     exprNode_traversEnsuresConstraints
1245                                     (exprData_getUopNode (data) ) );
1246       break;
1247
1248     case XPR_PARENS:
1249       ret = constraintList_addList (ret, exprNode_traversEnsuresConstraints
1250                                     (exprData_getUopNode (data) ) );
1251       break;
1252     case XPR_ASSIGN:
1253         ret = constraintList_addList (ret,
1254                                     exprNode_traversEnsuresConstraints
1255                                     (exprData_getOpA (data) ) );
1256
1257        ret = constraintList_addList (ret,
1258                                     exprNode_traversEnsuresConstraints
1259                                     (exprData_getOpB (data) ) );
1260        break;
1261     case XPR_OP:
1262        ret = constraintList_addList (ret,
1263                                     exprNode_traversEnsuresConstraints
1264                                     (exprData_getOpA (data) ) );
1265
1266        ret = constraintList_addList (ret,
1267                                     exprNode_traversEnsuresConstraints
1268                                     (exprData_getOpB (data) ) );
1269        break;
1270     case XPR_SIZEOFT:
1271
1272       //      ctype_unparse (qtype_getType (exprData_getType (data) ) );
1273
1274       break;
1275
1276     case XPR_SIZEOF:
1277
1278        ret = constraintList_addList (ret,
1279                                     exprNode_traversEnsuresConstraints
1280                                      (exprData_getSingle (data) ) );
1281        break;
1282
1283     case XPR_CALL:
1284       ret = constraintList_addList (ret,
1285                                      exprNode_traversEnsuresConstraints
1286                                     (exprData_getFcn (data) ) );
1287       /*@i11*/      //   exprNodeList_unparse (exprData_getArgs (data) );
1288          break;
1289
1290     case XPR_RETURN:
1291       ret = constraintList_addList (ret,
1292                                     exprNode_traversEnsuresConstraints
1293                                     (exprData_getSingle (data) ) );
1294       break;
1295
1296     case XPR_NULLRETURN:
1297       //      cstring_makeLiteral ("return");;
1298       break;
1299
1300     case XPR_FACCESS:
1301           ret = constraintList_addList (ret,
1302                                     exprNode_traversEnsuresConstraints
1303                                     (exprData_getFieldNode (data) ) );
1304        //exprData_getFieldName (data) ;
1305       break;
1306
1307     case XPR_ARROW:
1308         ret = constraintList_addList (ret,
1309                                     exprNode_traversEnsuresConstraints
1310                                     (exprData_getFieldNode (data) ) );
1311         //      exprData_getFieldName (data);
1312       break;
1313
1314     case XPR_STRINGLITERAL:
1315       //      cstring_copy (exprData_getLiteral (data));
1316       break;
1317
1318     case XPR_NUMLIT:
1319       //      cstring_copy (exprData_getLiteral (data));
1320       break;
1321     case XPR_POSTOP:
1322
1323            ret = constraintList_addList (ret,
1324                                     exprNode_traversEnsuresConstraints
1325                                     (exprData_getUopNode (data) ) );
1326            break;
1327     default:
1328       break;
1329     }
1330 DPRINTF( (message (
1331                      "exprnode_traversEnsuresConstraints call for %s with constraintList of  is returning %s",
1332                      exprNode_unparse (e),
1333              //              constraintList_print(e->ensuresConstraints),
1334                      constraintList_print(ret)
1335                      )
1336             ));
1337
1338
1339   return ret;
1340 }
1341