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