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
 683                                         (stmt->edata), exprNode_getfileloc(stmt));
 684
 685
 686       constraintList_free(*currentEnsures);
 687       *currentEnsures = constraintList_makeNew();
 688       *currentEnsures = constraintList_add(*currentEnsures, con);
 689
 690       constraintList_free(*currentRequires);
 691       *currentRequires = constraintList_makeNew();
 692       DPRINTF((message("exprNode_doGenerateConstraintSwitch: (switch %s) %s savedRequires:"
 693                         "%s savedEnsures:%s",
 694                         exprNode_unparse(switchExpr), exprNode_unparse(body),
 695                         constraintList_unparse(*savedRequires), constraintList_unparse(*savedEnsures)
 696                         )));
 697
 698     }
 699
 700   else if (exprNode_isCaseMarker(stmt))
 701     /* 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
 712       constraintList ensuresTemp;
 713
 714       DPRINTF ((message("Got case marker with no prior break")));
 715
 716       con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle
 717                                         (stmt->edata), exprNode_getfileloc(stmt));
 718
 719       ensuresTemp = constraintList_makeNew();
 720
 721       ensuresTemp = constraintList_add (ensuresTemp, con);
 722
 723       if (exprNode_isError(stmtList))
 724         {
 725           constraintList_free(*currentEnsures);
 726
 727           *currentEnsures = constraintList_copy(ensuresTemp);
 728           constraintList_free(ensuresTemp);
 729
 730         }
 731       else
 732         {
 733
 734           temp = constraintList_logicalOr (*currentEnsures, ensuresTemp);
 735
 736           constraintList_free(*currentEnsures);
 737           constraintList_free(ensuresTemp);
 738
 739           *currentEnsures = temp;
 740         }
 741       constraintList_free(*currentRequires);
 742
 743       *currentRequires = constraintList_makeNew();
 744     }
 745   else
 746     {
 747       /*
 748         we handle the case of ! exprNode_isCaseMarker above
 749         the else if clause should always be true.
 750       */
 751       BADEXIT;
 752     }
 753
 754   DPRINTF((message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
 755                     "%s currentEnsures:%s",
 756                     exprNode_unparse(switchExpr), exprNode_unparse(body),
 757                     constraintList_unparse(*currentRequires), constraintList_unparse(*currentEnsures)
 758                    )));
 759   /*@-onlytrans@*/
 760   return;
 761   /*@=onlytrans@*/
 762 }
 763
 764
 765 static void exprNode_generateConstraintSwitch (/*@notnull@*/ exprNode switchStmt)
 766 {
 767   constraintList constraintsRequires;
 768   constraintList constraintsEnsures;
 769   constraintList lastRequires;
 770   constraintList lastEnsures;
 771
 772   exprNode body;
 773   exprNode switchExpr;
 774
 775   switchExpr = exprData_getPairA (switchStmt->edata);
 776   body = exprData_getPairB (switchStmt->edata);
 777
 778   if (!exprNode_isDefined (body))
 779     {
 780       return;
 781     }
 782
 783   DPRINTF((message("")));
 784
 785   if (body->kind == XPR_BLOCK)
 786     body = exprData_getSingle(body->edata);
 787
 788
 789   constraintsRequires = constraintList_undefined;
 790   constraintsEnsures = constraintList_undefined;
 791
 792   lastRequires = constraintList_makeNew();
 793   lastEnsures = constraintList_makeNew();
 794
 795
 796   /*@-mustfree@*/
 797   /* evans 2002-01-01: spurious warnings for these becuase of stack allocated storage */
 798   exprNode_doGenerateConstraintSwitch (switchExpr, body, &lastRequires,
 799                                        &lastEnsures, &constraintsRequires, &constraintsEnsures);
 800   /*@=mustfree@*/
 801
 802   /*
 803     merge current and saved constraint with Logical Or...
 804     make a constraint for ensures
 805   */
 806
 807   constraintList_free(switchStmt->requiresConstraints);
 808   constraintList_free(switchStmt->ensuresConstraints);
 809
 810   if (constraintList_isDefined(constraintsEnsures) && constraintList_isDefined(constraintsRequires))
 811     {
 812       switchStmt->ensuresConstraints = constraintList_logicalOr(constraintsEnsures, lastEnsures);
 813       switchStmt->requiresConstraints =   constraintList_mergeRequires(constraintsRequires, lastRequires);
 814       constraintList_free (constraintsRequires);
 815       constraintList_free (constraintsEnsures);
 816     }
 817   else
 818     {
 819       switchStmt->ensuresConstraints =    constraintList_copy(lastEnsures);
 820       switchStmt->requiresConstraints =   constraintList_copy(lastRequires);
 821     }
 822
 823   constraintList_free (lastRequires);
 824   constraintList_free (lastEnsures);
 825
 826   DPRINTF(((message(" exprNode_generateConstraintSwitch returning requires: %s and ensures %s",
 827                      constraintList_unparse(switchStmt->requiresConstraints),
 828                      constraintList_unparse(switchStmt->ensuresConstraints)
 829                     )
 830             )));
 831 }
 832
 833 static exprNode doSwitch (/*@returned@*/ /*@notnull@*/ exprNode e)
 834 {
 835   exprNode body;
 836   exprData data;
 837
 838   data = e->edata;
 839   DPRINTF ((message ("doSwitch for: switch (%s) %s",
 840                       exprNode_unparse (exprData_getPairA (data)),
 841                       exprNode_unparse (exprData_getPairB (data)))));
 842
 843   body = exprData_getPairB (data);
 844   exprNode_generateConstraintSwitch (e);
 845   return e;
 846 }
 847
 848 void exprNode_multiStatement (/*@dependent@*/ exprNode e)
 849 {
 850
 851   bool ret;
 852   exprData data;
 853   exprNode e1, e2;
 854   exprNode p, trueBranch, falseBranch;
 855   exprNode forPred, forBody;
 856   exprNode test;
 857
 858   constraintList temp;
 859
 860   DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse(e),
 861                     fileloc_unparse(exprNode_getfileloc(e)))));
 862
 863   if (exprNode_handleError (e))
 864     {
 865       return;
 866     }
 867
 868   data = e->edata;
 869
 870   ret = TRUE;
 871
 872   switch (e->kind)
 873     {
 874
 875     case XPR_FOR:
 876       forPred = exprData_getPairA (data);
 877       forBody = exprData_getPairB (data);
 878
 879       /* First generate the constraints */
 880       exprNode_generateConstraints (forPred);
 881       exprNode_generateConstraints (forBody);
 882
 883
 884       doFor (e, forPred, forBody);
 885
 886       break;
 887
 888     case XPR_FORPRED:
 889       exprNode_generateConstraints (exprData_getTripleInit (data));
 890       test = exprData_getTripleTest (data);
 891       exprNode_exprTraverse (test,FALSE, FALSE, exprNode_loc(e));
 892       exprNode_generateConstraints (exprData_getTripleInc (data));
 893
 894       if (!exprNode_isError(test))
 895         {
 896           constraintList temp2;
 897           temp2 = test->trueEnsuresConstraints;
 898           test->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(test);
 899           constraintList_free(temp2);
 900         }
 901
 902       exprNode_generateConstraints (exprData_getTripleInc (data));
 903       break;
 904
 905     case XPR_WHILE:
 906       e1 = exprData_getPairA (data);
 907       e2 = exprData_getPairB (data);
 908
 909        exprNode_exprTraverse (e1,
 910                               FALSE, FALSE, exprNode_loc(e1));
 911
 912        exprNode_generateConstraints (e2);
 913
 914        e = doWhile (e, e1, e2);
 915
 916       break;
 917
 918     case XPR_IF:
 919       DPRINTF(("IF:"));
 920       DPRINTF ((exprNode_unparse(e)));
 921       e1 = exprData_getPairA (data);
 922       e2 = exprData_getPairB (data);
 923
 924       exprNode_exprTraverse (e1, FALSE, FALSE, exprNode_loc(e1));
 925
 926       exprNode_generateConstraints (e2);
 927       e = doIf (e, e1, e2);
 928       break;
 929
 930     case XPR_IFELSE:
 931       DPRINTF(("Starting IFELSE"));
 932       p = exprData_getTriplePred (data);
 933
 934       trueBranch = exprData_getTripleTrue (data);
 935       falseBranch = exprData_getTripleFalse (data);
 936
 937       exprNode_exprTraverse (p,
 938                              FALSE, FALSE, exprNode_loc(p));
 939       exprNode_generateConstraints (trueBranch);
 940       exprNode_generateConstraints (falseBranch);
 941
 942       llassert (exprNode_isDefined (p));
 943       temp = p->ensuresConstraints;
 944       p->ensuresConstraints = exprNode_traversEnsuresConstraints (p);
 945       constraintList_free(temp);
 946
 947       temp = p->requiresConstraints;
 948       p->requiresConstraints = exprNode_traversRequiresConstraints (p);
 949       constraintList_free(temp);
 950
 951       temp = p->trueEnsuresConstraints;
 952       p->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(p);
 953       constraintList_free(temp);
 954
 955
 956
 957       DPRINTF((message("p->trueEnsuresConstraints before substitue %s", constraintList_unparse(p->trueEnsuresConstraints)  )
 958                ));
 959
 960             /*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*/
 961
 962       p->trueEnsuresConstraints = constraintList_substituteFreeTarget (p->trueEnsuresConstraints,
 963                                                                        p->ensuresConstraints);
 964
 965       DPRINTF(( message ("p->trueEnsuresConstraints after substitue %s", constraintList_unparse(p->trueEnsuresConstraints) )
 966                 ));
 967
 968       temp = p->falseEnsuresConstraints;
 969       p->falseEnsuresConstraints =  exprNode_traversFalseEnsuresConstraints(p);
 970       constraintList_free(temp);
 971
 972       /*See comment on trueEnsures*/
 973       p->falseEnsuresConstraints = constraintList_substituteFreeTarget (p->falseEnsuresConstraints,
 974                                                                        p->ensuresConstraints);
 975
 976       e = doIfElse (e, p, trueBranch, falseBranch);
 977       DPRINTF(("Done IFELSE"));
 978       break;
 979
 980     case XPR_DOWHILE:
 981
 982       e2 = (exprData_getPairB (data));
 983       e1 = (exprData_getPairA (data));
 984
 985       DPRINTF((message ("do { %s } while (%s)", exprNode_unparse(e2), exprNode_unparse(e1))));
 986       exprNode_generateConstraints (e2);
 987       exprNode_generateConstraints (e1);
 988       e = exprNode_copyConstraints (e, e2);
 989       DPRINTF ((message ("e = %s  ", constraintList_unparse(e->requiresConstraints))));
 990
 991       break;
 992
 993     case XPR_BLOCK:
 994       {
 995         exprNode tempExpr;
 996
 997         tempExpr = exprData_getSingle (data);
 998
 999         exprNode_generateConstraints (tempExpr);
1000
1001         if (exprNode_isDefined(tempExpr) )
1002           {
1003             constraintList_free(e->requiresConstraints);
1004             e->requiresConstraints = constraintList_copy (tempExpr->requiresConstraints);
1005             constraintList_free(e->ensuresConstraints);
1006             e->ensuresConstraints = constraintList_copy (tempExpr->ensuresConstraints);
1007           }
1008         else
1009           {
1010             llassert(FALSE);
1011           }
1012       }
1013       break;
1014
1015     case XPR_SWITCH:
1016       e = doSwitch (e);
1017       break;
1018     case XPR_STMT:
1019     case XPR_STMTLIST:
1020       exprNode_stmtList (e);
1021       return ;
1022       /*@notreached@*/
1023       break;
1024     default:
1025       ret=FALSE;
1026     }
1027   return;
1028 }
1029
1030 static bool lltok_isBoolean_Op (lltok tok)
1031 {
1032   /*this should really be a switch statement but
1033     I don't want to violate the abstraction
1034     maybe this should go in lltok.c */
1035
1036   if (lltok_isEqOp (tok))
1037         {
1038           return TRUE;
1039         }
1040       if (lltok_isAndOp (tok))
1041
1042         {
1043
1044           return TRUE;
1045         }
1046    if (lltok_isOrOp (tok))
1047         {
1048           return TRUE;
1049         }
1050
1051    if (lltok_isGt_Op (tok))
1052      {
1053        return TRUE;
1054      }
1055    if (lltok_isLt_Op (tok))
1056      {
1057        return TRUE;
1058      }
1059
1060    if (lltok_isLe_Op (tok))
1061      {
1062        return TRUE;
1063      }
1064
1065    if (lltok_isGe_Op (tok))
1066      {
1067        return TRUE;
1068      }
1069
1070    return FALSE;
1071
1072 }
1073
1074
1075 static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ bool definatelv, /*@unused@*/ bool definaterv,  fileloc sequencePoint)
1076 {
1077   constraint cons;
1078   exprNode t1, t2;
1079   exprData data;
1080   lltok tok;
1081   constraintList tempList, temp;
1082
1083   if (exprNode_isUndefined(e) )
1084     {
1085       llassert (exprNode_isDefined(e) );
1086       return;
1087     }
1088
1089   data = e->edata;
1090
1091   tok = exprData_getOpTok (data);
1092   t1 = exprData_getOpA (data);
1093   t2 = exprData_getOpB (data);
1094
1095   /* drl 3/2/2003 we know this because of the type of expression*/
1096   llassert( exprNode_isDefined(t1) &&   exprNode_isDefined(t2) );
1097
1098
1099   tempList = constraintList_undefined;
1100
1101   /* arithmetic tests */
1102
1103   if (lltok_isEqOp (tok))
1104     {
1105       cons =  constraint_makeEnsureEqual (t1, t2, sequencePoint);
1106       e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1107     }
1108
1109
1110   if (lltok_isLt_Op (tok))
1111     {
1112       cons =  constraint_makeEnsureLessThan (t1, t2, sequencePoint);
1113       e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1114       cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
1115       e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1116     }
1117
1118   if (lltok_isGe_Op (tok))
1119     {
1120       cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
1121       e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1122
1123       cons =  constraint_makeEnsureLessThan (t1, t2, sequencePoint);
1124       e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1125     }
1126
1127   if (lltok_isGt_Op (tok))
1128     {
1129       cons =  constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
1130       e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1131       cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
1132       e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1133     }
1134
1135   if (lltok_isLe_Op (tok))
1136     {
1137       cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
1138       e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1139
1140       cons =  constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
1141       e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1142     }
1143
1144   /* Logical operations */
1145
1146   if (lltok_isAndOp (tok))
1147     {
1148       /* true ensures  */
1149       tempList = constraintList_copy (t1->trueEnsuresConstraints);
1150       tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
1151       e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList);
1152
1153       /* false ensures: fens t1 or tens t1 and fens t2 */
1154       tempList = constraintList_copy (t1->trueEnsuresConstraints);
1155       tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
1156       temp = tempList;
1157       tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints);
1158       constraintList_free (temp);
1159
1160       /* evans - was constraintList_addList - memory leak detected by splint */
1161       e->falseEnsuresConstraints = constraintList_addListFree (e->falseEnsuresConstraints, tempList);
1162     }
1163   else if (lltok_isOrOp (tok))
1164     {
1165       /* false ensures */
1166       tempList = constraintList_copy (t1->falseEnsuresConstraints);
1167       tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
1168       e->falseEnsuresConstraints = constraintList_addListFree(e->falseEnsuresConstraints, tempList);
1169
1170       /* true ensures: tens t1 or fens t1 and tens t2 */
1171       tempList = constraintList_copy (t1->falseEnsuresConstraints);
1172       tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
1173
1174       temp = tempList;
1175       tempList = constraintList_logicalOr (tempList, t1->trueEnsuresConstraints);
1176       constraintList_free(temp);
1177
1178       e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList);
1179       tempList = constraintList_undefined;
1180     }
1181   else
1182     {
1183       DPRINTF((message("%s is not a boolean operation", lltok_unparse(tok))));
1184     }
1185 }
1186
1187 void exprNode_exprTraverse (/*@dependent@*/ exprNode e, bool definatelv, bool definaterv,  /*@observer@*/ /*@temp@*/ fileloc sequencePoint)
1188 {
1189   exprNode t1, t2, fcn;
1190   lltok tok;
1191   bool handledExprNode;
1192   exprData data;
1193   constraint cons;
1194
1195   constraintList temp;
1196
1197   if (exprNode_isError(e))
1198     {
1199       return;
1200     }
1201
1202   DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse(e),
1203                     fileloc_unparse(exprNode_getfileloc(e)))));
1204
1205   /*e->requiresConstraints = constraintList_makeNew();
1206   e->ensuresConstraints = constraintList_makeNew();
1207   e->trueEnsuresConstraints = constraintList_makeNew();;
1208   e->falseEnsuresConstraints = constraintList_makeNew();;
1209   */
1210
1211   if (exprNode_isUnhandled (e))
1212      {
1213        return;
1214      }
1215
1216   handledExprNode = TRUE;
1217
1218   data = e->edata;
1219
1220   switch (e->kind)
1221     {
1222     case XPR_WHILEPRED:
1223       t1 = exprData_getSingle (data);
1224       exprNode_exprTraverse (t1,  definatelv, definaterv, sequencePoint);
1225       e = exprNode_copyConstraints (e, t1);
1226       break;
1227
1228     case XPR_FETCH:
1229
1230       if (definatelv)
1231         {
1232           t1 =  (exprData_getPairA (data));
1233           t2 =  (exprData_getPairB (data));
1234           cons =  constraint_makeWriteSafeExprNode (t1, t2);
1235         }
1236       else
1237         {
1238           t1 =  (exprData_getPairA (data));
1239           t2 =  (exprData_getPairB (data));
1240           cons = constraint_makeReadSafeExprNode (t1, t2);
1241         }
1242
1243       e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
1244       cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint);
1245       e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1246
1247       cons = constraint_makeEnsureLteMaxRead (t2, t1);
1248       e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1249
1250       exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
1251       exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
1252
1253       break;
1254
1255     case XPR_PARENS:
1256       exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint);
1257       break;
1258     case XPR_INIT:
1259       {
1260         /*
1261         idDecl t;
1262
1263         uentry ue;
1264         exprNode lhs;
1265
1266         t = exprData_getInitId (data);
1267         ue = usymtab_lookup (idDecl_observeId (t));
1268         lhs = exprNode_createId (ue);
1269         */
1270         t2 = exprData_getInitNode (data);
1271
1272         /*      DPRINTF(((message("initialization: %s = %s",
1273                            exprNode_unparse(lhs),
1274                            exprNode_unparse(t2)
1275                           )
1276                   )));  */
1277
1278         exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
1279
1280         /* this test is nessecary because some expressions generate a null expression node.  function pointer do that -- drl */
1281         if ((!exprNode_isError (e))  &&  (!exprNode_isError(t2)))
1282           {
1283             cons =  constraint_makeEnsureEqual (e, t2, sequencePoint);
1284             e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1285           }
1286       }
1287
1288       break;
1289     case XPR_ASSIGN:
1290       t1 = exprData_getOpA (data);
1291       t2 = exprData_getOpB (data);
1292       exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint);
1293       exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
1294
1295       /* this test is nessecary because some expressions generate a null expression node.  function pointer do that -- drl */
1296       if ((!exprNode_isError (t1))  &&  (!exprNode_isError(t2)))
1297         {
1298           cons =  constraint_makeEnsureEqual (t1, t2, sequencePoint);
1299           e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1300         }
1301       break;
1302     case XPR_OP:
1303       t1 = exprData_getOpA (data);
1304       t2 = exprData_getOpB (data);
1305       tok = exprData_getOpTok (data);
1306
1307       if (lltok_getTok (tok) == ADD_ASSIGN)
1308         {
1309           exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint);
1310           exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
1311
1312           cons = constraint_makeAddAssign (t1, t2,  sequencePoint);
1313           e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1314         }
1315       else if (lltok_getTok (tok) == SUB_ASSIGN)
1316         {
1317           exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint);
1318           exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
1319
1320           cons = constraint_makeSubtractAssign (t1, t2,  sequencePoint);
1321           e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1322         }
1323       else
1324         {
1325           exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint);
1326           exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint);
1327         }
1328
1329       if (lltok_isBoolean_Op (tok))
1330         exprNode_booleanTraverse (e, definatelv, definaterv, sequencePoint);
1331
1332       break;
1333     case XPR_SIZEOFT:
1334       /*drl 4-11-03 I think this is the same as the next case...*/
1335
1336       break;
1337
1338     case XPR_SIZEOF:
1339       /* drl  7-16-01
1340          C standard says operand to sizeof isn't evaluated unless
1341          its a variable length array.  So we don't generate constraints.
1342       */
1343
1344       break;
1345
1346     case XPR_CALL:
1347       fcn = exprData_getFcn(data);
1348
1349       exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint);
1350       DPRINTF ((message ("Got call that %s (%s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (exprData_getArgs (data)))));
1351
1352       llassert( exprNode_isDefined(fcn) );
1353
1354       fcn->requiresConstraints = constraintList_addListFree (fcn->requiresConstraints,
1355                                                  checkCall (fcn, exprData_getArgs (data) ));
1356
1357       fcn->ensuresConstraints = constraintList_addListFree (fcn->ensuresConstraints,
1358                                                  exprNode_getPostConditions(fcn, exprData_getArgs (data),e ));
1359
1360       t1 = exprNode_createNew (exprNode_getType (e));
1361       checkArgumentList (t1, exprData_getArgs(data), sequencePoint);
1362       exprNode_mergeResolve (e, t1, fcn);
1363       exprNode_free(t1);
1364       break;
1365
1366     case XPR_RETURN:
1367       exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint);
1368       break;
1369
1370     case XPR_NULLRETURN:
1371
1372       break;
1373
1374
1375     case XPR_FACCESS:
1376       exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint);
1377       break;
1378
1379     case XPR_ARROW:
1380       exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint);
1381       break;
1382
1383     case XPR_STRINGLITERAL:
1384
1385       break;
1386
1387     case XPR_NUMLIT:
1388
1389       break;
1390
1391     case XPR_PREOP:
1392       t1 = exprData_getUopNode(data);
1393
1394
1395       /* drl 3/2/2003 we know this because of the type of expression*/
1396       llassert( exprNode_isDefined(t1) );
1397
1398
1399       tok = (exprData_getUopTok (data));
1400       exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint);
1401       /*handle * pointer access */
1402       if (lltok_isIncOp (tok))
1403         {
1404           DPRINTF(("doing ++(var)"));
1405           t1 = exprData_getUopNode (data);
1406           cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint);
1407           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1408         }
1409       else if (lltok_isDecOp (tok))
1410         {
1411           DPRINTF(("doing --(var)"));
1412           t1 = exprData_getUopNode (data);
1413           cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint);
1414           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1415         }
1416       else if (lltok_isMult(tok ))
1417         {
1418           if (definatelv)
1419             {
1420               cons = constraint_makeWriteSafeInt (t1, 0);
1421             }
1422           else
1423             {
1424               cons = constraint_makeReadSafeInt (t1, 0);
1425             }
1426               e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
1427         }
1428       else if (lltok_isNotOp (tok))
1429         /* ! expr */
1430         {
1431           constraintList_free(e->trueEnsuresConstraints);
1432
1433           e->trueEnsuresConstraints  = constraintList_copy (t1->falseEnsuresConstraints);
1434           constraintList_free(e->falseEnsuresConstraints);
1435           e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints);
1436         }
1437
1438       else if (lltok_isAmpersand_Op (tok))
1439         {
1440           break;
1441         }
1442       else if (lltok_isMinus_Op (tok))
1443         {
1444           break;
1445         }
1446       else if (lltok_isExcl_Op (tok))
1447         {
1448           break;
1449         }
1450       else if (lltok_isTilde_Op (tok))
1451         {
1452           break;
1453         }
1454       else
1455         {
1456           llcontbug (message("Unsupported preop in %s", exprNode_unparse(e)));
1457           BADEXIT;
1458         }
1459       break;
1460
1461     case XPR_POSTOP:
1462       exprNode_exprTraverse (exprData_getUopNode (data), TRUE,
1463                              definaterv, sequencePoint);
1464
1465       if (lltok_isIncOp (exprData_getUopTok (data)))
1466         {
1467           DPRINTF(("doing ++"));
1468           t1 = exprData_getUopNode (data);
1469           cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint);
1470           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1471         }
1472        if (lltok_isDecOp (exprData_getUopTok (data)))
1473         {
1474           DPRINTF(("doing --"));
1475           t1 = exprData_getUopNode (data);
1476           cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint);
1477           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1478         }
1479       break;
1480     case XPR_CAST:
1481       {
1482         t2 =  exprData_getCastNode (data);
1483         DPRINTF ((message ("Examining cast (%q)%s",
1484                             qtype_unparse (exprData_getCastType (data)),
1485                             exprNode_unparse (t2))
1486                   ));
1487         exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint);
1488       }
1489       break;
1490
1491     case XPR_COND:
1492       {
1493         exprNode pred, trueBranch, falseBranch;
1494         llassert(FALSE);
1495         pred = exprData_getTriplePred (data);
1496         trueBranch = exprData_getTripleTrue (data);
1497         falseBranch = exprData_getTripleFalse (data);
1498
1499         llassert (exprNode_isDefined (pred));
1500         llassert (exprNode_isDefined (trueBranch));
1501         llassert (exprNode_isDefined (falseBranch));
1502
1503         exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint);
1504
1505         temp = pred->ensuresConstraints;
1506         pred->ensuresConstraints = exprNode_traversEnsuresConstraints(pred);
1507         constraintList_free(temp);
1508
1509         temp = pred->requiresConstraints;
1510         pred->requiresConstraints = exprNode_traversRequiresConstraints(pred);
1511         constraintList_free(temp);
1512
1513         temp = pred->trueEnsuresConstraints;
1514         pred->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(pred);
1515         constraintList_free(temp);
1516
1517         temp = pred->falseEnsuresConstraints;
1518         pred->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(pred);
1519         constraintList_free(temp);
1520
1521         exprNode_exprTraverse (trueBranch, FALSE, TRUE, sequencePoint);
1522
1523         temp = trueBranch->ensuresConstraints;
1524         trueBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(trueBranch);
1525         constraintList_free(temp);
1526
1527         temp = trueBranch->requiresConstraints;
1528         trueBranch->requiresConstraints = exprNode_traversRequiresConstraints(trueBranch);
1529         constraintList_free(temp);
1530
1531
1532         temp =       trueBranch->trueEnsuresConstraints;
1533         trueBranch->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(trueBranch);
1534         constraintList_free(temp);
1535
1536         temp =       trueBranch->falseEnsuresConstraints;
1537         trueBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(trueBranch);
1538         constraintList_free(temp);
1539
1540         exprNode_exprTraverse (falseBranch, FALSE, TRUE, sequencePoint);
1541
1542         temp = falseBranch->ensuresConstraints;
1543         falseBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(falseBranch);
1544         constraintList_free(temp);
1545
1546
1547         temp = falseBranch->requiresConstraints;
1548         falseBranch->requiresConstraints = exprNode_traversRequiresConstraints(falseBranch);
1549         constraintList_free(temp);
1550
1551         temp = falseBranch->trueEnsuresConstraints;
1552         falseBranch->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(falseBranch);
1553         constraintList_free(temp);
1554
1555         temp = falseBranch->falseEnsuresConstraints;
1556         falseBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(falseBranch);
1557         constraintList_free(temp);
1558
1559         /* if pred is true e equals true otherwise pred equals false */
1560
1561         cons =  constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
1562         trueBranch->ensuresConstraints = constraintList_add(trueBranch->ensuresConstraints, cons);
1563
1564         cons =  constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
1565         falseBranch->ensuresConstraints = constraintList_add(falseBranch->ensuresConstraints, cons);
1566
1567         e = doIfElse (e, pred, trueBranch, falseBranch);
1568       }
1569       break;
1570     case XPR_COMMA:
1571       llassert(FALSE);
1572       t1 = exprData_getPairA (data);
1573       t2 = exprData_getPairB (data);
1574     /* we essiantially treat this like expr1; expr2
1575      of course sequencePoint isn't adjusted so this isn't completely accurate
1576     problems../  */
1577       exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint);
1578       exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint);
1579       exprNode_mergeResolve (e, t1, t2);
1580       break;
1581
1582     default:
1583       handledExprNode = FALSE;
1584     }
1585
1586   e->requiresConstraints =  constraintList_preserveOrig (e->requiresConstraints);
1587   e->ensuresConstraints  =  constraintList_preserveOrig (e->ensuresConstraints);
1588   e->requiresConstraints = constraintList_addGeneratingExpr (e->requiresConstraints, e);
1589
1590   e->ensuresConstraints  = constraintList_addGeneratingExpr (e->ensuresConstraints, e);
1591
1592
1593   e->requiresConstraints = constraintList_removeSurpressed(e->requiresConstraints);
1594
1595   DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->ensuresConstraints))));
1596
1597   DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->ensuresConstraints))));
1598
1599   DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->trueEnsuresConstraints))));
1600
1601   DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->falseEnsuresConstraints))));
1602
1603   return;
1604 }
1605
1606
1607 constraintList exprNode_traversTrueEnsuresConstraints (exprNode e)
1608 {
1609   exprNode t1;
1610
1611   bool handledExprNode;
1612   exprData data;
1613   constraintList ret;
1614
1615   if (exprNode_handleError (e))
1616     {
1617       ret = constraintList_makeNew();
1618       return ret;
1619     }
1620
1621   ret = constraintList_copy (e->trueEnsuresConstraints);
1622
1623   handledExprNode = TRUE;
1624
1625   data = e->edata;
1626
1627   switch (e->kind)
1628     {
1629     case XPR_WHILEPRED:
1630       t1 = exprData_getSingle (data);
1631       ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (t1));
1632       break;
1633
1634     case XPR_FETCH:
1635
1636       ret = constraintList_addListFree (ret,
1637                                     exprNode_traversTrueEnsuresConstraints
1638                                     (exprData_getPairA (data)));
1639
1640       ret = constraintList_addListFree (ret,
1641                                     exprNode_traversTrueEnsuresConstraints
1642                                     (exprData_getPairB (data)));
1643       break;
1644     case XPR_PREOP:
1645
1646       ret = constraintList_addListFree (ret,
1647                                     exprNode_traversTrueEnsuresConstraints
1648                                     (exprData_getUopNode (data)));
1649       break;
1650
1651     case XPR_PARENS:
1652       ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints
1653                                     (exprData_getUopNode (data)));
1654       break;
1655
1656     case XPR_INIT:
1657       ret = constraintList_addListFree (ret,
1658                                         exprNode_traversTrueEnsuresConstraints
1659                                         (exprData_getInitNode (data)));
1660         break;
1661
1662
1663     case XPR_ASSIGN:
1664         ret = constraintList_addListFree (ret,
1665                                     exprNode_traversTrueEnsuresConstraints
1666                                     (exprData_getOpA (data)));
1667
1668        ret = constraintList_addListFree (ret,
1669                                     exprNode_traversTrueEnsuresConstraints
1670                                     (exprData_getOpB (data)));
1671        break;
1672     case XPR_OP:
1673        ret = constraintList_addListFree (ret,
1674                                     exprNode_traversTrueEnsuresConstraints
1675                                     (exprData_getOpA (data)));
1676
1677        ret = constraintList_addListFree (ret,
1678                                     exprNode_traversTrueEnsuresConstraints
1679                                     (exprData_getOpB (data)));
1680        break;
1681     case XPR_SIZEOFT:
1682       break;
1683
1684     case XPR_SIZEOF:
1685
1686        ret = constraintList_addListFree (ret,
1687                                          exprNode_traversTrueEnsuresConstraints
1688                                          (exprData_getSingle (data)));
1689        break;
1690
1691     case XPR_CALL:
1692       ret = constraintList_addListFree (ret,
1693                                      exprNode_traversTrueEnsuresConstraints
1694                                     (exprData_getFcn (data)));
1695       break;
1696
1697     case XPR_RETURN:
1698       ret = constraintList_addListFree (ret,
1699                                     exprNode_traversTrueEnsuresConstraints
1700                                     (exprData_getSingle (data)));
1701       break;
1702
1703     case XPR_NULLRETURN:
1704       break;
1705
1706     case XPR_FACCESS:
1707       ret = constraintList_addListFree (ret,
1708                                         exprNode_traversTrueEnsuresConstraints
1709                                         (exprData_getFieldNode (data)));
1710       break;
1711
1712     case XPR_ARROW:
1713       ret = constraintList_addListFree (ret,
1714                                         exprNode_traversTrueEnsuresConstraints
1715                                         (exprData_getFieldNode (data)));
1716       break;
1717
1718     case XPR_STRINGLITERAL:
1719       break;
1720
1721     case XPR_NUMLIT:
1722       break;
1723     case XPR_POSTOP:
1724
1725            ret = constraintList_addListFree (ret,
1726                                     exprNode_traversTrueEnsuresConstraints
1727                                     (exprData_getUopNode (data)));
1728            break;
1729
1730     case XPR_CAST:
1731
1732       ret = constraintList_addListFree (ret,
1733                                     exprNode_traversTrueEnsuresConstraints
1734                                     (exprData_getCastNode (data)));
1735       break;
1736
1737     default:
1738       break;
1739     }
1740
1741   return ret;
1742 }
1743
1744 constraintList exprNode_traversFalseEnsuresConstraints (exprNode e)
1745 {
1746   exprNode t1;
1747   bool handledExprNode;
1748   exprData data;
1749   constraintList ret;
1750
1751   if (exprNode_handleError (e))
1752     {
1753       ret = constraintList_makeNew();
1754       return ret;
1755     }
1756
1757   ret = constraintList_copy (e->falseEnsuresConstraints);
1758   handledExprNode = TRUE;
1759   data = e->edata;
1760
1761   switch (e->kind)
1762     {
1763    case XPR_WHILEPRED:
1764       t1 = exprData_getSingle (data);
1765       ret = constraintList_addListFree (ret,exprNode_traversFalseEnsuresConstraints (t1));
1766       break;
1767
1768     case XPR_FETCH:
1769
1770       ret = constraintList_addListFree (ret,
1771                                     exprNode_traversFalseEnsuresConstraints
1772                                     (exprData_getPairA (data)));
1773
1774       ret = constraintList_addListFree (ret,
1775                                     exprNode_traversFalseEnsuresConstraints
1776                                     (exprData_getPairB (data)));
1777       break;
1778     case XPR_PREOP:
1779
1780       ret = constraintList_addListFree (ret,
1781                                     exprNode_traversFalseEnsuresConstraints
1782                                     (exprData_getUopNode (data)));
1783       break;
1784
1785     case XPR_PARENS:
1786       ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints
1787                                     (exprData_getUopNode (data)));
1788       break;
1789     case XPR_INIT:
1790         ret = constraintList_addListFree (ret,
1791                                     exprNode_traversFalseEnsuresConstraints
1792                                     (   exprData_getInitNode (data)));
1793         break;
1794
1795     case XPR_ASSIGN:
1796         ret = constraintList_addListFree (ret,
1797                                     exprNode_traversFalseEnsuresConstraints
1798                                     (exprData_getOpA (data)));
1799
1800        ret = constraintList_addListFree (ret,
1801                                     exprNode_traversFalseEnsuresConstraints
1802                                     (exprData_getOpB (data)));
1803        break;
1804     case XPR_OP:
1805        ret = constraintList_addListFree (ret,
1806                                     exprNode_traversFalseEnsuresConstraints
1807                                     (exprData_getOpA (data)));
1808
1809        ret = constraintList_addListFree (ret,
1810                                     exprNode_traversFalseEnsuresConstraints
1811                                     (exprData_getOpB (data)));
1812        break;
1813     case XPR_SIZEOFT:
1814       break;
1815
1816     case XPR_SIZEOF:
1817
1818        ret = constraintList_addListFree (ret,
1819                                     exprNode_traversFalseEnsuresConstraints
1820                                      (exprData_getSingle (data)));
1821        break;
1822
1823     case XPR_CALL:
1824       ret = constraintList_addListFree (ret,
1825                                      exprNode_traversFalseEnsuresConstraints
1826                                     (exprData_getFcn (data)));
1827       break;
1828
1829     case XPR_RETURN:
1830       ret = constraintList_addListFree (ret,
1831                                     exprNode_traversFalseEnsuresConstraints
1832                                     (exprData_getSingle (data)));
1833       break;
1834
1835     case XPR_NULLRETURN:
1836       break;
1837
1838     case XPR_FACCESS:
1839       ret = constraintList_addListFree (ret,
1840                                         exprNode_traversFalseEnsuresConstraints
1841                                         (exprData_getFieldNode (data)));
1842       break;
1843
1844     case XPR_ARROW:
1845       ret = constraintList_addListFree (ret,
1846                                         exprNode_traversFalseEnsuresConstraints
1847                                         (exprData_getFieldNode (data)));
1848       break;
1849
1850     case XPR_STRINGLITERAL:
1851       break;
1852
1853     case XPR_NUMLIT:
1854       break;
1855     case XPR_POSTOP:
1856
1857            ret = constraintList_addListFree (ret,
1858                                     exprNode_traversFalseEnsuresConstraints
1859                                     (exprData_getUopNode (data)));
1860            break;
1861
1862     case XPR_CAST:
1863
1864       ret = constraintList_addListFree (ret,
1865                                     exprNode_traversFalseEnsuresConstraints
1866                                     (exprData_getCastNode (data)));
1867       break;
1868
1869     default:
1870       break;
1871     }
1872
1873   return ret;
1874 }
1875
1876
1877 /* walk down the tree and get all requires Constraints in each subexpression*/
1878 /*@only@*/ constraintList exprNode_traversRequiresConstraints (exprNode e)
1879 {
1880   exprNode t1;
1881
1882   bool handledExprNode;
1883   exprData data;
1884   constraintList ret;
1885
1886    if (exprNode_handleError (e))
1887      {
1888        ret = constraintList_makeNew();
1889        return ret;
1890      }
1891
1892   ret = constraintList_copy (e->requiresConstraints);
1893   handledExprNode = TRUE;
1894   data = e->edata;
1895
1896   switch (e->kind)
1897     {
1898    case XPR_WHILEPRED:
1899       t1 = exprData_getSingle (data);
1900       ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (t1));
1901       break;
1902
1903     case XPR_FETCH:
1904
1905       ret = constraintList_addListFree (ret,
1906                                     exprNode_traversRequiresConstraints
1907                                     (exprData_getPairA (data)));
1908
1909       ret = constraintList_addListFree (ret,
1910                                     exprNode_traversRequiresConstraints
1911                                     (exprData_getPairB (data)));
1912       break;
1913     case XPR_PREOP:
1914
1915       ret = constraintList_addListFree (ret,
1916                                     exprNode_traversRequiresConstraints
1917                                     (exprData_getUopNode (data)));
1918       break;
1919
1920     case XPR_PARENS:
1921       ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints
1922                                     (exprData_getUopNode (data)));
1923       break;
1924     case XPR_INIT:
1925       ret = constraintList_addListFree (ret,
1926                                         exprNode_traversRequiresConstraints
1927                                         (exprData_getInitNode (data)));
1928         break;
1929
1930     case XPR_ASSIGN:
1931         ret = constraintList_addListFree (ret,
1932                                     exprNode_traversRequiresConstraints
1933                                     (exprData_getOpA (data)));
1934
1935        ret = constraintList_addListFree (ret,
1936                                     exprNode_traversRequiresConstraints
1937                                     (exprData_getOpB (data)));
1938        break;
1939     case XPR_OP:
1940        ret = constraintList_addListFree (ret,
1941                                     exprNode_traversRequiresConstraints
1942                                     (exprData_getOpA (data)));
1943
1944        ret = constraintList_addListFree (ret,
1945                                     exprNode_traversRequiresConstraints
1946                                     (exprData_getOpB (data)));
1947        break;
1948     case XPR_SIZEOFT:
1949       break;
1950
1951     case XPR_SIZEOF:
1952
1953        ret = constraintList_addListFree (ret,
1954                                     exprNode_traversRequiresConstraints
1955                                      (exprData_getSingle (data)));
1956        break;
1957
1958     case XPR_CALL:
1959       ret = constraintList_addListFree (ret,
1960                                      exprNode_traversRequiresConstraints
1961                                     (exprData_getFcn (data)));
1962       break;
1963
1964     case XPR_RETURN:
1965       ret = constraintList_addListFree (ret,
1966                                     exprNode_traversRequiresConstraints
1967                                     (exprData_getSingle (data)));
1968       break;
1969
1970     case XPR_NULLRETURN:
1971       break;
1972
1973     case XPR_FACCESS:
1974       ret = constraintList_addListFree (ret,
1975                                         exprNode_traversRequiresConstraints
1976                                         (exprData_getFieldNode (data)));
1977       break;
1978
1979     case XPR_ARROW:
1980       ret = constraintList_addListFree (ret,
1981                                         exprNode_traversRequiresConstraints
1982                                         (exprData_getFieldNode (data)));
1983       break;
1984
1985     case XPR_STRINGLITERAL:
1986       break;
1987
1988     case XPR_NUMLIT:
1989       break;
1990     case XPR_POSTOP:
1991
1992            ret = constraintList_addListFree (ret,
1993                                     exprNode_traversRequiresConstraints
1994                                     (exprData_getUopNode (data)));
1995            break;
1996
1997     case XPR_CAST:
1998
1999       ret = constraintList_addListFree (ret,
2000                                     exprNode_traversRequiresConstraints
2001                                     (exprData_getCastNode (data)));
2002       break;
2003
2004     default:
2005       break;
2006     }
2007
2008   return ret;
2009 }
2010
2011
2012 /* walk down the tree and get all Ensures Constraints in each subexpression*/
2013 /*@only@*/ constraintList exprNode_traversEnsuresConstraints (exprNode e)
2014 {
2015   exprNode t1;
2016
2017   bool handledExprNode;
2018   exprData data;
2019   constraintList ret;
2020
2021   if (exprNode_handleError (e))
2022     {
2023       ret = constraintList_makeNew();
2024       return ret;
2025     }
2026
2027   ret = constraintList_copy (e->ensuresConstraints);
2028   handledExprNode = TRUE;
2029
2030   data = e->edata;
2031
2032   DPRINTF ((message ("exprnode_traversEnsuresConstraints call for %s with "
2033                      "constraintList of %s",
2034                      exprNode_unparse (e),
2035                      constraintList_unparse(e->ensuresConstraints)
2036                      )
2037             ));
2038
2039
2040   switch (e->kind)
2041     {
2042     case XPR_WHILEPRED:
2043       t1 = exprData_getSingle (data);
2044       ret = constraintList_addListFree (ret,exprNode_traversEnsuresConstraints (t1));
2045       break;
2046
2047     case XPR_FETCH:
2048       ret = constraintList_addListFree (ret,
2049                                         exprNode_traversEnsuresConstraints
2050                                         (exprData_getPairA (data)));
2051
2052       ret = constraintList_addListFree (ret,
2053                                         exprNode_traversEnsuresConstraints
2054                                         (exprData_getPairB (data)));
2055       break;
2056     case XPR_PREOP:
2057       ret = constraintList_addListFree (ret,
2058                                         exprNode_traversEnsuresConstraints
2059                                         (exprData_getUopNode (data)));
2060       break;
2061
2062     case XPR_PARENS:
2063       ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints
2064                                         (exprData_getUopNode (data)));
2065       break;
2066
2067     case XPR_INIT:
2068       ret = constraintList_addListFree (ret,
2069                                         exprNode_traversEnsuresConstraints
2070                                         (exprData_getInitNode (data)));
2071       break;
2072
2073
2074     case XPR_ASSIGN:
2075       ret = constraintList_addListFree (ret,
2076                                         exprNode_traversEnsuresConstraints
2077                                         (exprData_getOpA (data)));
2078
2079       ret = constraintList_addListFree (ret,
2080                                         exprNode_traversEnsuresConstraints
2081                                         (exprData_getOpB (data)));
2082       break;
2083     case XPR_OP:
2084       ret = constraintList_addListFree (ret,
2085                                         exprNode_traversEnsuresConstraints
2086                                         (exprData_getOpA (data)));
2087
2088       ret = constraintList_addListFree (ret,
2089                                         exprNode_traversEnsuresConstraints
2090                                         (exprData_getOpB (data)));
2091       break;
2092     case XPR_SIZEOFT:
2093       break;
2094
2095     case XPR_SIZEOF:
2096       ret = constraintList_addListFree (ret,
2097                                         exprNode_traversEnsuresConstraints
2098                                         (exprData_getSingle (data)));
2099       break;
2100     case XPR_CALL:
2101       ret = constraintList_addListFree (ret,
2102                                         exprNode_traversEnsuresConstraints
2103                                         (exprData_getFcn (data)));
2104       break;
2105     case XPR_RETURN:
2106       ret = constraintList_addListFree (ret,
2107                                         exprNode_traversEnsuresConstraints
2108                                         (exprData_getSingle (data)));
2109       break;
2110     case XPR_NULLRETURN:
2111       break;
2112     case XPR_FACCESS:
2113       ret = constraintList_addListFree (ret,
2114                                         exprNode_traversEnsuresConstraints
2115                                         (exprData_getFieldNode (data)));
2116       break;
2117     case XPR_ARROW:
2118       ret = constraintList_addListFree (ret,
2119                                         exprNode_traversEnsuresConstraints
2120                                         (exprData_getFieldNode (data)));
2121       break;
2122     case XPR_STRINGLITERAL:
2123       break;
2124     case XPR_NUMLIT:
2125       break;
2126     case XPR_POSTOP:
2127       ret = constraintList_addListFree (ret,
2128                                         exprNode_traversEnsuresConstraints
2129                                         (exprData_getUopNode (data)));
2130       break;
2131     case XPR_CAST:
2132       ret = constraintList_addListFree (ret,
2133                                         exprNode_traversEnsuresConstraints
2134                                         (exprData_getCastNode (data)));
2135       break;
2136     default:
2137       break;
2138     }
2139
2140   DPRINTF((message ("exprnode_traversEnsuresConstraints call for %s with "
2141                     "constraintList of  is returning %s",
2142                     exprNode_unparse (e),
2143                     constraintList_unparse(ret))));
2144
2145   return ret;
2146 }
2147
2148 /*drl moved out of constraintResolve.c 07-02-001 */
2149 void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist,
2150                         fileloc sequencePoint)
2151 {
2152
2153   llassert(temp != NULL );
2154
2155   temp->requiresConstraints = constraintList_makeNew();
2156   temp->ensuresConstraints = constraintList_makeNew();
2157   temp->trueEnsuresConstraints = constraintList_makeNew();
2158   temp->falseEnsuresConstraints = constraintList_makeNew();
2159
2160   exprNodeList_elements (arglist, el)
2161     {
2162       constraintList temp2;
2163
2164       llassert(exprNode_isDefined(el) );
2165
2166       exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint);
2167       temp2 = el->requiresConstraints;
2168       el->requiresConstraints = exprNode_traversRequiresConstraints(el);
2169       constraintList_free(temp2);
2170
2171       temp2 = el->ensuresConstraints;
2172       el->ensuresConstraints  = exprNode_traversEnsuresConstraints(el);
2173       constraintList_free(temp2);
2174
2175       temp->requiresConstraints = constraintList_addList(temp->requiresConstraints,
2176                                                             el->requiresConstraints);
2177
2178       temp->ensuresConstraints = constraintList_addList(temp->ensuresConstraints,
2179                                                            el->ensuresConstraints);
2180     }
2181   end_exprNodeList_elements;
2182
2183 }
2184
2185 /*drl moved out of constraintResolve.c 07-03-001 */
2186 constraintList exprNode_getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall)
2187 {
2188   constraintList postconditions;
2189   uentry temp;
2190   DPRINTF((message ("Got call that %s (%s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (arglist))));
2191
2192   temp = exprNode_getUentry (fcn);
2193
2194   postconditions = uentry_getFcnPostconditions (temp);
2195
2196   if (constraintList_isDefined (postconditions))
2197     {
2198       postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist);
2199       postconditions = constraintList_doFixResult (postconditions, fcnCall);
2200     }
2201   else
2202     {
2203       postconditions = constraintList_makeNew();
2204     }
2205
2206   return postconditions;
2207 }
2208
2209 /*
2210 comment this out for now
2211 we'll include it in a production release when its stable...
2212
2213   void findStructs (exprNodeList arglist)
2214 {
2215
2216   ctype ct, rt;
2217
2218   DPRINTF((
2219            message("doing findStructs: %s", exprNodeList_unparse(arglist))
2220           ));
2221
2222
2223   exprNodeList_elements(arglist, expr)
2224     {
2225       ct = exprNode_getType(expr);
2226
2227       rt =  ctype_realType (ct);
2228
2229       if (ctype_isStruct (rt))
2230         TPRINTF((message("Found structure %s", exprNode_unparse(expr))
2231                  ));
2232       if (hasInvariants(ct))
2233         {
2234           constraintList invars;
2235
2236           invars = getInvariants(ct);
2237
2238
2239           TPRINTF((message ("findStructs has invariants %s ", constraintList_unparse (invars))
2240                    ));
2241
2242           invars = constraintList_doSRefFixStructConstraint(invars, exprNode_getSref(expr), ct);
2243
2244
2245           TPRINTF((message ("findStructs finded invariants to be %s ", constraintList_unparse (invars))
2246                    ));
2247         }
2248     }
2249   end_exprNodeList_elements;
2250 }
2251
2252 */
2253
2254 /*drl moved out of constraintResolve.c 07-02-001 */
2255 constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist)
2256 {
2257   constraintList preconditions;
2258   uentry temp;
2259   DPRINTF((message ("Got call that %s (%s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (arglist))));
2260
2261   temp = exprNode_getUentry (fcn);
2262
2263   preconditions = uentry_getFcnPreconditions (temp);
2264
2265   if (constraintList_isDefined(preconditions))
2266     {
2267       preconditions = constraintList_togglePost (preconditions);
2268       preconditions = constraintList_preserveCallInfo(preconditions, fcn);
2269       preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist);
2270     }
2271   else
2272     {
2273       if (constraintList_isUndefined(preconditions))
2274         preconditions = constraintList_makeNew();
2275     }
2276
2277   if (context_getFlag (FLG_IMPLICTCONSTRAINT) )
2278     {
2279
2280       /*
2281       uentryList_elements (arglist, el)
2282         {
2283           sRef s;
2284           TPRINTF((message("setImplictfcnConstraints doing: %s", uentry_unparse(el) ) ));
2285
2286           s = uentry_getSref(el);
2287           if (sRef_isReference (s) )
2288             {
2289               TPRINTF((message ("%s is a pointer", sRef_unparse(s) ) ));
2290             }
2291           else
2292             {
2293               TPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) ));
2294             }
2295           //drl 4/26/01
2296           //chagned this from MaxSet(s) == 0 to MaxSet(s) >= 0
2297           c = constraint_makeSRefWriteSafeInt (s, 0);
2298
2299           implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c);
2300
2301           //drl 10/23/2002 added support for out
2302           if (!uentry_isOut(el) )
2303             {
2304               c = constraint_makeSRefReadSafeInt (s, 0);
2305               implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c);
2306             }
2307
2308
2309         }
2310       */
2311     }
2312
2313   DPRINTF ((message("Done checkCall\n")));
2314   DPRINTF ((message("Returning list %q ", constraintList_unparseDetailed(preconditions))));
2315
2316   /*
2317     drl we're going to comment this out for now
2318     we'll include it if we're sure it's working
2319
2320     findStructs(arglist);
2321   */
2322
2323   return preconditions;
2324 }
2325
2326 /*drl added this function 10.29.001
2327   takes an exprNode of the form const + const
2328   and sets the value
2329 */
2330 /*drl
2331   I'm a bit nervous about modifying the exprNode
2332   but this is the easy way to do this
2333   If I have time I'd like to cause the exprNode to get created correctly in the first place */
2334 void exprNode_findValue(exprNode e)
2335 {
2336   exprData data;
2337
2338   exprNode t1, t2;
2339   lltok tok;
2340
2341   llassert(exprNode_isDefined(e) );
2342
2343   data = e->edata;
2344
2345   if (exprNode_hasValue(e))
2346     return;
2347
2348   if (e->kind == XPR_OP)
2349     {
2350       t1 = exprData_getOpA (data);
2351      t2 = exprData_getOpB (data);
2352      tok = exprData_getOpTok (data);
2353
2354      exprNode_findValue(t1);
2355      exprNode_findValue(t2);
2356
2357      if (!(exprNode_knownIntValue(t1) && (exprNode_knownIntValue(t2))))
2358        return;
2359
2360      if (lltok_isPlus_Op (tok))
2361        {
2362          long v1, v2;
2363
2364          v1 = exprNode_getLongValue(t1);
2365          v2 = exprNode_getLongValue(t2);
2366
2367          if (multiVal_isDefined(e->val))
2368            multiVal_free (e->val);
2369
2370          e->val = multiVal_makeInt (v1 + v2);
2371        }
2372
2373      if (lltok_isMinus_Op (tok))
2374        {
2375          long v1, v2;
2376
2377          v1 = exprNode_getLongValue(t1);
2378          v2 = exprNode_getLongValue(t2);
2379
2380          if (multiVal_isDefined(e->val))
2381            {
2382              multiVal_free (e->val);
2383            }
2384
2385          e->val = multiVal_makeInt (v1 - v2);
2386        }
2387
2388      /*drl I should really do * and / at some point */
2389
2390     }
2391
2392 }
2393