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