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