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