src/constraintGeneration.c

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