src/constraintGeneration.c

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