src/constraintGeneration.c

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