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