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