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