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