src/constraintGeneration.c

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