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_traversTrueEnsuresConstraints (/*@temp@*/ exprNode p_e);
  52 static constraintList exprNode_traversFalseEnsuresConstraints (/*@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 Analysising %s at %s", exprNode_unparse(e),
 121                     fileloc_unparse(exprNode_getfileloc(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", constraintList_unparseDetailed (e->requiresConstraints))));
 150   return FALSE;
 151 }
 152
 153 static void exprNode_stmt (/*@temp@*/ exprNode e)
 154 {
 155   exprNode snode;
 156   fileloc loc;
 157   cstring s;
 158
 159   if (exprNode_isError(e))
 160     {
 161       return;
 162     }
 163
 164   /*e->requiresConstraints = constraintList_makeNew();
 165     e->ensuresConstraints  = constraintList_makeNew(); */
 166
 167   DPRINTF(("expNode_stmt: STMT:"));
 168   s =  exprNode_unparse(e);
 169   DPRINTF ((message("exprNode_stmt: STMT: %s ", s)));
 170
 171   if (e->kind == XPR_INIT)
 172     {
 173       constraintList tempList;
 174       DPRINTF (("Init"));
 175       DPRINTF ((message ("%s ", exprNode_unparse (e))));
 176       loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
 177       exprNode_exprTraverse (e, FALSE, FALSE, loc);
 178       fileloc_free(loc);
 179
 180       tempList = e->requiresConstraints;
 181       e->requiresConstraints = exprNode_traversRequiresConstraints(e);
 182       constraintList_free(tempList);
 183
 184       tempList = e->ensuresConstraints;
 185       e->ensuresConstraints  = exprNode_traversEnsuresConstraints(e);
 186       constraintList_free(tempList);
 187       return;
 188     }
 189
 190   /*drl 2/13/002 patched bug so return statement will be checked*/
 191   /*return is a stmt not not expression ...*/
 192   if (e->kind == XPR_RETURN)
 193     {
 194       constraintList tempList;
 195
 196       loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
 197
 198       exprNode_exprTraverse (exprData_getSingle (e->edata), FALSE, TRUE, loc);
 199       fileloc_free(loc);
 200
 201       tempList = e->requiresConstraints;
 202       e->requiresConstraints = exprNode_traversRequiresConstraints(e);
 203       constraintList_free(tempList);
 204     }
 205
 206   if (e->kind != XPR_STMT)
 207     {
 208
 209       DPRINTF (("Not Stmt"));
 210       DPRINTF ((message ("%s ", exprNode_unparse (e))));
 211
 212       if (exprNode_isMultiStatement (e))
 213         {
 214           exprNode_multiStatement (e); /* evans 2001-08-21: spurious return removed */
 215         }
 216       else
 217         {
 218           loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
 219
 220           exprNode_exprTraverse (e, FALSE, TRUE, loc);
 221           fileloc_free(loc);
 222
 223           }
 224           return;
 225     }
 226
 227   DPRINTF (("Stmt"));
 228   DPRINTF ((message ("%s ", exprNode_unparse (e))));
 229
 230   snode = exprData_getUopNode (e->edata);
 231
 232   /* could be stmt involving multiple statements:
 233      i.e. if, while for ect.
 234   */
 235
 236   if (exprNode_isMultiStatement (snode))
 237     {
 238       exprNode_multiStatement (snode);
 239       (void) exprNode_copyConstraints (e, snode);
 240       return;
 241     }
 242
 243   loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
 244   exprNode_exprTraverse (snode, FALSE, FALSE, loc);
 245
 246   fileloc_free(loc);
 247
 248   constraintList_free (e->requiresConstraints);
 249   e->requiresConstraints = exprNode_traversRequiresConstraints(snode);
 250
 251   constraintList_free (e->ensuresConstraints);
 252   e->ensuresConstraints  = exprNode_traversEnsuresConstraints(snode);
 253
 254   DPRINTF ((message ("smtlist constraints are: pre: %s \n and \t post %s\n",
 255                       constraintList_unparse(e->requiresConstraints),
 256                       constraintList_unparse(e->ensuresConstraints))));
 257
 258   return;
 259 }
 260
 261 static void exprNode_stmtList  (/*@dependent@*/ exprNode e)
 262 {
 263   exprNode stmt1, stmt2;
 264   if (exprNode_isError (e))
 265     {
 266       return;
 267     }
 268
 269   /*
 270     Handle case of stmtList with only one statement:
 271     The parse tree stores this as stmt instead of stmtList
 272   */
 273
 274   if (e->kind != XPR_STMTLIST)
 275     {
 276       exprNode_stmt(e);
 277       return;
 278     }
 279   llassert (e->kind == XPR_STMTLIST);
 280   DPRINTF(("exprNode_stmtList STMTLIST:"));
 281   DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e))));
 282   stmt1 = exprData_getPairA (e->edata);
 283   stmt2 = exprData_getPairB (e->edata);
 284
 285
 286   DPRINTF(("exprNode_stmtlist       "));
 287   DPRINTF ((message("XW%s    |        %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2))));
 288
 289   exprNode_stmt (stmt1);
 290   DPRINTF(("\nstmt after stmtList call "));
 291
 292   exprNode_stmt (stmt2);
 293   exprNode_mergeResolve (e, stmt1, stmt2);
 294
 295   DPRINTF ((message ("smtlist constraints are: pre: %s \n and \t post %s\n",
 296                       constraintList_unparse(e->requiresConstraints),
 297                       constraintList_unparse(e->ensuresConstraints))));
 298   return;
 299 }
 300
 301 static exprNode doIf (/*@returned@*/  exprNode e, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body)
 302 {
 303   constraintList temp;
 304
 305   DPRINTF ((message ("doIf: %s ", exprNode_unparse(e))));
 306
 307   llassert(exprNode_isDefined(test));
 308   llassert (exprNode_isDefined (e));
 309   llassert (exprNode_isDefined (body));
 310
 311
 312       DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->ensuresConstraints))));
 313
 314       DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->ensuresConstraints))));
 315
 316       DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->trueEnsuresConstraints))));
 317
 318       DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->falseEnsuresConstraints))));
 319
 320
 321
 322       DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(test), constraintList_unparseDetailed(test->ensuresConstraints))));
 323
 324       DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(test), constraintList_unparseDetailed(test->ensuresConstraints))));
 325
 326       DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_unparseDetailed(test->trueEnsuresConstraints))));
 327
 328       DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_unparseDetailed(test->falseEnsuresConstraints))));
 329
 330
 331
 332       temp = test->trueEnsuresConstraints;
 333       test->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(test);
 334       constraintList_free(temp);
 335
 336   temp = test->ensuresConstraints;
 337   test->ensuresConstraints = exprNode_traversEnsuresConstraints (test);
 338   constraintList_free(temp);
 339
 340   temp = test->requiresConstraints;
 341   test->requiresConstraints = exprNode_traversRequiresConstraints (test);
 342   constraintList_free(temp);
 343
 344
 345   test->trueEnsuresConstraints = constraintList_substituteFreeTarget(test->trueEnsuresConstraints, test->ensuresConstraints);
 346
 347   DPRINTF ((message ("doIf: test ensures %s ", constraintList_unparse(test->ensuresConstraints))));
 348
 349   DPRINTF ((message ("doIf: test true ensures %s ", constraintList_unparse(test->trueEnsuresConstraints))));
 350
 351   constraintList_free(e->requiresConstraints);
 352
 353
 354   e->requiresConstraints = constraintList_reflectChanges(body->requiresConstraints, test->trueEnsuresConstraints);
 355
 356   e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints,
 357                                            test->ensuresConstraints);
 358   temp = e->requiresConstraints;
 359   e->requiresConstraints = constraintList_mergeRequires (e->requiresConstraints, test->requiresConstraints);
 360   constraintList_free(temp);
 361
 362
 363   /* drl possible problem : warning bad */
 364   constraintList_free(e->ensuresConstraints);
 365   e->ensuresConstraints = constraintList_copy (test->ensuresConstraints);
 366
 367   if (exprNode_mayEscape (body))
 368     {
 369       DPRINTF ((message("doIf: the if statement body %s returns or exits", exprNode_unparse(body))));
 370       e->ensuresConstraints = constraintList_mergeEnsuresFreeFirst (e->ensuresConstraints,
 371                                                         test->falseEnsuresConstraints);
 372     }
 373
 374   DPRINTF ((message ("doIf: if requiers %s ", constraintList_unparse(e->requiresConstraints))));
 375
 376   return e;
 377 }
 378
 379 /*drl added 3/4/2001
 380   Also used for condition i.e. ?: operation
 381
 382   Precondition
 383   This function assumes that p, trueBranch, falseBranch have have all been traversed
 384   for constraints i.e. we assume that exprNode_traversEnsuresConstraints,
 385   exprNode_traversRequiresConstraints,  exprNode_traversTrueEnsuresConstraints,
 386   exprNode_traversFalseEnsuresConstraints have all been run
 387 */
 388
 389 static exprNode doIfElse (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode p, /*@dependent@*/ exprNode trueBranch, /*@dependent@*/ exprNode falseBranch)
 390 {
 391   constraintList c1, cons, t, t2, f, f2;
 392
 393   llassert (exprNode_isDefined (e));
 394   llassert (exprNode_isDefined (p));
 395   llassert (exprNode_isDefined (trueBranch));
 396   llassert (exprNode_isDefined (falseBranch));
 397   DPRINTF ((message ("doIfElse: %s ", exprNode_unparse(e))));
 398
 399   /* do requires clauses */
 400   c1 = constraintList_copy (p->ensuresConstraints);
 401
 402   t = constraintList_reflectChanges(trueBranch->requiresConstraints, p->trueEnsuresConstraints);
 403   t = constraintList_reflectChangesFreePre (t, p->ensuresConstraints);
 404
 405   cons = constraintList_reflectChanges(falseBranch->requiresConstraints, p->falseEnsuresConstraints);
 406   cons  = constraintList_reflectChangesFreePre (cons, c1);
 407
 408   constraintList_free (e->requiresConstraints);
 409   e->requiresConstraints = constraintList_mergeRequiresFreeFirst (t, cons);
 410   e->requiresConstraints = constraintList_mergeRequiresFreeFirst (e->requiresConstraints, p->requiresConstraints);
 411
 412   /* do ensures clauses
 413      find the  the ensures lists for each subbranch
 414   */
 415
 416   t = constraintList_mergeEnsures (p->trueEnsuresConstraints, trueBranch->ensuresConstraints);
 417   t2 = t;
 418   t = constraintList_mergeEnsures (p->ensuresConstraints, t);
 419   constraintList_free(t2);
 420
 421   f = constraintList_mergeEnsures (p->falseEnsuresConstraints, falseBranch->ensuresConstraints);
 422   f2 = f;
 423   f = constraintList_mergeEnsures (p->ensuresConstraints, f);
 424   constraintList_free(f2);
 425
 426   /* find ensures for whole if/else statement */
 427
 428   constraintList_free(e->ensuresConstraints);
 429
 430   e->ensuresConstraints = constraintList_logicalOr (t, f);
 431
 432   constraintList_free(t);
 433   constraintList_free(f);
 434   constraintList_free(cons);
 435   constraintList_free(c1);
 436
 437   DPRINTF ((message ("doIfElse: if requires %q ", constraintList_unparse(e->requiresConstraints))));
 438   DPRINTF ((message ("doIfElse: if ensures %q ", constraintList_unparse(e->ensuresConstraints))));
 439
 440   return e;
 441 }
 442
 443 static exprNode doWhile (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body)
 444 {
 445   DPRINTF ((message ("doWhile: %s ", exprNode_unparse(e))));
 446   return doIf (e, test, body);
 447 }
 448
 449 /*@only@*/ constraintList constraintList_makeFixedArrayConstraints (/*@observer@*/ sRefSet s)
 450 {
 451   constraintList ret;
 452   constraint con;
 453   ret = constraintList_makeNew();
 454
 455   sRefSet_elements (s, el)
 456     {
 457       if (sRef_isFixedArray(el))
 458         {
 459           size_t size;
 460           DPRINTF((message("%s is a fixed array",
 461                             sRef_unparse(el))));
 462           size = sRef_getArraySize(el);
 463           DPRINTF((message("%s is a fixed array with size %d",
 464                             sRef_unparse(el), (int)size)));
 465           con = constraint_makeSRefSetBufferSize (el, size_toLong (size - 1));
 466           ret = constraintList_add(ret, con);
 467         }
 468       else
 469         {
 470           DPRINTF((message("%s is not a fixed array",
 471                             sRef_unparse(el))));
 472
 473
 474           if (sRef_isExternallyVisible (el))
 475             {
 476               /*
 477                 DPRINTF((message("%s is externally visible",
 478                 sRef_unparse(el))));
 479                 con = constraint_makeSRefWriteSafeInt(el, 0);
 480                 ret = constraintList_add(ret, con);
 481
 482                 con = constraint_makeSRefReadSafeInt(el, 0);
 483
 484                 ret = constraintList_add(ret, con);
 485               */
 486             }
 487         }
 488     }
 489   end_sRefSet_elements ;
 490
 491   DPRINTF((message("constraintList_makeFixedArrayConstraints returning %s",
 492                     constraintList_unparse(ret))));
 493   return ret;
 494 }
 495
 496 # if 0
 497 exprNode makeDataTypeConstraints (/*@returned@*/ exprNode e)
 498 {
 499   constraintList c;
 500   DPRINTF(("makeDataTypeConstraints"));
 501
 502   c = constraintList_makeFixedArrayConstraints (e->uses);
 503
 504   e->ensuresConstraints = constraintList_addListFree (e->ensuresConstraints, c);
 505
 506  return e;
 507 }
 508 # endif
 509
 510 static void doFor (/*@dependent@*/ exprNode e, /*@dependent@*/ exprNode forPred, /*@dependent@*/ exprNode forBody)
 511 {
 512   exprNode init, test, inc;
 513   /* merge the constraints: modle as if statement */
 514
 515   /* init
 516      if (test)
 517      for body
 518      inc        */
 519
 520   llassert (exprNode_isDefined (e));
 521   llassert (exprNode_isDefined (forPred));
 522   llassert (exprNode_isDefined (forBody));
 523
 524   init = exprData_getTripleInit (forPred->edata);
 525   test = exprData_getTripleTest (forPred->edata);
 526   inc = exprData_getTripleInc (forPred->edata);
 527
 528   if (((exprNode_isError (test) /*|| (exprNode_isError(init))*/) || (exprNode_isError (inc))))
 529     {
 530       DPRINTF ((message ("strange for statement:%s, ignoring it", exprNode_unparse(e))));
 531       return;
 532     }
 533
 534   exprNode_forLoopHeuristics(e, forPred, forBody);
 535
 536   constraintList_free(e->requiresConstraints);
 537   e->requiresConstraints = constraintList_reflectChanges(forBody->requiresConstraints, test->ensuresConstraints);
 538   e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, test->trueEnsuresConstraints);
 539   e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, forPred->ensuresConstraints);
 540
 541   if (!forBody->canBreak)
 542     {
 543       e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints, constraintList_copy(forPred->ensuresConstraints));
 544       e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints,constraintList_copy(test->falseEnsuresConstraints));
 545     }
 546   else
 547     {
 548       DPRINTF(("Can break"));
 549     }
 550 }
 551
 552 static /*@dependent@*/ exprNode exprNode_makeDependent(/*@returned@*/  exprNode e)
 553 {
 554   /* !!! DRL - this is ridiculous!  Read the manual on memory annotations please! */
 555   return e;
 556 }
 557
 558 static void
 559 exprNode_doGenerateConstraintSwitch
 560   (/*@dependent@*/ exprNode switchExpr,
 561    /*@dependent@*/ exprNode body,
 562    /*@special@*/ constraintList *currentRequires,
 563    /*@special@*/ constraintList *currentEnsures,
 564    /*@special@*/ constraintList *savedRequires,
 565    /*@special@*/ constraintList *savedEnsures)
 566   /*@post:only *currentRequires, *currentEnsures, *savedRequires, *savedEnsures @*/
 567   /*@sets *currentRequires,  *currentEnsures,  *savedRequires, *savedEnsures @*/
 568 {
 569   exprNode stmt, stmtList;
 570
 571   DPRINTF((message("exprNode_doGenerateConstraintSwitch: (switch %s) %s",
 572                     exprNode_unparse(switchExpr), exprNode_unparse(body)
 573                    )));
 574
 575   if (exprNode_isError(body))
 576     {
 577       *currentRequires = constraintList_makeNew ();
 578       *currentEnsures = constraintList_makeNew ();
 579
 580       *savedRequires = constraintList_makeNew ();
 581       *savedEnsures = constraintList_makeNew ();
 582       /*@-onlytrans@*/
 583       return;
 584       /*@=onlytrans@*/
 585     }
 586
 587   if (body->kind != XPR_STMTLIST)
 588     {
 589       DPRINTF((message("exprNode_doGenerateConstraintSwitch: non stmtlist: %s",
 590                        exprNode_unparse(body))));
 591       stmt = body;
 592       stmtList = exprNode_undefined;
 593       stmt = exprNode_makeDependent(stmt);
 594       stmtList = exprNode_makeDependent(stmtList);
 595     }
 596   else
 597     {
 598       stmt     = exprData_getPairB(body->edata);
 599       stmtList = exprData_getPairA(body->edata);
 600       stmt = exprNode_makeDependent(stmt);
 601       stmtList = exprNode_makeDependent(stmtList);
 602     }
 603
 604   DPRINTF((message("exprNode_doGenerateConstraintSwitch: stmtlist: %s stmt: %s",
 605                    exprNode_unparse(stmtList), exprNode_unparse(stmt))
 606           ));
 607
 608
 609   exprNode_doGenerateConstraintSwitch (switchExpr, stmtList, currentRequires, currentEnsures,
 610                                        savedRequires, savedEnsures);
 611
 612   if (exprNode_isError(stmt))
 613     /*@-onlytrans@*/
 614     return;
 615     /*@=onlytrans@*/
 616
 617   exprNode_stmt(stmt);
 618
 619   switchExpr = exprNode_makeDependent (switchExpr);
 620
 621   if (! exprNode_isCaseMarker(stmt))
 622     {
 623
 624       constraintList temp;
 625
 626       DPRINTF ((message("Got normal statement %s (requires %s ensures %s)", exprNode_unparse(stmt),
 627                          constraintList_unparse(stmt->requiresConstraints), constraintList_unparse(stmt->ensuresConstraints))));
 628
 629       temp = constraintList_reflectChanges (stmt->requiresConstraints,
 630                                             *currentEnsures);
 631
 632             *currentRequires = constraintList_mergeRequiresFreeFirst(
 633                                                                      *currentRequires,
 634                                                                      temp);
 635
 636             constraintList_free(temp);
 637
 638                   *currentEnsures = constraintList_mergeEnsuresFreeFirst
 639                     (*currentEnsures,
 640                      stmt->ensuresConstraints);
 641                   DPRINTF((message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
 642                                     "%s currentEnsures:%s",
 643                                     exprNode_unparse(switchExpr), exprNode_unparse(body),
 644                                     constraintList_unparse(*currentRequires), constraintList_unparse(*currentEnsures)
 645                                    )));
 646                   /*@-onlytrans@*/
 647                   return;
 648                   /*@=onlytrans@*/
 649
 650     }
 651
 652   if (exprNode_isCaseMarker(stmt) && exprNode_mustEscape(stmtList))
 653     {
 654       /*
 655       ** merge current and saved constraint with Logical Or...
 656       ** make a constraint for ensures
 657       */
 658
 659       constraintList temp;
 660       constraint con;
 661
 662       DPRINTF ((message("Got case marker")));
 663
 664       if (constraintList_isUndefined(*savedEnsures) &&
 665           constraintList_isUndefined(*savedRequires))
 666         {
 667           llassert(constraintList_isUndefined(*savedEnsures));
 668           llassert(constraintList_isUndefined(*savedRequires));
 669           *savedEnsures  = constraintList_copy(*currentEnsures);
 670           *savedRequires = constraintList_copy(*currentRequires);
 671         }
 672       else
 673         {
 674           DPRINTF ((message("Doing logical or")));
 675           temp = constraintList_logicalOr (*savedEnsures, *currentEnsures);
 676           constraintList_free (*savedEnsures);
 677           *savedEnsures = temp;
 678
 679           *savedRequires = constraintList_mergeRequiresFreeFirst (*savedRequires, *currentRequires);
 680         }
 681
 682       con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle (stmt->edata), exprNode_loc (stmt));
 683
 684       constraintList_free (*currentEnsures);
 685       *currentEnsures = constraintList_makeNew();
 686       *currentEnsures = constraintList_add(*currentEnsures, con);
 687
 688       constraintList_free(*currentRequires);
 689       *currentRequires = constraintList_makeNew();
 690       DPRINTF (("exprNode_doGenerateConstraintSwitch: (switch %s) %s savedRequires:"
 691                 "%s savedEnsures:%s",
 692                 exprNode_unparse(switchExpr), exprNode_unparse(body),
 693                 constraintList_unparse(*savedRequires), constraintList_unparse(*savedEnsures)
 694                 ));
 695     }
 696   else if (exprNode_isCaseMarker(stmt)) /* prior case has no break. */
 697     {
 698       /*
 699          We don't do anything to the sved constraints because the case hasn't ended
 700          The new ensures constraints for the case will be:
 701          the constraint for the case statement (CASE_LABEL == SWITCH_EXPR) logicalOr currentEnsures
 702       */
 703
 704       constraintList temp;
 705       constraint con;
 706       constraintList ensuresTemp;
 707
 708       con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle (stmt->edata), exprNode_loc (stmt));
 709
 710       ensuresTemp = constraintList_makeNew ();
 711       ensuresTemp = constraintList_add (ensuresTemp, con);
 712
 713       if (exprNode_isError (stmtList))
 714         {
 715           constraintList_free (*currentEnsures);
 716           *currentEnsures = constraintList_copy (ensuresTemp);
 717           constraintList_free (ensuresTemp);
 718         }
 719       else
 720         {
 721           temp = constraintList_logicalOr (*currentEnsures, ensuresTemp);
 722           constraintList_free (*currentEnsures);
 723           constraintList_free (ensuresTemp);
 724           *currentEnsures = temp;
 725         }
 726
 727       constraintList_free (*currentRequires);
 728       *currentRequires = constraintList_makeNew();
 729     }
 730   else
 731     {
 732       /*
 733         we handle the case of ! exprNode_isCaseMarker above
 734         the else if clause should always be true.
 735       */
 736       BADEXIT;
 737     }
 738
 739   DPRINTF (("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
 740             "%s currentEnsures:%s",
 741             exprNode_unparse(switchExpr), exprNode_unparse(body),
 742             constraintList_unparse(*currentRequires), constraintList_unparse(*currentEnsures)
 743             ));
 744
 745   /*@-onlytrans@*/
 746   return;
 747   /*@=onlytrans@*/
 748 }
 749
 750
 751 static void exprNode_generateConstraintSwitch (/*@notnull@*/ exprNode switchStmt)
 752 {
 753   constraintList constraintsRequires;
 754   constraintList constraintsEnsures;
 755   constraintList lastRequires;
 756   constraintList lastEnsures;
 757
 758   exprNode body;
 759   exprNode switchExpr;
 760
 761   switchExpr = exprData_getPairA (switchStmt->edata);
 762   body = exprData_getPairB (switchStmt->edata);
 763
 764   if (!exprNode_isDefined (body))
 765     {
 766       return;
 767     }
 768
 769   DPRINTF((message("")));
 770
 771   if (body->kind == XPR_BLOCK)
 772     body = exprData_getSingle(body->edata);
 773
 774
 775   constraintsRequires = constraintList_undefined;
 776   constraintsEnsures = constraintList_undefined;
 777
 778   lastRequires = constraintList_makeNew();
 779   lastEnsures = constraintList_makeNew();
 780
 781
 782   /*@-mustfree@*/
 783   /* evans 2002-01-01: spurious warnings for these becuase of stack allocated storage */
 784   exprNode_doGenerateConstraintSwitch (switchExpr, body, &lastRequires,
 785                                        &lastEnsures, &constraintsRequires, &constraintsEnsures);
 786   /*@=mustfree@*/
 787
 788   /*
 789     merge current and saved constraint with Logical Or...
 790     make a constraint for ensures
 791   */
 792
 793   constraintList_free(switchStmt->requiresConstraints);
 794   constraintList_free(switchStmt->ensuresConstraints);
 795
 796   if (constraintList_isDefined(constraintsEnsures) && constraintList_isDefined(constraintsRequires))
 797     {
 798       switchStmt->ensuresConstraints = constraintList_logicalOr(constraintsEnsures, lastEnsures);
 799       switchStmt->requiresConstraints =   constraintList_mergeRequires(constraintsRequires, lastRequires);
 800       constraintList_free (constraintsRequires);
 801       constraintList_free (constraintsEnsures);
 802     }
 803   else
 804     {
 805       switchStmt->ensuresConstraints =    constraintList_copy(lastEnsures);
 806       switchStmt->requiresConstraints =   constraintList_copy(lastRequires);
 807     }
 808
 809   constraintList_free (lastRequires);
 810   constraintList_free (lastEnsures);
 811
 812   DPRINTF(((message(" exprNode_generateConstraintSwitch returning requires: %s and ensures %s",
 813                      constraintList_unparse(switchStmt->requiresConstraints),
 814                      constraintList_unparse(switchStmt->ensuresConstraints)
 815                     )
 816             )));
 817 }
 818
 819 static exprNode doSwitch (/*@returned@*/ /*@notnull@*/ exprNode e)
 820 {
 821   exprNode body;
 822   exprData data;
 823
 824   data = e->edata;
 825   DPRINTF ((message ("doSwitch for: switch (%s) %s",
 826                       exprNode_unparse (exprData_getPairA (data)),
 827                       exprNode_unparse (exprData_getPairB (data)))));
 828
 829   body = exprData_getPairB (data);
 830   exprNode_generateConstraintSwitch (e);
 831   return e;
 832 }
 833
 834 void exprNode_multiStatement (/*@dependent@*/ exprNode e)
 835 {
 836
 837   bool ret;
 838   exprData data;
 839   exprNode e1, e2;
 840   exprNode p, trueBranch, falseBranch;
 841   exprNode forPred, forBody;
 842   exprNode test;
 843
 844   constraintList temp;
 845
 846   DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse(e),
 847                     fileloc_unparse(exprNode_getfileloc(e)))));
 848
 849   if (exprNode_handleError (e))
 850     {
 851       return;
 852     }
 853
 854   data = e->edata;
 855
 856   ret = TRUE;
 857
 858   switch (e->kind)
 859     {
 860
 861     case XPR_FOR:
 862       forPred = exprData_getPairA (data);
 863       forBody = exprData_getPairB (data);
 864
 865       /* First generate the constraints */
 866       exprNode_generateConstraints (forPred);
 867       exprNode_generateConstraints (forBody);
 868
 869
 870       doFor (e, forPred, forBody);
 871
 872       break;
 873
 874     case XPR_FORPRED:
 875       exprNode_generateConstraints (exprData_getTripleInit (data));
 876       test = exprData_getTripleTest (data);
 877       exprNode_exprTraverse (test,FALSE, FALSE, exprNode_loc(e));
 878       exprNode_generateConstraints (exprData_getTripleInc (data));
 879
 880       if (!exprNode_isError(test))
 881         {
 882           constraintList temp2;
 883           temp2 = test->trueEnsuresConstraints;
 884           test->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(test);
 885           constraintList_free(temp2);
 886         }
 887
 888       exprNode_generateConstraints (exprData_getTripleInc (data));
 889       break;
 890
 891     case XPR_WHILE:
 892       e1 = exprData_getPairA (data);
 893       e2 = exprData_getPairB (data);
 894
 895        exprNode_exprTraverse (e1,
 896                               FALSE, FALSE, exprNode_loc(e1));
 897
 898        exprNode_generateConstraints (e2);
 899
 900        e = doWhile (e, e1, e2);
 901
 902       break;
 903
 904     case XPR_IF:
 905       DPRINTF(("IF:"));
 906       DPRINTF ((exprNode_unparse(e)));
 907       e1 = exprData_getPairA (data);
 908       e2 = exprData_getPairB (data);
 909
 910       exprNode_exprTraverse (e1, FALSE, FALSE, exprNode_loc(e1));
 911
 912       exprNode_generateConstraints (e2);
 913       e = doIf (e, e1, e2);
 914       break;
 915
 916     case XPR_IFELSE:
 917       DPRINTF(("Starting IFELSE"));
 918       p = exprData_getTriplePred (data);
 919
 920       trueBranch = exprData_getTripleTrue (data);
 921       falseBranch = exprData_getTripleFalse (data);
 922
 923       exprNode_exprTraverse (p,
 924                              FALSE, FALSE, exprNode_loc(p));
 925       exprNode_generateConstraints (trueBranch);
 926       exprNode_generateConstraints (falseBranch);
 927
 928       llassert (exprNode_isDefined (p));
 929       temp = p->ensuresConstraints;
 930       p->ensuresConstraints = exprNode_traversEnsuresConstraints (p);
 931       constraintList_free(temp);
 932
 933       temp = p->requiresConstraints;
 934       p->requiresConstraints = exprNode_traversRequiresConstraints (p);
 935       constraintList_free(temp);
 936
 937       temp = p->trueEnsuresConstraints;
 938       p->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(p);
 939       constraintList_free(temp);
 940
 941
 942
 943       DPRINTF((message("p->trueEnsuresConstraints before substitue %s", constraintList_unparse(p->trueEnsuresConstraints)  )
 944                ));
 945
 946             /*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*/
 947
 948       p->trueEnsuresConstraints = constraintList_substituteFreeTarget (p->trueEnsuresConstraints,
 949                                                                        p->ensuresConstraints);
 950
 951       DPRINTF(( message ("p->trueEnsuresConstraints after substitue %s", constraintList_unparse(p->trueEnsuresConstraints) )
 952                 ));
 953
 954       temp = p->falseEnsuresConstraints;
 955       p->falseEnsuresConstraints =  exprNode_traversFalseEnsuresConstraints(p);
 956       constraintList_free(temp);
 957
 958       /*See comment on trueEnsures*/
 959       p->falseEnsuresConstraints = constraintList_substituteFreeTarget (p->falseEnsuresConstraints,
 960                                                                        p->ensuresConstraints);
 961
 962       e = doIfElse (e, p, trueBranch, falseBranch);
 963       DPRINTF(("Done IFELSE"));
 964       break;
 965
 966     case XPR_DOWHILE:
 967
 968       e2 = (exprData_getPairB (data));
 969       e1 = (exprData_getPairA (data));
 970
 971       DPRINTF((message ("do { %s } while (%s)", exprNode_unparse(e2), exprNode_unparse(e1))));
 972       exprNode_generateConstraints (e2);
 973       exprNode_generateConstraints (e1);
 974       e = exprNode_copyConstraints (e, e2);
 975       DPRINTF ((message ("e = %s  ", constraintList_unparse(e->requiresConstraints))));
 976
 977       break;
 978
 979     case XPR_BLOCK:
 980       {
 981         exprNode tempExpr;
 982
 983         tempExpr = exprData_getSingle (data);
 984
 985         exprNode_generateConstraints (tempExpr);
 986
 987         if (exprNode_isDefined(tempExpr) )
 988           {
 989             constraintList_free(e->requiresConstraints);
 990             e->requiresConstraints = constraintList_copy (tempExpr->requiresConstraints);
 991             constraintList_free(e->ensuresConstraints);
 992             e->ensuresConstraints = constraintList_copy (tempExpr->ensuresConstraints);
 993           }
 994         else
 995           {
 996             llassert(FALSE);
 997           }
 998       }
 999       break;
1000
1001     case XPR_SWITCH:
1002       e = doSwitch (e);
1003       break;
1004     case XPR_STMT:
1005     case XPR_STMTLIST:
1006       exprNode_stmtList (e);
1007       return ;
1008       /*@notreached@*/
1009       break;
1010     default:
1011       ret=FALSE;
1012     }
1013   return;
1014 }
1015
1016 static bool lltok_isBoolean_Op (lltok tok)
1017 {
1018   /*this should really be a switch statement but
1019     I don't want to violate the abstraction
1020     maybe this should go in lltok.c */
1021
1022   if (lltok_isEqOp (tok))
1023         {
1024           return TRUE;
1025         }
1026       if (lltok_isAndOp (tok))
1027
1028         {
1029
1030           return TRUE;
1031         }
1032    if (lltok_isOrOp (tok))
1033         {
1034           return TRUE;
1035         }
1036
1037    if (lltok_isGt_Op (tok))
1038      {
1039        return TRUE;
1040      }
1041    if (lltok_isLt_Op (tok))
1042      {
1043        return TRUE;
1044      }
1045
1046    if (lltok_isLe_Op (tok))
1047      {
1048        return TRUE;
1049      }
1050
1051    if (lltok_isGe_Op (tok))
1052      {
1053        return TRUE;
1054      }
1055
1056    return FALSE;
1057
1058 }
1059
1060
1061 static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ bool definatelv, /*@unused@*/ bool definaterv,  fileloc sequencePoint)
1062 {
1063   constraint cons;
1064   exprNode t1, t2;
1065   exprData data;
1066   lltok tok;
1067   constraintList tempList, temp;
1068
1069   if (exprNode_isUndefined(e) )
1070     {
1071       llassert (exprNode_isDefined(e) );
1072       return;
1073     }
1074
1075   data = e->edata;
1076
1077   tok = exprData_getOpTok (data);
1078   t1 = exprData_getOpA (data);
1079   t2 = exprData_getOpB (data);
1080
1081   /* drl 3/2/2003 we know this because of the type of expression*/
1082   llassert( exprNode_isDefined(t1) &&   exprNode_isDefined(t2) );
1083
1084
1085   tempList = constraintList_undefined;
1086
1087   /* arithmetic tests */
1088
1089   if (lltok_isEqOp (tok))
1090     {
1091       cons =  constraint_makeEnsureEqual (t1, t2, sequencePoint);
1092       e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1093     }
1094
1095
1096   if (lltok_isLt_Op (tok))
1097     {
1098       cons =  constraint_makeEnsureLessThan (t1, t2, sequencePoint);
1099       e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1100       cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
1101       e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1102     }
1103
1104   if (lltok_isGe_Op (tok))
1105     {
1106       cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
1107       e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1108
1109       cons =  constraint_makeEnsureLessThan (t1, t2, sequencePoint);
1110       e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1111     }
1112
1113   if (lltok_isGt_Op (tok))
1114     {
1115       cons =  constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
1116       e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1117       cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
1118       e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1119     }
1120
1121   if (lltok_isLe_Op (tok))
1122     {
1123       cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
1124       e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1125
1126       cons =  constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
1127       e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1128     }
1129
1130   /* Logical operations */
1131
1132   if (lltok_isAndOp (tok))
1133     {
1134       /* true ensures  */
1135       tempList = constraintList_copy (t1->trueEnsuresConstraints);
1136       tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
1137       e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList);
1138
1139       /* false ensures: fens t1 or tens t1 and fens t2 */
1140       tempList = constraintList_copy (t1->trueEnsuresConstraints);
1141       tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
1142       temp = tempList;
1143       tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints);
1144       constraintList_free (temp);
1145
1146       /* evans - was constraintList_addList - memory leak detected by splint */
1147       e->falseEnsuresConstraints = constraintList_addListFree (e->falseEnsuresConstraints, tempList);
1148     }
1149   else if (lltok_isOrOp (tok))
1150     {
1151       /* false ensures */
1152       tempList = constraintList_copy (t1->falseEnsuresConstraints);
1153       tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
1154       e->falseEnsuresConstraints = constraintList_addListFree(e->falseEnsuresConstraints, tempList);
1155
1156       /* true ensures: tens t1 or fens t1 and tens t2 */
1157       tempList = constraintList_copy (t1->falseEnsuresConstraints);
1158       tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
1159
1160       temp = tempList;
1161       tempList = constraintList_logicalOr (tempList, t1->trueEnsuresConstraints);
1162       constraintList_free(temp);
1163
1164       e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList);
1165       tempList = constraintList_undefined;
1166     }
1167   else
1168     {
1169       DPRINTF((message("%s is not a boolean operation", lltok_unparse(tok))));
1170     }
1171 }
1172
1173 void exprNode_exprTraverse (/*@dependent@*/ exprNode e, bool definatelv, bool definaterv,  /*@observer@*/ /*@temp@*/ fileloc sequencePoint)
1174 {
1175   exprNode t1, t2, fcn;
1176   lltok tok;
1177   bool handledExprNode;
1178   exprData data;
1179   constraint cons;
1180
1181   constraintList temp;
1182
1183   if (exprNode_isError(e))
1184     {
1185       return;
1186     }
1187
1188   DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse(e),
1189                     fileloc_unparse(exprNode_getfileloc(e)))));
1190
1191   /*e->requiresConstraints = constraintList_makeNew();
1192   e->ensuresConstraints = constraintList_makeNew();
1193   e->trueEnsuresConstraints = constraintList_makeNew();;
1194   e->falseEnsuresConstraints = constraintList_makeNew();;
1195   */
1196
1197   if (exprNode_isUnhandled (e))
1198      {
1199        return;
1200      }
1201
1202   handledExprNode = TRUE;
1203
1204   data = e->edata;
1205
1206   switch (e->kind)
1207     {
1208     case XPR_WHILEPRED:
1209       t1 = exprData_getSingle (data);
1210       exprNode_exprTraverse (t1,  definatelv, definaterv, sequencePoint);
1211       e = exprNode_copyConstraints (e, t1);
1212       break;
1213
1214     case XPR_FETCH:
1215
1216       if (definatelv)
1217         {
1218           t1 =  (exprData_getPairA (data));
1219           t2 =  (exprData_getPairB (data));
1220           cons =  constraint_makeWriteSafeExprNode (t1, t2);
1221         }
1222       else
1223         {
1224           t1 =  (exprData_getPairA (data));
1225           t2 =  (exprData_getPairB (data));
1226           cons = constraint_makeReadSafeExprNode (t1, t2);
1227         }
1228
1229       e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
1230       cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint);
1231       e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1232
1233       cons = constraint_makeEnsureLteMaxRead (t2, t1);
1234       e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1235
1236       exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
1237       exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
1238
1239       break;
1240
1241     case XPR_PARENS:
1242       exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint);
1243       break;
1244     case XPR_INIT:
1245       {
1246         /*
1247         idDecl t;
1248
1249         uentry ue;
1250         exprNode lhs;
1251
1252         t = exprData_getInitId (data);
1253         ue = usymtab_lookup (idDecl_observeId (t));
1254         lhs = exprNode_createId (ue);
1255         */
1256         t2 = exprData_getInitNode (data);
1257
1258         /*      DPRINTF(((message("initialization: %s = %s",
1259                            exprNode_unparse(lhs),
1260                            exprNode_unparse(t2)
1261                           )
1262                   )));  */
1263
1264         exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
1265
1266         /* this test is nessecary because some expressions generate a null expression node.  function pointer do that -- drl */
1267         if ((!exprNode_isError (e))  &&  (!exprNode_isError(t2)))
1268           {
1269             cons =  constraint_makeEnsureEqual (e, t2, sequencePoint);
1270             e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1271           }
1272       }
1273
1274       break;
1275     case XPR_ASSIGN:
1276       t1 = exprData_getOpA (data);
1277       t2 = exprData_getOpB (data);
1278       exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint);
1279       exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
1280
1281       /* this test is nessecary because some expressions generate a null expression node.  function pointer do that -- drl */
1282       if ((!exprNode_isError (t1))  &&  (!exprNode_isError(t2)))
1283         {
1284           cons =  constraint_makeEnsureEqual (t1, t2, sequencePoint);
1285           e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1286         }
1287       break;
1288     case XPR_OP:
1289       t1 = exprData_getOpA (data);
1290       t2 = exprData_getOpB (data);
1291       tok = exprData_getOpTok (data);
1292
1293       if (lltok_getTok (tok) == ADD_ASSIGN)
1294         {
1295           exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint);
1296           exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
1297
1298           cons = constraint_makeAddAssign (t1, t2,  sequencePoint);
1299           e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1300         }
1301       else if (lltok_getTok (tok) == SUB_ASSIGN)
1302         {
1303           exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint);
1304           exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
1305
1306           cons = constraint_makeSubtractAssign (t1, t2,  sequencePoint);
1307           e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1308         }
1309       else
1310         {
1311           exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint);
1312           exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint);
1313         }
1314
1315       if (lltok_isBoolean_Op (tok))
1316         exprNode_booleanTraverse (e, definatelv, definaterv, sequencePoint);
1317
1318       break;
1319     case XPR_SIZEOFT:
1320       /*drl 4-11-03 I think this is the same as the next case...*/
1321
1322       break;
1323
1324     case XPR_SIZEOF:
1325       /* drl  7-16-01
1326          C standard says operand to sizeof isn't evaluated unless
1327          its a variable length array.  So we don't generate constraints.
1328       */
1329
1330       break;
1331
1332     case XPR_CALL:
1333       fcn = exprData_getFcn(data);
1334
1335       exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint);
1336       DPRINTF ((message ("Got call that %s (%s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (exprData_getArgs (data)))));
1337
1338       llassert( exprNode_isDefined(fcn) );
1339
1340       fcn->requiresConstraints = constraintList_addListFree (fcn->requiresConstraints,
1341                                                  checkCall (fcn, exprData_getArgs (data) ));
1342
1343       fcn->ensuresConstraints = 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_traversEnsuresConstraints(pred);
1493         constraintList_free(temp);
1494
1495         temp = pred->requiresConstraints;
1496         pred->requiresConstraints = exprNode_traversRequiresConstraints(pred);
1497         constraintList_free(temp);
1498
1499         temp = pred->trueEnsuresConstraints;
1500         pred->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(pred);
1501         constraintList_free(temp);
1502
1503         temp = pred->falseEnsuresConstraints;
1504         pred->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(pred);
1505         constraintList_free(temp);
1506
1507         exprNode_exprTraverse (trueBranch, FALSE, TRUE, sequencePoint);
1508
1509         temp = trueBranch->ensuresConstraints;
1510         trueBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(trueBranch);
1511         constraintList_free(temp);
1512
1513         temp = trueBranch->requiresConstraints;
1514         trueBranch->requiresConstraints = exprNode_traversRequiresConstraints(trueBranch);
1515         constraintList_free(temp);
1516
1517
1518         temp =       trueBranch->trueEnsuresConstraints;
1519         trueBranch->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(trueBranch);
1520         constraintList_free(temp);
1521
1522         temp =       trueBranch->falseEnsuresConstraints;
1523         trueBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(trueBranch);
1524         constraintList_free(temp);
1525
1526         exprNode_exprTraverse (falseBranch, FALSE, TRUE, sequencePoint);
1527
1528         temp = falseBranch->ensuresConstraints;
1529         falseBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(falseBranch);
1530         constraintList_free(temp);
1531
1532
1533         temp = falseBranch->requiresConstraints;
1534         falseBranch->requiresConstraints = exprNode_traversRequiresConstraints(falseBranch);
1535         constraintList_free(temp);
1536
1537         temp = falseBranch->trueEnsuresConstraints;
1538         falseBranch->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(falseBranch);
1539         constraintList_free(temp);
1540
1541         temp = falseBranch->falseEnsuresConstraints;
1542         falseBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(falseBranch);
1543         constraintList_free(temp);
1544
1545         /* if pred is true e equals true otherwise pred equals false */
1546
1547         cons =  constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
1548         trueBranch->ensuresConstraints = constraintList_add(trueBranch->ensuresConstraints, cons);
1549
1550         cons =  constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
1551         falseBranch->ensuresConstraints = constraintList_add(falseBranch->ensuresConstraints, cons);
1552
1553         e = doIfElse (e, pred, trueBranch, falseBranch);
1554       }
1555       break;
1556     case XPR_COMMA:
1557       llassert(FALSE);
1558       t1 = exprData_getPairA (data);
1559       t2 = exprData_getPairB (data);
1560     /* we essiantially treat this like expr1; expr2
1561      of course sequencePoint isn't adjusted so this isn't completely accurate
1562     problems../  */
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       handledExprNode = FALSE;
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
1576   e->ensuresConstraints  = constraintList_addGeneratingExpr (e->ensuresConstraints, e);
1577
1578
1579   e->requiresConstraints = constraintList_removeSurpressed(e->requiresConstraints);
1580
1581   DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->ensuresConstraints))));
1582
1583   DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->ensuresConstraints))));
1584
1585   DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->trueEnsuresConstraints))));
1586
1587   DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->falseEnsuresConstraints))));
1588
1589   return;
1590 }
1591
1592
1593 constraintList exprNode_traversTrueEnsuresConstraints (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_traversTrueEnsuresConstraints (t1));
1618       break;
1619
1620     case XPR_FETCH:
1621
1622       ret = constraintList_addListFree (ret,
1623                                     exprNode_traversTrueEnsuresConstraints
1624                                     (exprData_getPairA (data)));
1625
1626       ret = constraintList_addListFree (ret,
1627                                     exprNode_traversTrueEnsuresConstraints
1628                                     (exprData_getPairB (data)));
1629       break;
1630     case XPR_PREOP:
1631
1632       ret = constraintList_addListFree (ret,
1633                                     exprNode_traversTrueEnsuresConstraints
1634                                     (exprData_getUopNode (data)));
1635       break;
1636
1637     case XPR_PARENS:
1638       ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints
1639                                     (exprData_getUopNode (data)));
1640       break;
1641
1642     case XPR_INIT:
1643       ret = constraintList_addListFree (ret,
1644                                         exprNode_traversTrueEnsuresConstraints
1645                                         (exprData_getInitNode (data)));
1646         break;
1647
1648
1649     case XPR_ASSIGN:
1650         ret = constraintList_addListFree (ret,
1651                                     exprNode_traversTrueEnsuresConstraints
1652                                     (exprData_getOpA (data)));
1653
1654        ret = constraintList_addListFree (ret,
1655                                     exprNode_traversTrueEnsuresConstraints
1656                                     (exprData_getOpB (data)));
1657        break;
1658     case XPR_OP:
1659        ret = constraintList_addListFree (ret,
1660                                     exprNode_traversTrueEnsuresConstraints
1661                                     (exprData_getOpA (data)));
1662
1663        ret = constraintList_addListFree (ret,
1664                                     exprNode_traversTrueEnsuresConstraints
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_traversTrueEnsuresConstraints
1674                                          (exprData_getSingle (data)));
1675        break;
1676
1677     case XPR_CALL:
1678       ret = constraintList_addListFree (ret,
1679                                      exprNode_traversTrueEnsuresConstraints
1680                                     (exprData_getFcn (data)));
1681       break;
1682
1683     case XPR_RETURN:
1684       ret = constraintList_addListFree (ret,
1685                                     exprNode_traversTrueEnsuresConstraints
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_traversTrueEnsuresConstraints
1695                                         (exprData_getFieldNode (data)));
1696       break;
1697
1698     case XPR_ARROW:
1699       ret = constraintList_addListFree (ret,
1700                                         exprNode_traversTrueEnsuresConstraints
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_traversTrueEnsuresConstraints
1713                                     (exprData_getUopNode (data)));
1714            break;
1715
1716     case XPR_CAST:
1717
1718       ret = constraintList_addListFree (ret,
1719                                     exprNode_traversTrueEnsuresConstraints
1720                                     (exprData_getCastNode (data)));
1721       break;
1722
1723     default:
1724       break;
1725     }
1726
1727   return ret;
1728 }
1729
1730 constraintList exprNode_traversFalseEnsuresConstraints (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_traversFalseEnsuresConstraints (t1));
1752       break;
1753
1754     case XPR_FETCH:
1755
1756       ret = constraintList_addListFree (ret,
1757                                     exprNode_traversFalseEnsuresConstraints
1758                                     (exprData_getPairA (data)));
1759
1760       ret = constraintList_addListFree (ret,
1761                                     exprNode_traversFalseEnsuresConstraints
1762                                     (exprData_getPairB (data)));
1763       break;
1764     case XPR_PREOP:
1765
1766       ret = constraintList_addListFree (ret,
1767                                     exprNode_traversFalseEnsuresConstraints
1768                                     (exprData_getUopNode (data)));
1769       break;
1770
1771     case XPR_PARENS:
1772       ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints
1773                                     (exprData_getUopNode (data)));
1774       break;
1775     case XPR_INIT:
1776         ret = constraintList_addListFree (ret,
1777                                     exprNode_traversFalseEnsuresConstraints
1778                                     (   exprData_getInitNode (data)));
1779         break;
1780
1781     case XPR_ASSIGN:
1782         ret = constraintList_addListFree (ret,
1783                                     exprNode_traversFalseEnsuresConstraints
1784                                     (exprData_getOpA (data)));
1785
1786        ret = constraintList_addListFree (ret,
1787                                     exprNode_traversFalseEnsuresConstraints
1788                                     (exprData_getOpB (data)));
1789        break;
1790     case XPR_OP:
1791        ret = constraintList_addListFree (ret,
1792                                     exprNode_traversFalseEnsuresConstraints
1793                                     (exprData_getOpA (data)));
1794
1795        ret = constraintList_addListFree (ret,
1796                                     exprNode_traversFalseEnsuresConstraints
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_traversFalseEnsuresConstraints
1806                                      (exprData_getSingle (data)));
1807        break;
1808
1809     case XPR_CALL:
1810       ret = constraintList_addListFree (ret,
1811                                      exprNode_traversFalseEnsuresConstraints
1812                                     (exprData_getFcn (data)));
1813       break;
1814
1815     case XPR_RETURN:
1816       ret = constraintList_addListFree (ret,
1817                                     exprNode_traversFalseEnsuresConstraints
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_traversFalseEnsuresConstraints
1827                                         (exprData_getFieldNode (data)));
1828       break;
1829
1830     case XPR_ARROW:
1831       ret = constraintList_addListFree (ret,
1832                                         exprNode_traversFalseEnsuresConstraints
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_traversFalseEnsuresConstraints
1845                                     (exprData_getUopNode (data)));
1846            break;
1847
1848     case XPR_CAST:
1849
1850       ret = constraintList_addListFree (ret,
1851                                     exprNode_traversFalseEnsuresConstraints
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_traversRequiresConstraints (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_traversRequiresConstraints (t1));
1887       break;
1888
1889     case XPR_FETCH:
1890
1891       ret = constraintList_addListFree (ret,
1892                                     exprNode_traversRequiresConstraints
1893                                     (exprData_getPairA (data)));
1894
1895       ret = constraintList_addListFree (ret,
1896                                     exprNode_traversRequiresConstraints
1897                                     (exprData_getPairB (data)));
1898       break;
1899     case XPR_PREOP:
1900
1901       ret = constraintList_addListFree (ret,
1902                                     exprNode_traversRequiresConstraints
1903                                     (exprData_getUopNode (data)));
1904       break;
1905
1906     case XPR_PARENS:
1907       ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints
1908                                     (exprData_getUopNode (data)));
1909       break;
1910     case XPR_INIT:
1911       ret = constraintList_addListFree (ret,
1912                                         exprNode_traversRequiresConstraints
1913                                         (exprData_getInitNode (data)));
1914         break;
1915
1916     case XPR_ASSIGN:
1917         ret = constraintList_addListFree (ret,
1918                                     exprNode_traversRequiresConstraints
1919                                     (exprData_getOpA (data)));
1920
1921        ret = constraintList_addListFree (ret,
1922                                     exprNode_traversRequiresConstraints
1923                                     (exprData_getOpB (data)));
1924        break;
1925     case XPR_OP:
1926        ret = constraintList_addListFree (ret,
1927                                     exprNode_traversRequiresConstraints
1928                                     (exprData_getOpA (data)));
1929
1930        ret = constraintList_addListFree (ret,
1931                                     exprNode_traversRequiresConstraints
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_traversRequiresConstraints
1941                                      (exprData_getSingle (data)));
1942        break;
1943
1944     case XPR_CALL:
1945       ret = constraintList_addListFree (ret,
1946                                      exprNode_traversRequiresConstraints
1947                                     (exprData_getFcn (data)));
1948       break;
1949
1950     case XPR_RETURN:
1951       ret = constraintList_addListFree (ret,
1952                                     exprNode_traversRequiresConstraints
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_traversRequiresConstraints
1962                                         (exprData_getFieldNode (data)));
1963       break;
1964
1965     case XPR_ARROW:
1966       ret = constraintList_addListFree (ret,
1967                                         exprNode_traversRequiresConstraints
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_traversRequiresConstraints
1980                                     (exprData_getUopNode (data)));
1981            break;
1982
1983     case XPR_CAST:
1984
1985       ret = constraintList_addListFree (ret,
1986                                     exprNode_traversRequiresConstraints
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_traversEnsuresConstraints (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_traversEnsuresConstraints (t1));
2031       break;
2032
2033     case XPR_FETCH:
2034       ret = constraintList_addListFree (ret,
2035                                         exprNode_traversEnsuresConstraints
2036                                         (exprData_getPairA (data)));
2037
2038       ret = constraintList_addListFree (ret,
2039                                         exprNode_traversEnsuresConstraints
2040                                         (exprData_getPairB (data)));
2041       break;
2042     case XPR_PREOP:
2043       ret = constraintList_addListFree (ret,
2044                                         exprNode_traversEnsuresConstraints
2045                                         (exprData_getUopNode (data)));
2046       break;
2047
2048     case XPR_PARENS:
2049       ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints
2050                                         (exprData_getUopNode (data)));
2051       break;
2052
2053     case XPR_INIT:
2054       ret = constraintList_addListFree (ret,
2055                                         exprNode_traversEnsuresConstraints
2056                                         (exprData_getInitNode (data)));
2057       break;
2058
2059
2060     case XPR_ASSIGN:
2061       ret = constraintList_addListFree (ret,
2062                                         exprNode_traversEnsuresConstraints
2063                                         (exprData_getOpA (data)));
2064
2065       ret = constraintList_addListFree (ret,
2066                                         exprNode_traversEnsuresConstraints
2067                                         (exprData_getOpB (data)));
2068       break;
2069     case XPR_OP:
2070       ret = constraintList_addListFree (ret,
2071                                         exprNode_traversEnsuresConstraints
2072                                         (exprData_getOpA (data)));
2073
2074       ret = constraintList_addListFree (ret,
2075                                         exprNode_traversEnsuresConstraints
2076                                         (exprData_getOpB (data)));
2077       break;
2078     case XPR_SIZEOFT:
2079       break;
2080
2081     case XPR_SIZEOF:
2082       ret = constraintList_addListFree (ret,
2083                                         exprNode_traversEnsuresConstraints
2084                                         (exprData_getSingle (data)));
2085       break;
2086     case XPR_CALL:
2087       ret = constraintList_addListFree (ret,
2088                                         exprNode_traversEnsuresConstraints
2089                                         (exprData_getFcn (data)));
2090       break;
2091     case XPR_RETURN:
2092       ret = constraintList_addListFree (ret,
2093                                         exprNode_traversEnsuresConstraints
2094                                         (exprData_getSingle (data)));
2095       break;
2096     case XPR_NULLRETURN:
2097       break;
2098     case XPR_FACCESS:
2099       ret = constraintList_addListFree (ret,
2100                                         exprNode_traversEnsuresConstraints
2101                                         (exprData_getFieldNode (data)));
2102       break;
2103     case XPR_ARROW:
2104       ret = constraintList_addListFree (ret,
2105                                         exprNode_traversEnsuresConstraints
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_traversEnsuresConstraints
2115                                         (exprData_getUopNode (data)));
2116       break;
2117     case XPR_CAST:
2118       ret = constraintList_addListFree (ret,
2119                                         exprNode_traversEnsuresConstraints
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_traversRequiresConstraints(el);
2155       constraintList_free(temp2);
2156
2157       temp2 = el->ensuresConstraints;
2158       el->ensuresConstraints  = exprNode_traversEnsuresConstraints(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