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