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