src/constraintGeneration.c

   1
   2 /*
   3 ** constraintGeneration.c
   4 */
   5
   6 //#define DEBUGPRINT 1
   7
   8 # include <ctype.h> /* for isdigit */
   9 # include "lclintMacros.nf"
  10 # include "basic.h"
  11
  12 # include "cgrammar_tokens.h"
  13
  14 # include "exprChecks.h"
  15 # include "exprNodeSList.h"
  16
  17 //# include "exprDataQuite.i"
  18
  19 /*@access exprNode @*/
  20
  21
  22 static bool exprNode_handleError(/*@dependent@*/ exprNode p_e);
  23
  24 //static cstring exprNode_findConstraints ( exprNode p_e);
  25 static bool exprNode_isMultiStatement(/*@dependent@*/ exprNode p_e);
  26 static void  exprNode_multiStatement (/*@dependent@*/ exprNode p_e);
  27
  28 //static void exprNode_constraintPropagateUp (exprNode p_e);
  29
  30 static constraintList exprNode_traversTrueEnsuresConstraints (/*@dependent@*/ exprNode p_e);
  31 static constraintList exprNode_traversFalseEnsuresConstraints (/*@dependent@*/ exprNode p_e);
  32
  33 static exprNode makeDataTypeConstraints (/*@returned@*/ exprNode p_e);
  34
  35 static void checkArgumentList (/*@out@*/ exprNode p_temp, exprNodeList p_arglist, fileloc p_sequencePoint) /*@modifies p_temp @*/;
  36
  37 static  constraintList checkCall (/*@dependent@*/ exprNode p_fcn, exprNodeList p_arglist);
  38
  39 //constraintList constraintList_makeFixedArrayConstraints (sRefSet s);
  40
  41 //bool exprNode_testd()
  42 //{
  43   /*        if ( ( (exprNode_isError  ) ) )
  44           {
  45           }
  46         if ( ( (e_1  ) ) )
  47           {
  48           }
  49   */
  50 //}
  51
  52 static bool exprNode_isUnhandled (/*@dependent@*/ /*@observer@*/ exprNode e)
  53 {
  54   llassert( exprNode_isDefined(e) );
  55   switch (e->kind)
  56     {
  57     case XPR_INITBLOCK:
  58     case XPR_EMPTY:
  59     case XPR_LABEL:
  60     case XPR_CONST:
  61     case XPR_VAR:
  62     case XPR_BODY:
  63     case XPR_OFFSETOF:
  64     case XPR_ALIGNOFT:
  65     case XPR_ALIGNOF:
  66     case XPR_VAARG:
  67     case XPR_ITERCALL:
  68     case XPR_ITER:
  69     case XPR_GOTO:
  70     case XPR_CONTINUE:
  71     case XPR_BREAK:
  72     case XPR_COMMA:
  73     case XPR_COND:
  74     case XPR_TOK:
  75     case XPR_FTDEFAULT:
  76     case XPR_DEFAULT:
  77       //    case XPR_SWITCH:
  78     case XPR_FTCASE:
  79     case XPR_CASE:
  80       //    case XPR_INIT:
  81     case XPR_NODE:
  82       DPRINTF((message ("Warning current constraint generation does not handle expression %s", exprNode_unparse(e)) ) );
  83       return TRUE;
  84       /*@notreached@*/
  85       break;
  86     default:
  87       return FALSE;
  88
  89     }
  90   /*not reached*/
  91   return FALSE;
  92 }
  93
  94 bool exprNode_handleError( exprNode e)
  95 {
  96    if (exprNode_isError (e) || exprNode_isUnhandled(e) )
  97     {
  98       static /*@only@*/ cstring error = cstring_undefined;
  99
 100       if (!cstring_isDefined (error))
 101         {
 102           error = cstring_makeLiteral ("<error>");
 103         }
 104
 105       /*@-unqualifiedtrans*/ return TRUE; /*@=unqualifiedtrans*/
 106     }
 107    return FALSE;
 108 }
 109
 110 bool /*@alt void@*/ exprNode_generateConstraints (/*@dependent@*/ exprNode e)
 111 {
 112   if (exprNode_isError (e) )
 113     return FALSE;
 114
 115   if (exprNode_isUnhandled (e) )
 116     {
 117       DPRINTF( (message("Warning ignoring %s", exprNode_unparse (e) ) ) );
 118         return FALSE;
 119     }
 120
 121
 122   //  e = makeDataTypeConstraints (e);
 123
 124   DPRINTF((message ("exprNode_generateConstraints Analysising %s at %s", exprNode_unparse( e),
 125                     fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
 126
 127   if (exprNode_isMultiStatement ( e) )
 128     {
 129       exprNode_multiStatement(e);
 130     }
 131   else
 132     {
 133       fileloc loc;
 134
 135       loc = exprNode_getNextSequencePoint(e);
 136       exprNode_exprTraverse(e, FALSE, FALSE, loc);
 137
 138       fileloc_free(loc);
 139       return FALSE;
 140     }
 141
 142   {
 143     constraintList c;
 144
 145     c = constraintList_makeFixedArrayConstraints (e->uses);
 146     e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, c);
 147
 148   //  e->ensuresConstraints = constraintList_mergeEnsures(c, e->ensuresConstraints);
 149
 150     constraintList_free(c);
 151   }
 152
 153   DPRINTF ( (message ("e->requiresConstraints %s", constraintList_printDetailed (e->requiresConstraints) ) ) );
 154   return FALSE;
 155 }
 156
 157
 158 /* handles multiple statements */
 159
 160 bool exprNode_isMultiStatement(exprNode e)
 161 {
 162 if (exprNode_handleError (e) != NULL)
 163   return FALSE;
 164
 165   switch (e->kind)
 166     {
 167     case XPR_FOR:
 168     case XPR_FORPRED:
 169     case XPR_IF:
 170     case XPR_IFELSE:
 171     case XPR_WHILE:
 172     case XPR_WHILEPRED:
 173     case XPR_DOWHILE:
 174     case XPR_BLOCK:
 175     case XPR_STMT:
 176     case XPR_STMTLIST:
 177     case XPR_SWITCH:
 178       return TRUE;
 179     default:
 180       return FALSE;
 181     }
 182
 183 }
 184
 185 static void exprNode_stmt ( /*@dependent@*/ /*@temp@*/ exprNode e)
 186 {
 187   exprNode snode;
 188   fileloc loc;
 189   cstring s;
 190
 191   if (exprNode_isError(e) )
 192     {
 193       return; // FALSE;
 194     }
 195   /*e->requiresConstraints = constraintList_makeNew();
 196     e->ensuresConstraints  = constraintList_makeNew(); */
 197   //  e = makeDataTypeConstraints(e);
 198
 199
 200   DPRINTF(( "STMT:") );
 201   s =  exprNode_unparse(e);
 202   // DPRINTF ( ( message("STMT: %s ") ) );
 203
 204   if (e->kind == XPR_INIT)
 205     {
 206       constraintList tempList;
 207       DPRINTF (("Init") );
 208       DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
 209       loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
 210       exprNode_exprTraverse (e, FALSE, FALSE, loc);
 211       fileloc_free(loc);
 212
 213       tempList = e->requiresConstraints;
 214       e->requiresConstraints = exprNode_traversRequiresConstraints(e);
 215       constraintList_free(tempList);
 216
 217       tempList = e->ensuresConstraints;
 218       e->ensuresConstraints  = exprNode_traversEnsuresConstraints(e);
 219       constraintList_free(tempList);
 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
 257   fileloc_free(loc);
 258
 259   constraintList_free (e->requiresConstraints);
 260   e->requiresConstraints = exprNode_traversRequiresConstraints(snode);
 261   //  printf ("For: %s \n", exprNode_unparse (e) );
 262   // printf ("%s\n", constraintList_print(e->requiresConstraints) );
 263
 264   constraintList_free (e->ensuresConstraints);
 265   e->ensuresConstraints  = exprNode_traversEnsuresConstraints(snode);
 266   // printf ("Ensures that:\n %s\n", constraintList_print(e->ensuresConstraints) );
 267   //  llassert(notError);
 268
 269   DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n",
 270                       constraintList_print(e->requiresConstraints),
 271                       constraintList_print(e->ensuresConstraints) ) ) );
 272
 273   return; // notError;
 274
 275 }
 276
 277
 278 static void exprNode_stmtList  (/*@dependent@*/ exprNode e)
 279 {
 280   exprNode stmt1, stmt2;
 281   if (exprNode_isError (e) )
 282     {
 283       return; // FALSE;
 284     }
 285
 286   /*
 287     e->requiresConstraints = constraintList_makeNew();
 288     e->ensuresConstraints  = constraintList_makeNew();
 289   */
 290   //  e = makeDataTypeConstraints(e);
 291
 292   /*Handle case of stmtList with only one statement:
 293    The parse tree stores this as stmt instead of stmtList*/
 294   if (e->kind != XPR_STMTLIST)
 295     {
 296       exprNode_stmt(e);
 297       return;
 298     }
 299   llassert (e->kind == XPR_STMTLIST);
 300   DPRINTF(( "STMTLIST:") );
 301   DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)) ) );
 302   stmt1 = exprData_getPairA (e->edata);
 303   stmt2 = exprData_getPairB (e->edata);
 304
 305
 306   DPRINTF(("        stmtlist       ") );
 307   DPRINTF ((message("XW%s    |        %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2) ) ) );
 308
 309   exprNode_stmt (stmt1);
 310   DPRINTF(("\nstmt after stmtList call " ));
 311
 312   exprNode_stmt (stmt2);
 313   exprNode_mergeResolve (e, stmt1, stmt2 );
 314
 315   DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n",
 316                       constraintList_print(e->requiresConstraints),
 317                       constraintList_print(e->ensuresConstraints) ) ) );
 318   return; // TRUE;
 319 }
 320
 321 static exprNode doIf (/*@returned@*/  exprNode e, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body)
 322 {
 323   constraintList temp;
 324
 325   DPRINTF ((message ("doIf: %s ", exprNode_unparse(e) ) ) );
 326
 327   llassert(exprNode_isDefined(test) );
 328   llassert (exprNode_isDefined (e) );
 329   llassert (exprNode_isDefined (body) );
 330
 331
 332       DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) ));
 333
 334       DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) ));
 335
 336       DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->trueEnsuresConstraints) ) ));
 337
 338       DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->falseEnsuresConstraints) ) ));
 339
 340
 341
 342       DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->ensuresConstraints) ) ));
 343
 344       DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->ensuresConstraints) ) ));
 345
 346       DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->trueEnsuresConstraints) ) ));
 347
 348       DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->falseEnsuresConstraints) ) ));
 349
 350
 351
 352       temp = test->trueEnsuresConstraints;
 353       test->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(test);
 354       constraintList_free(temp);
 355
 356   temp = test->ensuresConstraints;
 357   test->ensuresConstraints = exprNode_traversEnsuresConstraints (test);
 358   constraintList_free(temp);
 359
 360   temp = test->requiresConstraints;
 361   test->requiresConstraints = exprNode_traversRequiresConstraints (test);
 362   constraintList_free(temp);
 363
 364
 365   test->trueEnsuresConstraints = constraintList_substituteFreeTarget(test->trueEnsuresConstraints, test->ensuresConstraints);
 366
 367   DPRINTF ((message ("doIf: test ensures %s ", constraintList_print(test->ensuresConstraints) ) ) );
 368
 369   DPRINTF ((message ("doIf: test true ensures %s ", constraintList_print(test->trueEnsuresConstraints) ) ) );
 370
 371   constraintList_free(e->requiresConstraints);
 372   e->requiresConstraints = constraintList_reflectChanges(body->requiresConstraints, test->trueEnsuresConstraints);
 373
 374   e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints,
 375                                            test->ensuresConstraints);
 376   temp = e->requiresConstraints;
 377   e->requiresConstraints = constraintList_mergeRequires (e->requiresConstraints, test->requiresConstraints);
 378   constraintList_free(temp);
 379
 380
 381 //drl possible problem : warning bad
 382   constraintList_free(e->ensuresConstraints);
 383   e->ensuresConstraints = constraintList_copy (test->ensuresConstraints);
 384
 385   if (exprNode_mayEscape (body) )
 386     {
 387       DPRINTF (( message("doIf: the if statement body %s returns or exits", exprNode_unparse(body) ) ));
 388       e->ensuresConstraints = constraintList_mergeEnsuresFreeFirst (e->ensuresConstraints,
 389                                                         test->falseEnsuresConstraints);
 390     }
 391
 392   DPRINTF ((message ("doIf: if requiers %s ", constraintList_print(e->requiresConstraints) ) ) );
 393
 394   return e;
 395 }
 396
 397 /*drl added 3/4/2001
 398   Also used for condition i.e. ?: operation
 399
 400   Precondition
 401   This function assumes that p, trueBranch, falseBranch have have all been traversed
 402   for constraints i.e. we assume that exprNode_traversEnsuresConstraints,
 403   exprNode_traversRequiresConstraints,  exprNode_traversTrueEnsuresConstraints,
 404   exprNode_traversFalseEnsuresConstraints have all been run
 405 */
 406
 407
 408 static exprNode doIfElse (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode p, /*@dependent@*/ exprNode trueBranch, /*@dependent@*/ exprNode falseBranch)
 409 {
 410
 411     constraintList c1, cons, t, t2, f, f2;
 412
 413   DPRINTF ((message ("doIfElse: %s ", exprNode_unparse(e) ) ) );
 414
 415     // do requires clauses
 416     c1 = constraintList_copy (p->ensuresConstraints);
 417
 418     t = constraintList_reflectChanges(trueBranch->requiresConstraints, p->trueEnsuresConstraints);
 419     t = constraintList_reflectChangesFreePre (t, p->ensuresConstraints);
 420
 421     cons = constraintList_reflectChanges(falseBranch->requiresConstraints, p->falseEnsuresConstraints);
 422     cons  = constraintList_reflectChangesFreePre (cons, c1);
 423
 424     constraintList_free(e->requiresConstraints);
 425     e->requiresConstraints = constraintList_mergeRequiresFreeFirst (t, cons);
 426     e->requiresConstraints = constraintList_mergeRequiresFreeFirst (e->requiresConstraints, p->requiresConstraints);
 427
 428     // do ensures clauses
 429     // find the  the ensures lists for each subbranch
 430     t = constraintList_mergeEnsures (p->trueEnsuresConstraints, trueBranch->ensuresConstraints);
 431     t2 = t;
 432     t = constraintList_mergeEnsures (p->ensuresConstraints, t);
 433     constraintList_free(t2);
 434
 435     f = constraintList_mergeEnsures (p->falseEnsuresConstraints, falseBranch->ensuresConstraints);
 436     f2 = f;
 437     f = constraintList_mergeEnsures (p->ensuresConstraints, f);
 438     constraintList_free(f2);
 439
 440     // find ensures for whole if/else statement
 441
 442     constraintList_free(e->ensuresConstraints);
 443
 444     e->ensuresConstraints = constraintList_logicalOr (t, f);
 445
 446     constraintList_free(t);
 447     constraintList_free(f);
 448     constraintList_free(cons);
 449     constraintList_free(c1);
 450
 451     DPRINTF ((message ("doIfElse: if requires %q ", constraintList_print(e->requiresConstraints) ) ) );
 452     DPRINTF ((message ("doIfElse: if ensures %q ", constraintList_print(e->ensuresConstraints) ) ) );
 453
 454     return e;
 455 }
 456
 457 static exprNode doWhile (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body)
 458 {
 459   DPRINTF ((message ("doWhile: %s ", exprNode_unparse(e) ) ) );
 460   return doIf (e, test, body);
 461 }
 462
 463 /*@only@*/ constraintList constraintList_makeFixedArrayConstraints (/*@observer@*/ sRefSet s)
 464 {
 465   constraintList ret;
 466   constraint con;
 467   ret = constraintList_makeNew();
 468
 469   sRefSet_elements (s, el)
 470     {
 471       //    llassert (el);
 472     if (sRef_isFixedArray(el) )
 473       {
 474         long int size;
 475         DPRINTF( (message("%s is a fixed array",
 476                           sRef_unparse(el)) ) );
 477         //if (el->kind == SK_DERIVED)
 478           //  break; //hack until I find the real problem
 479         size = sRef_getArraySize(el);
 480         DPRINTF( (message("%s is a fixed array with size %d",
 481                           sRef_unparse(el), (int)size) ) );
 482         con = constraint_makeSRefSetBufferSize (el, (size - 1));
 483         //con = constraint_makeSRefWriteSafeInt (el, (size - 1));
 484         ret = constraintList_add(ret, con);
 485       }
 486     else
 487       {
 488         DPRINTF( (message("%s is not a fixed array",
 489                           sRef_unparse(el)) ) );
 490
 491
 492     if (sRef_isExternallyVisible (el) )
 493       {
 494         /*DPRINTF( (message("%s is externally visible",
 495                           sRef_unparse(el) ) ));
 496         con = constraint_makeSRefWriteSafeInt(el, 0);
 497         ret = constraintList_add(ret, con);
 498
 499         con = constraint_makeSRefReadSafeInt(el, 0);
 500
 501         ret = constraintList_add(ret, con);*/
 502       }
 503       }
 504     }
 505   end_sRefSet_elements
 506
 507     DPRINTF(( message("constraintList_makeFixedArrayConstraints returning %s",
 508                       constraintList_print(ret) ) ));
 509     return ret;
 510 }
 511
 512 exprNode makeDataTypeConstraints (/*@returned@*/ exprNode e)
 513 {
 514   constraintList c;
 515   DPRINTF(("makeDataTypeConstraints"));
 516
 517   c = constraintList_makeFixedArrayConstraints (e->uses);
 518
 519   e->ensuresConstraints = constraintList_addListFree (e->ensuresConstraints, c);
 520
 521  return e;
 522 }
 523
 524 static void doFor (/*@dependent@*/ exprNode e, /*@dependent@*/ exprNode forPred, /*@dependent@*/ exprNode forBody)
 525 {
 526   exprNode init, test, inc;
 527   //merge the constraints: modle as if statement
 528       /* init
 529         if (test)
 530            for body
 531            inc        */
 532       init  =  exprData_getTripleInit (forPred->edata);
 533       test =   exprData_getTripleTest (forPred->edata);
 534       inc  =   exprData_getTripleInc (forPred->edata);
 535
 536       if ( ( (exprNode_isError (test) /*|| (exprNode_isError(init) )*/ ) || (exprNode_isError (inc) ) ) )
 537         {
 538           DPRINTF ((message ("strange for statement:%s, ignoring it", exprNode_unparse(e) ) ) );
 539           return;
 540         }
 541
 542       exprNode_forLoopHeuristics(e, forPred, forBody);
 543
 544       constraintList_free(e->requiresConstraints);
 545       e->requiresConstraints = constraintList_reflectChanges(forBody->requiresConstraints, test->ensuresConstraints);
 546       e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, test->trueEnsuresConstraints);
 547       e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, forPred->ensuresConstraints);
 548
 549       if (!forBody->canBreak)
 550         {
 551           e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints, constraintList_copy(forPred->ensuresConstraints) );
 552           e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints,constraintList_copy( test->falseEnsuresConstraints));
 553           //      forPred->ensuresConstraints = constraintList_undefined;
 554           //      test->falseEnsuresConstraints = constraintList_undefined;
 555         }
 556       else
 557         {
 558           DPRINTF(("Can break") );
 559         }
 560
 561 }
 562
 563 static /*@dependent@*/ exprNode exprNode_makeDependent(/*@returned@*/  exprNode e)
 564 {
 565   /*@-temptrans@*/
 566   return e;
 567   /*@=temptrans@*/
 568 }
 569
 570 static void exprNode_doGenerateConstraintSwitch (/*@dependent@*/ exprNode switchExpr,
 571                                                   /*@dependent@*/ exprNode body, /*@special@*/ constraintList * currentRequires, /*@special@*/  constraintList *
 572                                                   currentEnsures,  /*@special@*/  constraintList * savedRequires, /*@special@*/ constraintList *
 573                                                   savedEnsures)
 574      /*@post:only *currentRequires,  *currentEnsures,  *savedRequires, *savedEnsures @*/ /*@defines *currentRequires,  *currentEnsures,  *savedRequires, *savedEnsures @*/
 575 {
 576   exprNode stmt, stmtList;
 577
 578   DPRINTF(( message("exprNode_doGenerateConstraintSwitch: (switch %s) %s",
 579                     exprNode_unparse(switchExpr), exprNode_unparse(body)
 580                     ) ));
 581
 582   if (exprNode_isError(body) )
 583     {
 584       *currentRequires = constraintList_makeNew();
 585       *currentEnsures = constraintList_makeNew();
 586
 587       *savedRequires = constraintList_makeNew();
 588       *savedEnsures = constraintList_makeNew();
 589       /*@-onlytrans@*/
 590       return;
 591       /*@=onlytrans@*/
 592     }
 593
 594   if (body->kind != XPR_STMTLIST )
 595     {
 596       DPRINTF((message("exprNode_doGenerateConstraintSwitch: non
 597 stmtlist: %s",
 598                        exprNode_unparse(body) )
 599                ));
 600       //      llassert(body->kind == XPR_STMT );
 601       stmt = body;
 602       stmtList = exprNode_undefined;
 603       stmt = exprNode_makeDependent(stmt);
 604       stmtList = exprNode_makeDependent(stmtList);
 605     }
 606   else
 607     {
 608       stmt     = exprData_getPairB(body->edata);
 609       stmtList = exprData_getPairA(body->edata);
 610       stmt = exprNode_makeDependent(stmt);
 611       stmtList = exprNode_makeDependent(stmtList);
 612     }
 613
 614   DPRINTF((message("exprNode_doGenerateConstraintSwitch: stmtlist: %s
 615 stmt: %s",
 616                    exprNode_unparse(stmtList), exprNode_unparse(stmt) )
 617            ));
 618
 619
 620   exprNode_doGenerateConstraintSwitch (switchExpr, stmtList, currentRequires, currentEnsures,
 621                                        savedRequires, savedEnsures );
 622
 623   if (exprNode_isError(stmt) )
 624     /*@-onlytrans@*/
 625     return;
 626     /*@=onlytrans@*/
 627
 628   exprNode_stmt(stmt);
 629
 630   switchExpr = exprNode_makeDependent (switchExpr);
 631
 632   //, FALSE, FALSE, exprNode_getfileloc(stmt) );
 633
 634   if (! exprNode_isCaseMarker(stmt) )
 635     {
 636
 637       constraintList temp;
 638
 639       DPRINTF (( message("Got normal statement %s (requires %s ensures %s)", exprNode_unparse(stmt),
 640                          constraintList_unparse(stmt->requiresConstraints), constraintList_unparse(stmt->ensuresConstraints) ) ));
 641
 642       temp = constraintList_reflectChanges (stmt->requiresConstraints,
 643                                             *currentEnsures);
 644
 645             *currentRequires = constraintList_mergeRequiresFreeFirst(
 646                                                                      *currentRequires,
 647                                                                      temp);
 648
 649             constraintList_free(temp);
 650
 651                   *currentEnsures = constraintList_mergeEnsuresFreeFirst
 652                     (*currentEnsures,
 653                      stmt->ensuresConstraints);
 654                   DPRINTF(( message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
 655                                     "%s currentEnsures:%s",
 656                                     exprNode_unparse(switchExpr), exprNode_unparse(body),
 657                                     constraintList_print(*currentRequires), constraintList_print(*currentEnsures)
 658                                     ) ));
 659                   /*@-onlytrans@*/
 660                   return;
 661                   /*@=onlytrans@*/
 662
 663     }
 664
 665   if (exprNode_isCaseMarker(stmt) && exprNode_mustEscape(stmtList) )
 666     {
 667       // merge current and saved constraint with Logical Or...
 668       // make a constraint for ensures
 669
 670       constraintList temp;
 671       constraint con;
 672
 673       DPRINTF (( message("Got case marker") ));
 674
 675       if (constraintList_isUndefined(*savedEnsures) &&
 676           constraintList_isUndefined(*savedRequires) )
 677         {
 678           llassert(constraintList_isUndefined(*savedEnsures) );
 679           llassert(constraintList_isUndefined(*savedRequires) );
 680           *savedEnsures  = constraintList_copy(*currentEnsures);
 681           *savedRequires = constraintList_copy(*currentRequires);
 682         }
 683       else
 684         {
 685           DPRINTF (( message("Doing logical or") ));
 686           temp = constraintList_logicalOr (*savedEnsures, *currentEnsures);
 687           constraintList_free (*savedEnsures);
 688           *savedEnsures = temp;
 689
 690           *savedRequires = constraintList_mergeRequiresFreeFirst (*savedRequires, *currentRequires);
 691         }
 692
 693       con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle
 694                                         (stmt->edata), exprNode_getfileloc(stmt) );
 695
 696
 697       constraintList_free(*currentEnsures);
 698       *currentEnsures = constraintList_makeNew();
 699       *currentEnsures = constraintList_add(*currentEnsures, con);
 700
 701       constraintList_free(*currentRequires);
 702       *currentRequires = constraintList_makeNew();
 703       DPRINTF(( message("exprNode_doGenerateConstraintSwitch: (switch %s) %s savedRequires:"
 704                         "%s savedEnsures:%s",
 705                         exprNode_unparse(switchExpr), exprNode_unparse(body),
 706                         constraintList_print(*savedRequires), constraintList_print(*savedEnsures)
 707                         ) ));
 708
 709     }
 710
 711   else if (exprNode_isCaseMarker(stmt) )
 712     //prior case has no break.
 713     {
 714       // We don't do anything to the sved constraints because the case hasn't ended
 715       //The new ensures constraints for the case will be:
 716       // the constraint for the case statement (CASE_LABEL == SWITCH_EXPR) logicalOr currentEnsures
 717
 718       constraintList temp;
 719       constraint con;
 720
 721       constraintList ensuresTemp;
 722
 723       DPRINTF (( message("Got case marker with no prior break") ));
 724
 725       con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle
 726                                         (stmt->edata), exprNode_getfileloc(stmt) );
 727
 728       ensuresTemp = constraintList_makeNew();
 729
 730       ensuresTemp = constraintList_add (ensuresTemp, con);
 731
 732       if (exprNode_isError(stmtList) )
 733         {
 734           constraintList_free(*currentEnsures);
 735
 736           *currentEnsures = constraintList_copy(ensuresTemp);
 737           constraintList_free(ensuresTemp);
 738
 739         }
 740       else
 741         {
 742
 743           temp = constraintList_logicalOr (*currentEnsures, ensuresTemp);
 744
 745           constraintList_free(*currentEnsures);
 746           constraintList_free(ensuresTemp);
 747
 748           *currentEnsures = temp;
 749         }
 750       constraintList_free(*currentRequires);
 751
 752       *currentRequires = constraintList_makeNew();
 753     }
 754   else
 755     {
 756       // we handle the case of ! exprNode_isCaseMarker above
 757       // the else if clause should always be true.
 758       BADEXIT;
 759     }
 760
 761   DPRINTF(( message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
 762                     "%s currentEnsures:%s",
 763                     exprNode_unparse(switchExpr), exprNode_unparse(body),
 764                     constraintList_print(*currentRequires), constraintList_print(*currentEnsures)
 765                     ) ));
 766   /*@-onlytrans@*/
 767   return;
 768   /*@=onlytrans@*/
 769
 770 }
 771
 772
 773 static void exprNode_generateConstraintSwitch ( exprNode switchStmt)
 774 {
 775   constraintList constraintsRequires;
 776   constraintList constraintsEnsures;
 777   constraintList lastRequires;
 778   constraintList lastEnsures;
 779
 780   exprNode body;
 781   exprNode switchExpr;
 782
 783   switchExpr = exprData_getPairA(switchStmt->edata);
 784   body = exprData_getPairB(switchStmt->edata);
 785
 786   /*@i22*/
 787   if ( body->kind == XPR_BLOCK)
 788     body = exprData_getSingle(body->edata);
 789
 790   /*
 791   constraintsRequires = constraintList_undefined;
 792   constraintsEnsures = constraintList_undefined;
 793
 794   lastRequires = constraintList_makeNew();
 795   lastEnsures = constraintList_makeNew();
 796   */
 797
 798   exprNode_doGenerateConstraintSwitch (switchExpr, body, &lastRequires, &lastEnsures, &constraintsRequires, &constraintsEnsures);
 799
 800   // merge current and saved constraint with Logical Or...
 801   // make a constraint for ensures
 802
 803   constraintList_free(switchStmt->requiresConstraints);
 804   constraintList_free(switchStmt->ensuresConstraints);
 805
 806   if (constraintList_isDefined(constraintsEnsures) && constraintList_isDefined(constraintsRequires) )
 807     {
 808       switchStmt->ensuresConstraints = constraintList_logicalOr(constraintsEnsures, lastEnsures);
 809       switchStmt->requiresConstraints =   constraintList_mergeRequires(constraintsRequires, lastRequires);
 810       constraintList_free (constraintsRequires);
 811       constraintList_free (constraintsEnsures);
 812     }
 813   else
 814     {
 815       switchStmt->ensuresConstraints =    constraintList_copy(lastEnsures);
 816       switchStmt->requiresConstraints =   constraintList_copy(lastRequires);
 817     }
 818
 819   constraintList_free (lastRequires);
 820   constraintList_free (lastEnsures);
 821
 822   DPRINTF(( (message(" exprNode_generateConstraintSwitch returning requires: %s and ensures %s",
 823                      constraintList_print( switchStmt->requiresConstraints),
 824                      constraintList_print( switchStmt->ensuresConstraints)
 825                      )
 826              ) ));
 827 }
 828
 829 static exprNode doSwitch (/*@returned@*/ exprNode e)
 830 {
 831   exprNode body;
 832   exprData data;
 833
 834   data = e->edata;
 835   //  llassert(FALSE);
 836   DPRINTF (( message ("doSwitch for: switch (%s) %s",
 837                       exprNode_unparse (exprData_getPairA (data)),
 838                       exprNode_unparse (exprData_getPairB (data))) ));
 839
 840   body = exprData_getPairB (data);
 841
 842   exprNode_generateConstraints(body);
 843
 844   exprNode_generateConstraintSwitch (e);
 845
 846   //  e->requiresConstraints = constraintList_copy (body->requiresConstraints );
 847   // e->ensuresConstraints = constraintList_copy (body->ensuresConstraints );
 848
 849   return e;
 850 }
 851
 852
 853
 854
 855 void exprNode_multiStatement (/*@dependent@*/ exprNode e)
 856 {
 857
 858   bool ret;
 859   exprData data;
 860   exprNode e1, e2;
 861   exprNode p, trueBranch, falseBranch;
 862   exprNode forPred, forBody;
 863   exprNode test;
 864
 865   constraintList temp;
 866
 867   //  constraintList t, f;
 868   /*e->requiresConstraints = constraintList_makeNew();
 869   e->ensuresConstraints = constraintList_makeNew();
 870   e->trueEnsuresConstraints = constraintList_makeNew();
 871   e->falseEnsuresConstraints = constraintList_makeNew();
 872   */
 873   //  e = makeDataTypeConstraints(e);
 874
 875   DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse( e),
 876                     fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
 877
 878   if (exprNode_handleError (e))
 879     {
 880       return; // FALSE;
 881     }
 882
 883   data = e->edata;
 884
 885   ret = TRUE;
 886
 887   switch (e->kind)
 888     {
 889
 890     case XPR_FOR:
 891       // ret = message ("%s %s",
 892       forPred = exprData_getPairA (data);
 893       forBody = exprData_getPairB (data);
 894
 895       //first generate the constraints
 896       exprNode_generateConstraints (forPred);
 897       exprNode_generateConstraints (forBody);
 898
 899
 900       doFor (e, forPred, forBody);
 901
 902       break;
 903
 904     case XPR_FORPRED:
 905       //            ret = message ("for (%s; %s; %s)",
 906       exprNode_generateConstraints (exprData_getTripleInit (data) );
 907       test = exprData_getTripleTest (data);
 908       exprNode_exprTraverse (test,FALSE, FALSE, exprNode_loc(e));
 909       exprNode_generateConstraints (exprData_getTripleInc (data) );
 910
 911       if (!exprNode_isError(test) )
 912         {
 913           constraintList temp2;
 914           temp2 = test->trueEnsuresConstraints;
 915           test->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(test);
 916           constraintList_free(temp2);
 917         }
 918
 919       exprNode_generateConstraints (exprData_getTripleInc (data));
 920       break;
 921
 922     case XPR_WHILE:
 923       e1 = exprData_getPairA (data);
 924       e2 = exprData_getPairB (data);
 925
 926        exprNode_exprTraverse (e1,
 927                               FALSE, FALSE, exprNode_loc(e1));
 928
 929        exprNode_generateConstraints (e2);
 930
 931        e = doWhile (e, e1, e2);
 932
 933       break;
 934
 935     case XPR_IF:
 936       DPRINTF(( "IF:") );
 937       DPRINTF ((exprNode_unparse(e) ) );
 938       //      ret = message ("if (%s) %s",
 939       e1 = exprData_getPairA (data);
 940       e2 = exprData_getPairB (data);
 941
 942       exprNode_exprTraverse (e1,
 943                              FALSE, FALSE, exprNode_loc(e1));
 944
 945       exprNode_generateConstraints (e2);
 946       e = doIf (e, e1, e2);
 947
 948
 949       //      e->constraints = constraintList_exprNodemerge (exprData_getPairA (data),exprData_getPairB(data));
 950       break;
 951
 952
 953     case XPR_IFELSE:
 954       DPRINTF(("Starting IFELSE"));
 955       //      ret = message ("if (%s) %s else %s",
 956       p = exprData_getTriplePred (data);
 957       trueBranch = exprData_getTripleTrue (data);
 958       falseBranch = exprData_getTripleFalse (data);
 959
 960       exprNode_exprTraverse (p,
 961                              FALSE, FALSE, exprNode_loc(p));
 962       exprNode_generateConstraints (trueBranch);
 963       exprNode_generateConstraints (falseBranch);
 964
 965       temp = p->ensuresConstraints;
 966       p->ensuresConstraints = exprNode_traversEnsuresConstraints (p);
 967       constraintList_free(temp);
 968
 969       temp = p->requiresConstraints;
 970       p->requiresConstraints = exprNode_traversRequiresConstraints (p);
 971       constraintList_free(temp);
 972
 973       temp = p->trueEnsuresConstraints;
 974       p->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(p);
 975       constraintList_free(temp);
 976
 977       temp = p->falseEnsuresConstraints;
 978       p->falseEnsuresConstraints =  exprNode_traversFalseEnsuresConstraints(p);
 979       constraintList_free(temp);
 980
 981           e = doIfElse (e, p, trueBranch, falseBranch);
 982       DPRINTF( ("Done IFELSE") );
 983       break;
 984
 985     case XPR_DOWHILE:
 986
 987       e2 = (exprData_getPairB (data));
 988       e1 = (exprData_getPairA (data));
 989
 990       DPRINTF((message ("do { %s } while (%s)", exprNode_unparse(e2), exprNode_unparse(e1) ) ));
 991       exprNode_generateConstraints (e2);
 992       exprNode_generateConstraints (e1);
 993       e = exprNode_copyConstraints (e, e2);
 994       DPRINTF ((message ("e = %s  ", constraintList_print(e->requiresConstraints) ) ));
 995
 996       break;
 997
 998     case XPR_BLOCK:
 999       //      ret = message ("{ %s }",
1000                      exprNode_generateConstraints (exprData_getSingle (data));
1001
1002                      constraintList_free(e->requiresConstraints);
1003                      e->requiresConstraints = constraintList_copy ( (exprData_getSingle (data))->requiresConstraints );
1004
1005                      constraintList_free(e->ensuresConstraints);
1006                      e->ensuresConstraints = constraintList_copy ( (exprData_getSingle (data))->ensuresConstraints );
1007                      //      e->constraints = (exprData_getSingle (data))->constraints;
1008       break;
1009
1010     case XPR_SWITCH:
1011       e = doSwitch (e);
1012       break;
1013     case XPR_STMT:
1014     case XPR_STMTLIST:
1015       exprNode_stmtList (e);
1016       return ;
1017       /*@notreached@*/
1018       break;
1019     default:
1020       ret=FALSE;
1021     }
1022   return; // ret;
1023 }
1024
1025 static bool lltok_isBoolean_Op (lltok tok)
1026 {
1027   /*this should really be a switch statement but
1028     I don't want to violate the abstraction
1029     maybe this should go in lltok.c */
1030
1031   if (lltok_isEq_Op (tok) )
1032         {
1033           return TRUE;
1034         }
1035       if (lltok_isAnd_Op (tok) )
1036
1037         {
1038
1039           return TRUE;
1040         }
1041    if (lltok_isOr_Op (tok) )
1042         {
1043           return TRUE;
1044         }
1045
1046    if (lltok_isGt_Op (tok) )
1047      {
1048        return TRUE;
1049      }
1050    if (lltok_isLt_Op (tok) )
1051      {
1052        return TRUE;
1053      }
1054
1055    if (lltok_isLe_Op (tok) )
1056      {
1057        return TRUE;
1058      }
1059
1060    if (lltok_isGe_Op (tok) )
1061      {
1062        return TRUE;
1063      }
1064
1065    return FALSE;
1066
1067 }
1068
1069
1070 static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ bool definatelv, /*@unused@*/ bool definaterv,  fileloc sequencePoint)
1071 {
1072  constraint cons;
1073 exprNode t1, t2;
1074 exprData data;
1075 lltok tok;
1076 constraintList tempList, temp;
1077 data = e->edata;
1078
1079 tok = exprData_getOpTok (data);
1080
1081
1082 t1 = exprData_getOpA (data);
1083 t2 = exprData_getOpB (data);
1084
1085
1086  tempList = constraintList_undefined;
1087
1088 /* arithmetic tests */
1089
1090 if (lltok_isEq_Op (tok) )
1091 {
1092   cons =  constraint_makeEnsureEqual (t1, t2, sequencePoint);
1093   e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1094 }
1095
1096
1097  if (lltok_isLt_Op (tok) )
1098    {
1099      cons =  constraint_makeEnsureLessThan (t1, t2, sequencePoint);
1100      e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1101      cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
1102      e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1103    }
1104
1105
1106 if (lltok_isGe_Op (tok) )
1107 {
1108
1109   cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
1110   e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1111
1112   cons =  constraint_makeEnsureLessThan (t1, t2, sequencePoint);
1113   e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1114
1115 }
1116
1117
1118   if (lltok_isGt_Op (tok) )
1119 {
1120   cons =  constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
1121   e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1122   cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
1123   e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1124 }
1125
1126 if (lltok_isLe_Op (tok) )
1127 {
1128    cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
1129   e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1130
1131   cons =  constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
1132   e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1133 }
1134
1135
1136
1137 /*Logical operations */
1138
1139
1140  if (lltok_isAnd_Op (tok) )
1141
1142    {
1143      //true ensures
1144      tempList = constraintList_copy (t1->trueEnsuresConstraints);
1145      tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
1146      e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList);
1147
1148       //false ensures: fens t1 or tens t1 and fens t2
1149      tempList = constraintList_copy (t1->trueEnsuresConstraints);
1150      tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
1151      temp = tempList;
1152      tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints);
1153      constraintList_free (temp);
1154
1155      /* evans - was constraintList_addList - memory leak detected by lclint */
1156      e->falseEnsuresConstraints =constraintList_addListFree (e->falseEnsuresConstraints, tempList);
1157    }
1158  else if (lltok_isOr_Op (tok) )
1159   {
1160       //false ensures
1161       tempList = constraintList_copy (t1->falseEnsuresConstraints);
1162       tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
1163       e->falseEnsuresConstraints = constraintList_addListFree(e->falseEnsuresConstraints, tempList);
1164
1165       //true ensures: tens t1 or fens t1 and tens t2
1166       tempList = constraintList_copy (t1->falseEnsuresConstraints);
1167       tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
1168
1169       temp = tempList;
1170       tempList = constraintList_logicalOr (tempList, t1->trueEnsuresConstraints);
1171       constraintList_free(temp);
1172
1173       e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList);
1174       tempList = constraintList_undefined;
1175     }
1176  else
1177     {
1178       DPRINTF((message("%s is not a boolean operation", lltok_unparse(tok) ) ));
1179     }
1180 }
1181
1182 void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv,  /*@observer@*/ /*@temp@*/ fileloc sequencePoint)
1183 {
1184   exprNode t1, t2, fcn;
1185   lltok tok;
1186   bool handledExprNode;
1187   exprData data;
1188   constraint cons;
1189
1190   constraintList temp;
1191
1192   if (exprNode_isError(e) )
1193     {
1194       return; // FALSE;
1195     }
1196
1197   DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e),
1198                     fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
1199
1200   /*e->requiresConstraints = constraintList_makeNew();
1201   e->ensuresConstraints = constraintList_makeNew();
1202   e->trueEnsuresConstraints = constraintList_makeNew();;
1203   e->falseEnsuresConstraints = constraintList_makeNew();;
1204   */
1205   if (exprNode_isUnhandled (e) )
1206      {
1207        return; // FALSE;
1208      }
1209    //   e = makeDataTypeConstraints (e);
1210
1211    handledExprNode = TRUE;
1212
1213   data = e->edata;
1214
1215   switch (e->kind)
1216     {
1217     case XPR_WHILEPRED:
1218       t1 = exprData_getSingle (data);
1219       exprNode_exprTraverse (t1,  definatelv, definaterv, sequencePoint);
1220       e = exprNode_copyConstraints (e, t1);
1221       break;
1222
1223     case XPR_FETCH:
1224
1225       if (definatelv )
1226         {
1227           t1 =  (exprData_getPairA (data) );
1228           t2 =  (exprData_getPairB (data) );
1229           cons =  constraint_makeWriteSafeExprNode (t1, t2);
1230         }
1231       else
1232         {
1233           t1 =  (exprData_getPairA (data) );
1234           t2 =  (exprData_getPairB (data) );
1235           cons = constraint_makeReadSafeExprNode (t1, t2 );
1236         }
1237
1238       e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
1239       cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint);
1240       e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1241
1242       cons = constraint_makeEnsureLteMaxRead (t2, t1);
1243       e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1244
1245       //      cons = constraint_makeEnsureMinReadAtMost (t1, t2, sequencePoint);
1246       // e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1247
1248       exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
1249       exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
1250
1251             /*@i325 Should check which is array/index. */
1252       break;
1253
1254     case XPR_PARENS:
1255       exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint);
1256       //    e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined);
1257       break;
1258     case XPR_INIT:
1259       {
1260         /*
1261         idDecl t;
1262
1263         uentry ue;
1264         exprNode lhs;
1265
1266         t = exprData_getInitId (data);
1267         ue = usymtab_lookup (idDecl_observeId (t));
1268         lhs = exprNode_createId (ue);
1269         */
1270         t2 = exprData_getInitNode (data);
1271
1272         /*      DPRINTF(( (message("initialization: %s = %s",
1273                            exprNode_unparse(lhs),
1274                            exprNode_unparse(t2)
1275                            )
1276                    ) ));        */
1277
1278         //exprNode_exprTraverse (t1, TRUE, FALSE, sequencePoint );
1279
1280         exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
1281
1282         /* this test is nessecary because some expressions generate a null expression node.  function pointer do that -- drl */
1283         if ( (!exprNode_isError (e))  &&  (!exprNode_isError(t2)) )
1284           {
1285             cons =  constraint_makeEnsureEqual (e, t2, sequencePoint);
1286             e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1287           }
1288       }
1289
1290       break;
1291     case XPR_ASSIGN:
1292       t1 = exprData_getOpA (data);
1293       t2 = exprData_getOpB (data);
1294       exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
1295       //lltok_unparse (exprData_getOpTok (data));
1296
1297       exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
1298
1299       /* this test is nessecary because some expressions generate a null expression node.  function pointer do that -- drl */
1300       if ( (!exprNode_isError (t1))  &&  (!exprNode_isError(t2)) )
1301         {
1302           cons =  constraint_makeEnsureEqual (t1, t2, sequencePoint);
1303           e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1304         }
1305       break;
1306     case XPR_OP:
1307       t1 = exprData_getOpA (data);
1308       t2 = exprData_getOpB (data);
1309       tok = exprData_getOpTok (data);
1310
1311
1312       if (tok.tok == ADD_ASSIGN)
1313         {
1314           exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
1315           exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
1316
1317           cons = constraint_makeAddAssign (t1, t2,  sequencePoint );
1318           e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1319         }
1320       else if (tok.tok == SUB_ASSIGN)
1321         {
1322           exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
1323           exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
1324
1325           cons = constraint_makeSubtractAssign (t1, t2,  sequencePoint );
1326           e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1327         }
1328       else
1329         {
1330           exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
1331           exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
1332         }
1333
1334       if (lltok_isBoolean_Op (tok) )
1335         exprNode_booleanTraverse (e, definatelv, definaterv, sequencePoint);
1336
1337       //      e->constraints  = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data));
1338       break;
1339     case XPR_SIZEOFT:
1340       //drl possible problem : warning make sure the case can be ignored..
1341
1342       break;
1343
1344     case XPR_SIZEOF:
1345       /* drl  7-16-01
1346          C standard says operand to sizeof isn't evaluated unless
1347          its a variable length array.  So we don't generate constraints.
1348       */
1349
1350       //      exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
1351       //      e->constraints = constraintList_exprNodemerge (exprData_getSingle (e->edata), exprNode_undefined);
1352       break;
1353
1354     case XPR_CALL:
1355       fcn = exprData_getFcn(data);
1356
1357       exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint );
1358       DPRINTF ( (message ("Got call that %s ( %s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (exprData_getArgs (data) ) ) ) );
1359
1360       fcn->requiresConstraints = constraintList_addListFree (fcn->requiresConstraints,
1361                                                  checkCall (fcn, exprData_getArgs (data)  ) );
1362
1363       fcn->ensuresConstraints = constraintList_addListFree (fcn->ensuresConstraints,
1364                                                  exprNode_getPostConditions(fcn, exprData_getArgs (data),e  ) );
1365
1366       t1 = exprNode_createNew (exprNode_getType (e) );
1367
1368       checkArgumentList (t1, exprData_getArgs(data), sequencePoint);
1369
1370
1371       exprNode_mergeResolve (e, t1, fcn);
1372
1373       exprNode_free(t1);
1374
1375       //      e->constraints = constraintList_add (e->constraints, constraint_create (e,exprNode_undefined, GT,  CALLSAFE ) );
1376
1377       break;
1378
1379     case XPR_RETURN:
1380       exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
1381       break;
1382
1383     case XPR_NULLRETURN:
1384
1385       break;
1386
1387
1388     case XPR_FACCESS:
1389       exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
1390       break;
1391
1392     case XPR_ARROW:
1393       exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
1394       break;
1395
1396     case XPR_STRINGLITERAL:
1397
1398       break;
1399
1400     case XPR_NUMLIT:
1401
1402       break;
1403
1404     case XPR_PREOP:
1405       t1 = exprData_getUopNode(data);
1406       tok = (exprData_getUopTok (data));
1407       //lltok_unparse (exprData_getUopTok (data));
1408       exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
1409       /*handle * pointer access */
1410       if (lltok_isInc_Op (tok) )
1411         {
1412           DPRINTF(("doing ++(var)"));
1413           t1 = exprData_getUopNode (data);
1414           cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
1415           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1416         }
1417       else if (lltok_isDec_Op (tok) )
1418         {
1419           DPRINTF(("doing --(var)"));
1420           t1 = exprData_getUopNode (data);
1421           cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint );
1422           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1423         }
1424       else if (lltok_isMult( tok  ) )
1425         {
1426           if (definatelv)
1427             {
1428               cons = constraint_makeWriteSafeInt (t1, 0);
1429             }
1430           else
1431             {
1432               cons = constraint_makeReadSafeInt (t1, 0);
1433             }
1434               e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
1435         }
1436       else if (lltok_isNot_Op (tok) )
1437         /* ! expr */
1438         {
1439           constraintList_free(e->trueEnsuresConstraints);
1440
1441           e->trueEnsuresConstraints  = constraintList_copy (t1->falseEnsuresConstraints);
1442           constraintList_free(e->falseEnsuresConstraints);
1443           e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints);
1444         }
1445
1446       else if (lltok_isAmpersand_Op (tok) )
1447         {
1448           break;
1449         }
1450       else if (lltok_isMinus_Op (tok) )
1451         {
1452           break;
1453         }
1454       else if ( lltok_isExcl_Op (tok) )
1455         {
1456           break;
1457         }
1458       else if (lltok_isTilde_Op (tok) )
1459         {
1460           break;
1461         }
1462       else
1463         {
1464           llcontbug((message("Unsupported preop in %s", exprNode_unparse(e) ) ));
1465           BADEXIT;
1466         }
1467       break;
1468
1469     case XPR_POSTOP:
1470
1471       exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint );
1472
1473       if (lltok_isInc_Op (exprData_getUopTok (data) ) )
1474         {
1475           DPRINTF(("doing ++"));
1476           t1 = exprData_getUopNode (data);
1477           cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
1478           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1479         }
1480        if (lltok_isDec_Op (exprData_getUopTok (data) ) )
1481         {
1482           DPRINTF(("doing --"));
1483           t1 = exprData_getUopNode (data);
1484           cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint );
1485           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1486         }
1487       break;
1488     case XPR_CAST:
1489       {
1490         t2 =  exprData_getCastNode (data);
1491         DPRINTF (( message ("Examining cast (%q)%s",
1492                             qtype_unparse (exprData_getCastType (data)),
1493                             exprNode_unparse (t2) )
1494                    ));
1495         exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
1496       }
1497       break;
1498
1499     case XPR_COND:
1500       {
1501         exprNode pred, trueBranch, falseBranch;
1502            llassert(FALSE);
1503       pred = exprData_getTriplePred (data);
1504       trueBranch = exprData_getTripleTrue (data);
1505       falseBranch = exprData_getTripleFalse (data);
1506
1507       exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint );
1508
1509       temp =       pred->ensuresConstraints;
1510       pred->ensuresConstraints = exprNode_traversEnsuresConstraints(pred);
1511       constraintList_free(temp);
1512
1513       temp =       pred->requiresConstraints;
1514       pred->requiresConstraints = exprNode_traversRequiresConstraints(pred);
1515       constraintList_free(temp);
1516
1517       temp =       pred->trueEnsuresConstraints;
1518       pred->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(pred);
1519       constraintList_free(temp);
1520
1521       temp =       pred->falseEnsuresConstraints;
1522       pred->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(pred);
1523       constraintList_free(temp);
1524
1525
1526       exprNode_exprTraverse (trueBranch, FALSE, TRUE, sequencePoint );
1527
1528       temp =       trueBranch->ensuresConstraints;
1529       trueBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(trueBranch);
1530       constraintList_free(temp);
1531
1532
1533       temp =       trueBranch->requiresConstraints;
1534       trueBranch->requiresConstraints = exprNode_traversRequiresConstraints(trueBranch);
1535       constraintList_free(temp);
1536
1537
1538       temp =       trueBranch->trueEnsuresConstraints;
1539       trueBranch->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(trueBranch);
1540       constraintList_free(temp);
1541
1542       temp =       trueBranch->falseEnsuresConstraints;
1543       trueBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(trueBranch);
1544       constraintList_free(temp);
1545
1546       //dfdf
1547       exprNode_exprTraverse (falseBranch, FALSE, TRUE, sequencePoint );
1548
1549       temp =       falseBranch->ensuresConstraints;
1550       falseBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(falseBranch);
1551       constraintList_free(temp);
1552
1553
1554       temp =       falseBranch->requiresConstraints;
1555       falseBranch->requiresConstraints = exprNode_traversRequiresConstraints(falseBranch);
1556       constraintList_free(temp);
1557
1558
1559       temp =       falseBranch->trueEnsuresConstraints;
1560       falseBranch->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(falseBranch);
1561       constraintList_free(temp);
1562
1563       temp =       falseBranch->falseEnsuresConstraints;
1564       falseBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(falseBranch);
1565       constraintList_free(temp);
1566
1567       /* if pred is true e equals true otherwise pred equals false */
1568
1569       cons =  constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
1570       trueBranch->ensuresConstraints = constraintList_add(trueBranch->ensuresConstraints, cons);
1571
1572       cons =  constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
1573       falseBranch->ensuresConstraints = constraintList_add(falseBranch->ensuresConstraints, cons);
1574
1575       e = doIfElse (e, pred, trueBranch, falseBranch);
1576
1577       }
1578       break;
1579     case XPR_COMMA:
1580       llassert(FALSE);
1581       t1 = exprData_getPairA (data);
1582       t2 = exprData_getPairB (data);
1583     /* we essiantially treat this like expr1; expr2
1584      of course sequencePoint isn't adjusted so this isn't completely accurate
1585     problems../  */
1586       exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint );
1587       exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
1588       exprNode_mergeResolve (e, t1, t2);
1589       break;
1590
1591     default:
1592       handledExprNode = FALSE;
1593     }
1594
1595   e->requiresConstraints =  constraintList_preserveOrig ( e->requiresConstraints);
1596   e->ensuresConstraints  =  constraintList_preserveOrig ( e->ensuresConstraints);
1597   e->requiresConstraints = constraintList_addGeneratingExpr ( e->requiresConstraints, e);
1598
1599   e->ensuresConstraints  = constraintList_addGeneratingExpr ( e->ensuresConstraints, e);
1600
1601   DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) ));
1602
1603   DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) ));
1604
1605   DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->trueEnsuresConstraints) ) ));
1606
1607   DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->falseEnsuresConstraints) ) ));
1608
1609   return; // handledExprNode;
1610 }
1611
1612
1613 constraintList exprNode_traversTrueEnsuresConstraints (exprNode e)
1614 {
1615   exprNode t1;
1616
1617   bool handledExprNode;
1618   //  char * mes;
1619   exprData data;
1620   constraintList ret;
1621
1622   if (exprNode_handleError (e))
1623     {
1624       ret = constraintList_makeNew();
1625       return ret;
1626     }
1627   ret = constraintList_copy (e->trueEnsuresConstraints );
1628
1629   handledExprNode = TRUE;
1630
1631   data = e->edata;
1632
1633   switch (e->kind)
1634     {
1635     case XPR_WHILEPRED:
1636       t1 = exprData_getSingle (data);
1637       ret = constraintList_addListFree ( ret, exprNode_traversTrueEnsuresConstraints (t1) );
1638       break;
1639
1640     case XPR_FETCH:
1641
1642       ret = constraintList_addListFree (ret,
1643                                     exprNode_traversTrueEnsuresConstraints
1644                                     (exprData_getPairA (data) ) );
1645
1646       ret = constraintList_addListFree (ret,
1647                                     exprNode_traversTrueEnsuresConstraints
1648                                     (exprData_getPairB (data) ) );
1649       break;
1650     case XPR_PREOP:
1651
1652       ret = constraintList_addListFree (ret,
1653                                     exprNode_traversTrueEnsuresConstraints
1654                                     (exprData_getUopNode (data) ) );
1655       break;
1656
1657     case XPR_PARENS:
1658       ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints
1659                                     (exprData_getUopNode (data) ) );
1660       break;
1661
1662     case XPR_INIT:
1663       ret = constraintList_addListFree (ret,
1664                                         exprNode_traversTrueEnsuresConstraints
1665                                         (exprData_getInitNode (data) ) );
1666         break;
1667
1668
1669     case XPR_ASSIGN:
1670         ret = constraintList_addListFree (ret,
1671                                     exprNode_traversTrueEnsuresConstraints
1672                                     (exprData_getOpA (data) ) );
1673
1674        ret = constraintList_addListFree (ret,
1675                                     exprNode_traversTrueEnsuresConstraints
1676                                     (exprData_getOpB (data) ) );
1677        break;
1678     case XPR_OP:
1679        ret = constraintList_addListFree (ret,
1680                                     exprNode_traversTrueEnsuresConstraints
1681                                     (exprData_getOpA (data) ) );
1682
1683        ret = constraintList_addListFree (ret,
1684                                     exprNode_traversTrueEnsuresConstraints
1685                                     (exprData_getOpB (data) ) );
1686        break;
1687     case XPR_SIZEOFT:
1688
1689       //      ctype_unparse (qtype_getType (exprData_getType (data) ) );
1690
1691       break;
1692
1693     case XPR_SIZEOF:
1694
1695        ret = constraintList_addListFree (ret,
1696                                          exprNode_traversTrueEnsuresConstraints
1697                                          (exprData_getSingle (data) ) );
1698        break;
1699
1700     case XPR_CALL:
1701       ret = constraintList_addListFree (ret,
1702                                      exprNode_traversTrueEnsuresConstraints
1703                                     (exprData_getFcn (data) ) );
1704       /*@i11*/      //   exprNodeList_unparse (exprData_getArgs (data) );
1705          break;
1706
1707     case XPR_RETURN:
1708       ret = constraintList_addListFree (ret,
1709                                     exprNode_traversTrueEnsuresConstraints
1710                                     (exprData_getSingle (data) ) );
1711       break;
1712
1713     case XPR_NULLRETURN:
1714       //      cstring_makeLiteral ("return");;
1715       break;
1716
1717     case XPR_FACCESS:
1718           ret = constraintList_addListFree (ret,
1719                                     exprNode_traversTrueEnsuresConstraints
1720                                     (exprData_getFieldNode (data) ) );
1721        //exprData_getFieldName (data) ;
1722       break;
1723
1724     case XPR_ARROW:
1725         ret = constraintList_addListFree (ret,
1726                                     exprNode_traversTrueEnsuresConstraints
1727                                     (exprData_getFieldNode (data) ) );
1728         //      exprData_getFieldName (data);
1729       break;
1730
1731     case XPR_STRINGLITERAL:
1732       //      cstring_copy (exprData_getLiteral (data));
1733       break;
1734
1735     case XPR_NUMLIT:
1736       //      cstring_copy (exprData_getLiteral (data));
1737       break;
1738     case XPR_POSTOP:
1739
1740            ret = constraintList_addListFree (ret,
1741                                     exprNode_traversTrueEnsuresConstraints
1742                                     (exprData_getUopNode (data) ) );
1743            break;
1744
1745     case XPR_CAST:
1746
1747       ret = constraintList_addListFree (ret,
1748                                     exprNode_traversTrueEnsuresConstraints
1749                                     (exprData_getCastNode (data) ) );
1750       break;
1751
1752     default:
1753       break;
1754     }
1755
1756   return ret;
1757 }
1758
1759 constraintList exprNode_traversFalseEnsuresConstraints (exprNode e)
1760 {
1761    exprNode t1;
1762
1763   bool handledExprNode;
1764   //  char * mes;
1765   exprData data;
1766   constraintList ret;
1767
1768    if (exprNode_handleError (e))
1769      {
1770        ret = constraintList_makeNew();
1771        return ret;
1772      }
1773   ret = constraintList_copy (e->falseEnsuresConstraints );
1774
1775    handledExprNode = TRUE;
1776
1777   data = e->edata;
1778
1779   switch (e->kind)
1780     {
1781    case XPR_WHILEPRED:
1782       t1 = exprData_getSingle (data);
1783       ret = constraintList_addListFree ( ret,exprNode_traversFalseEnsuresConstraints (t1) );
1784       break;
1785
1786     case XPR_FETCH:
1787
1788       ret = constraintList_addListFree (ret,
1789                                     exprNode_traversFalseEnsuresConstraints
1790                                     (exprData_getPairA (data) ) );
1791
1792       ret = constraintList_addListFree (ret,
1793                                     exprNode_traversFalseEnsuresConstraints
1794                                     (exprData_getPairB (data) ) );
1795       break;
1796     case XPR_PREOP:
1797
1798       ret = constraintList_addListFree (ret,
1799                                     exprNode_traversFalseEnsuresConstraints
1800                                     (exprData_getUopNode (data) ) );
1801       break;
1802
1803     case XPR_PARENS:
1804       ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints
1805                                     (exprData_getUopNode (data) ) );
1806       break;
1807     case XPR_INIT:
1808         ret = constraintList_addListFree (ret,
1809                                     exprNode_traversFalseEnsuresConstraints
1810                                     (   exprData_getInitNode (data) ) );
1811         break;
1812
1813     case XPR_ASSIGN:
1814         ret = constraintList_addListFree (ret,
1815                                     exprNode_traversFalseEnsuresConstraints
1816                                     (exprData_getOpA (data) ) );
1817
1818        ret = constraintList_addListFree (ret,
1819                                     exprNode_traversFalseEnsuresConstraints
1820                                     (exprData_getOpB (data) ) );
1821        break;
1822     case XPR_OP:
1823        ret = constraintList_addListFree (ret,
1824                                     exprNode_traversFalseEnsuresConstraints
1825                                     (exprData_getOpA (data) ) );
1826
1827        ret = constraintList_addListFree (ret,
1828                                     exprNode_traversFalseEnsuresConstraints
1829                                     (exprData_getOpB (data) ) );
1830        break;
1831     case XPR_SIZEOFT:
1832
1833       //      ctype_unparse (qtype_getType (exprData_getType (data) ) );
1834
1835       break;
1836
1837     case XPR_SIZEOF:
1838
1839        ret = constraintList_addListFree (ret,
1840                                     exprNode_traversFalseEnsuresConstraints
1841                                      (exprData_getSingle (data) ) );
1842        break;
1843
1844     case XPR_CALL:
1845       ret = constraintList_addListFree (ret,
1846                                      exprNode_traversFalseEnsuresConstraints
1847                                     (exprData_getFcn (data) ) );
1848       /*@i11*/      //   exprNodeList_unparse (exprData_getArgs (data) );
1849          break;
1850
1851     case XPR_RETURN:
1852       ret = constraintList_addListFree (ret,
1853                                     exprNode_traversFalseEnsuresConstraints
1854                                     (exprData_getSingle (data) ) );
1855       break;
1856
1857     case XPR_NULLRETURN:
1858       //      cstring_makeLiteral ("return");;
1859       break;
1860
1861     case XPR_FACCESS:
1862           ret = constraintList_addListFree (ret,
1863                                     exprNode_traversFalseEnsuresConstraints
1864                                     (exprData_getFieldNode (data) ) );
1865        //exprData_getFieldName (data) ;
1866       break;
1867
1868     case XPR_ARROW:
1869         ret = constraintList_addListFree (ret,
1870                                     exprNode_traversFalseEnsuresConstraints
1871                                     (exprData_getFieldNode (data) ) );
1872         //      exprData_getFieldName (data);
1873       break;
1874
1875     case XPR_STRINGLITERAL:
1876       //      cstring_copy (exprData_getLiteral (data));
1877       break;
1878
1879     case XPR_NUMLIT:
1880       //      cstring_copy (exprData_getLiteral (data));
1881       break;
1882     case XPR_POSTOP:
1883
1884            ret = constraintList_addListFree (ret,
1885                                     exprNode_traversFalseEnsuresConstraints
1886                                     (exprData_getUopNode (data) ) );
1887            break;
1888
1889     case XPR_CAST:
1890
1891       ret = constraintList_addListFree (ret,
1892                                     exprNode_traversFalseEnsuresConstraints
1893                                     (exprData_getCastNode (data) ) );
1894       break;
1895
1896     default:
1897       break;
1898     }
1899
1900   return ret;
1901 }
1902
1903
1904 /* walk down the tree and get all requires Constraints in each subexpression*/
1905 /*@only@*/ constraintList exprNode_traversRequiresConstraints (exprNode e)
1906 {
1907   exprNode t1;
1908
1909   bool handledExprNode;
1910   //  char * mes;
1911   exprData data;
1912   constraintList ret;
1913
1914    if (exprNode_handleError (e))
1915      {
1916        ret = constraintList_makeNew();
1917        return ret;
1918      }
1919   ret = constraintList_copy (e->requiresConstraints );
1920
1921    handledExprNode = TRUE;
1922
1923   data = e->edata;
1924
1925   switch (e->kind)
1926     {
1927    case XPR_WHILEPRED:
1928       t1 = exprData_getSingle (data);
1929       ret = constraintList_addListFree ( ret, exprNode_traversRequiresConstraints (t1) );
1930       break;
1931
1932     case XPR_FETCH:
1933
1934       ret = constraintList_addListFree (ret,
1935                                     exprNode_traversRequiresConstraints
1936                                     (exprData_getPairA (data) ) );
1937
1938       ret = constraintList_addListFree (ret,
1939                                     exprNode_traversRequiresConstraints
1940                                     (exprData_getPairB (data) ) );
1941       break;
1942     case XPR_PREOP:
1943
1944       ret = constraintList_addListFree (ret,
1945                                     exprNode_traversRequiresConstraints
1946                                     (exprData_getUopNode (data) ) );
1947       break;
1948
1949     case XPR_PARENS:
1950       ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints
1951                                     (exprData_getUopNode (data) ) );
1952       break;
1953     case XPR_INIT:
1954       ret = constraintList_addListFree (ret,
1955                                         exprNode_traversRequiresConstraints
1956                                         (exprData_getInitNode (data) ) );
1957         break;
1958
1959     case XPR_ASSIGN:
1960         ret = constraintList_addListFree (ret,
1961                                     exprNode_traversRequiresConstraints
1962                                     (exprData_getOpA (data) ) );
1963
1964        ret = constraintList_addListFree (ret,
1965                                     exprNode_traversRequiresConstraints
1966                                     (exprData_getOpB (data) ) );
1967        break;
1968     case XPR_OP:
1969        ret = constraintList_addListFree (ret,
1970                                     exprNode_traversRequiresConstraints
1971                                     (exprData_getOpA (data) ) );
1972
1973        ret = constraintList_addListFree (ret,
1974                                     exprNode_traversRequiresConstraints
1975                                     (exprData_getOpB (data) ) );
1976        break;
1977     case XPR_SIZEOFT:
1978
1979       //      ctype_unparse (qtype_getType (exprData_getType (data) ) );
1980
1981       break;
1982
1983     case XPR_SIZEOF:
1984
1985        ret = constraintList_addListFree (ret,
1986                                     exprNode_traversRequiresConstraints
1987                                      (exprData_getSingle (data) ) );
1988        break;
1989
1990     case XPR_CALL:
1991       ret = constraintList_addListFree (ret,
1992                                      exprNode_traversRequiresConstraints
1993                                     (exprData_getFcn (data) ) );
1994       /*@i11*/      //   exprNodeList_unparse (exprData_getArgs (data) );
1995          break;
1996
1997     case XPR_RETURN:
1998       ret = constraintList_addListFree (ret,
1999                                     exprNode_traversRequiresConstraints
2000                                     (exprData_getSingle (data) ) );
2001       break;
2002
2003     case XPR_NULLRETURN:
2004       //      cstring_makeLiteral ("return");;
2005       break;
2006
2007     case XPR_FACCESS:
2008           ret = constraintList_addListFree (ret,
2009                                     exprNode_traversRequiresConstraints
2010                                     (exprData_getFieldNode (data) ) );
2011        //exprData_getFieldName (data) ;
2012       break;
2013
2014     case XPR_ARROW:
2015         ret = constraintList_addListFree (ret,
2016                                     exprNode_traversRequiresConstraints
2017                                     (exprData_getFieldNode (data) ) );
2018         //      exprData_getFieldName (data);
2019       break;
2020
2021     case XPR_STRINGLITERAL:
2022       //      cstring_copy (exprData_getLiteral (data));
2023       break;
2024
2025     case XPR_NUMLIT:
2026       //      cstring_copy (exprData_getLiteral (data));
2027       break;
2028     case XPR_POSTOP:
2029
2030            ret = constraintList_addListFree (ret,
2031                                     exprNode_traversRequiresConstraints
2032                                     (exprData_getUopNode (data) ) );
2033            break;
2034
2035     case XPR_CAST:
2036
2037       ret = constraintList_addListFree (ret,
2038                                     exprNode_traversRequiresConstraints
2039                                     (exprData_getCastNode (data) ) );
2040       break;
2041
2042     default:
2043       break;
2044     }
2045
2046   return ret;
2047 }
2048
2049
2050 /* walk down the tree and get all Ensures Constraints in each subexpression*/
2051 /*@only@*/ constraintList exprNode_traversEnsuresConstraints (exprNode e)
2052 {
2053   exprNode t1;
2054
2055   bool handledExprNode;
2056   //  char * mes;
2057   exprData data;
2058   //  constraintExpr tmp;
2059   //  constraint cons;
2060   constraintList ret;
2061
2062
2063    if (exprNode_handleError (e))
2064      {
2065        ret = constraintList_makeNew();
2066        return ret;
2067      }
2068
2069   ret = constraintList_copy (e->ensuresConstraints );
2070    handledExprNode = TRUE;
2071
2072   data = e->edata;
2073
2074   DPRINTF( (message (
2075                      "exprnode_traversEnsuresConstraints call for %s with constraintList of %s",
2076                      exprNode_unparse (e),
2077                      constraintList_print(e->ensuresConstraints)
2078                      )
2079             ));
2080
2081
2082   switch (e->kind)
2083     {
2084    case XPR_WHILEPRED:
2085       t1 = exprData_getSingle (data);
2086       ret = constraintList_addListFree ( ret,exprNode_traversEnsuresConstraints (t1) );
2087       break;
2088
2089     case XPR_FETCH:
2090
2091       ret = constraintList_addListFree (ret,
2092                                     exprNode_traversEnsuresConstraints
2093                                     (exprData_getPairA (data) ) );
2094
2095       ret = constraintList_addListFree (ret,
2096                                     exprNode_traversEnsuresConstraints
2097                                     (exprData_getPairB (data) ) );
2098       break;
2099     case XPR_PREOP:
2100
2101       ret = constraintList_addListFree (ret,
2102                                     exprNode_traversEnsuresConstraints
2103                                     (exprData_getUopNode (data) ) );
2104       break;
2105
2106     case XPR_PARENS:
2107       ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints
2108                                     (exprData_getUopNode (data) ) );
2109       break;
2110
2111     case XPR_INIT:
2112       ret = constraintList_addListFree (ret,
2113                                         exprNode_traversEnsuresConstraints
2114                                         (exprData_getInitNode (data) ) );
2115         break;
2116
2117
2118     case XPR_ASSIGN:
2119         ret = constraintList_addListFree (ret,
2120                                     exprNode_traversEnsuresConstraints
2121                                     (exprData_getOpA (data) ) );
2122
2123        ret = constraintList_addListFree (ret,
2124                                     exprNode_traversEnsuresConstraints
2125                                     (exprData_getOpB (data) ) );
2126        break;
2127     case XPR_OP:
2128        ret = constraintList_addListFree (ret,
2129                                     exprNode_traversEnsuresConstraints
2130                                     (exprData_getOpA (data) ) );
2131
2132        ret = constraintList_addListFree (ret,
2133                                     exprNode_traversEnsuresConstraints
2134                                     (exprData_getOpB (data) ) );
2135        break;
2136     case XPR_SIZEOFT:
2137
2138       //      ctype_unparse (qtype_getType (exprData_getType (data) ) );
2139
2140       break;
2141
2142     case XPR_SIZEOF:
2143
2144        ret = constraintList_addListFree (ret,
2145                                     exprNode_traversEnsuresConstraints
2146                                      (exprData_getSingle (data) ) );
2147        break;
2148
2149     case XPR_CALL:
2150       ret = constraintList_addListFree (ret,
2151                                      exprNode_traversEnsuresConstraints
2152                                     (exprData_getFcn (data) ) );
2153       /*@i11*/      //   exprNodeList_unparse (exprData_getArgs (data) );
2154          break;
2155
2156     case XPR_RETURN:
2157       ret = constraintList_addListFree (ret,
2158                                     exprNode_traversEnsuresConstraints
2159                                     (exprData_getSingle (data) ) );
2160       break;
2161
2162     case XPR_NULLRETURN:
2163       //      cstring_makeLiteral ("return");;
2164       break;
2165
2166     case XPR_FACCESS:
2167           ret = constraintList_addListFree (ret,
2168                                     exprNode_traversEnsuresConstraints
2169                                     (exprData_getFieldNode (data) ) );
2170        //exprData_getFieldName (data) ;
2171       break;
2172
2173     case XPR_ARROW:
2174         ret = constraintList_addListFree (ret,
2175                                     exprNode_traversEnsuresConstraints
2176                                     (exprData_getFieldNode (data) ) );
2177         //      exprData_getFieldName (data);
2178       break;
2179
2180     case XPR_STRINGLITERAL:
2181       //      cstring_copy (exprData_getLiteral (data));
2182       break;
2183
2184     case XPR_NUMLIT:
2185       //      cstring_copy (exprData_getLiteral (data));
2186       break;
2187     case XPR_POSTOP:
2188
2189            ret = constraintList_addListFree (ret,
2190                                     exprNode_traversEnsuresConstraints
2191                                     (exprData_getUopNode (data) ) );
2192            break;
2193     case XPR_CAST:
2194
2195       ret = constraintList_addListFree (ret,
2196                                     exprNode_traversEnsuresConstraints
2197                                     (exprData_getCastNode (data) ) );
2198       break;
2199
2200     default:
2201       break;
2202     }
2203 DPRINTF( (message (
2204                      "exprnode_traversEnsuresConstraints call for %s with constraintList of  is returning %s",
2205                      exprNode_unparse (e),
2206              //              constraintList_print(e->ensuresConstraints),
2207                      constraintList_print(ret)
2208                      )
2209             ));
2210
2211
2212   return ret;
2213 }
2214
2215 /*drl moved out of constraintResolve.c 07-02-001 */
2216 void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist, fileloc sequencePoint)
2217 {
2218   temp->requiresConstraints = constraintList_makeNew();
2219   temp->ensuresConstraints = constraintList_makeNew();
2220   temp->trueEnsuresConstraints = constraintList_makeNew();
2221   temp->falseEnsuresConstraints = constraintList_makeNew();
2222
2223   exprNodeList_elements (arglist, el)
2224     {
2225       constraintList temp2;
2226       exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint);
2227       temp2 = el->requiresConstraints;
2228       el->requiresConstraints = exprNode_traversRequiresConstraints(el);
2229       constraintList_free(temp2);
2230
2231       temp2 = el->ensuresConstraints;
2232       el->ensuresConstraints  = exprNode_traversEnsuresConstraints(el);
2233       constraintList_free(temp2);
2234
2235       temp->requiresConstraints = constraintList_addList(temp->requiresConstraints,
2236                                                             el->requiresConstraints);
2237
2238       temp->ensuresConstraints = constraintList_addList(temp->ensuresConstraints,
2239                                                            el->ensuresConstraints);
2240     }
2241   end_exprNodeList_elements;
2242
2243 }
2244
2245 /*drl moved out of constraintResolve.c 07-03-001 */
2246 constraintList exprNode_getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall)
2247 {
2248   constraintList postconditions;
2249   uentry temp;
2250   DPRINTF( (message ("Got call that %s ( %s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (arglist ) ) ) );
2251
2252   temp = exprNode_getUentry (fcn);
2253
2254   postconditions = uentry_getFcnPostconditions (temp);
2255
2256   if (constraintList_isDefined (postconditions))
2257     {
2258       postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist);
2259       postconditions = constraintList_doFixResult (postconditions, fcnCall);
2260     }
2261   else
2262     {
2263       postconditions = constraintList_makeNew();
2264     }
2265
2266   return postconditions;
2267 }
2268
2269
2270 /*drl moved out of constraintResolve.c 07-02-001 */
2271 constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist)
2272 {
2273   constraintList preconditions;
2274   uentry temp;
2275   DPRINTF( (message ("Got call that %s ( %s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (arglist ) ) ) );
2276
2277   temp = exprNode_getUentry (fcn);
2278
2279   preconditions = uentry_getFcnPreconditions (temp);
2280
2281   if (constraintList_isDefined(preconditions) )
2282     {
2283       preconditions = constraintList_togglePost (preconditions);
2284       preconditions = constraintList_preserveCallInfo(preconditions, fcn);
2285       preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist);
2286     }
2287   else
2288     {
2289       if (constraintList_isUndefined(preconditions) )
2290         preconditions = constraintList_makeNew();
2291     }
2292   DPRINTF (( message("Done checkCall\n") ));
2293   DPRINTF (( message("Returning list %q ", constraintList_printDetailed(preconditions) ) ));
2294   return preconditions;
2295 }