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
 157   if (exprNode_isError(e))
 158     {
 159       return;
 160     }
 161
 162   /*e->requiresConstraints = constraintList_makeNew();
 163     e->ensuresConstraints  = constraintList_makeNew(); */
 164
 165   DPRINTF(("expNode_stmt: STMT:"));
 166
 167   DPRINTF ((message("exprNode_stmt: STMT: %s ",  exprNode_unparse(e) ) ) );
 168
 169   if (e->kind == XPR_INIT)
 170     {
 171       constraintList tempList;
 172       DPRINTF (("Init"));
 173       DPRINTF ((message ("%s ", exprNode_unparse (e))));
 174       loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
 175       exprNode_exprTraverse (e, FALSE, FALSE, loc);
 176       fileloc_free(loc);
 177
 178       tempList = e->requiresConstraints;
 179       e->requiresConstraints = exprNode_traversRequiresConstraints(e);
 180       constraintList_free(tempList);
 181
 182       tempList = e->ensuresConstraints;
 183       e->ensuresConstraints  = exprNode_traversEnsuresConstraints(e);
 184       constraintList_free(tempList);
 185       return;
 186     }
 187
 188   /*drl 2/13/002 patched bug so return statement will be checked*/
 189   /*return is a stmt not not expression ...*/
 190   if (e->kind == XPR_RETURN)
 191     {
 192       constraintList tempList;
 193
 194       loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
 195
 196       exprNode_exprTraverse (exprData_getSingle (e->edata), FALSE, TRUE, loc);
 197       fileloc_free(loc);
 198
 199       tempList = e->requiresConstraints;
 200       e->requiresConstraints = exprNode_traversRequiresConstraints(e);
 201       constraintList_free(tempList);
 202     }
 203
 204   if (e->kind != XPR_STMT)
 205     {
 206
 207       DPRINTF (("Not Stmt"));
 208       DPRINTF ((message ("%s ", exprNode_unparse (e))));
 209
 210       if (exprNode_isMultiStatement (e))
 211         {
 212           exprNode_multiStatement (e); /* evans 2001-08-21: spurious return removed */
 213         }
 214       else
 215         {
 216           loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
 217
 218           exprNode_exprTraverse (e, FALSE, TRUE, loc);
 219           fileloc_free(loc);
 220
 221           }
 222           return;
 223     }
 224
 225   DPRINTF (("Stmt"));
 226   DPRINTF ((message ("%s ", exprNode_unparse (e))));
 227
 228   snode = exprData_getUopNode (e->edata);
 229
 230   /* could be stmt involving multiple statements:
 231      i.e. if, while for ect.
 232   */
 233
 234   if (exprNode_isMultiStatement (snode))
 235     {
 236       exprNode_multiStatement (snode);
 237       (void) exprNode_copyConstraints (e, snode);
 238       return;
 239     }
 240
 241   loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
 242   exprNode_exprTraverse (snode, FALSE, FALSE, loc);
 243
 244   fileloc_free(loc);
 245
 246   constraintList_free (e->requiresConstraints);
 247   e->requiresConstraints = exprNode_traversRequiresConstraints(snode);
 248
 249   constraintList_free (e->ensuresConstraints);
 250   e->ensuresConstraints  = exprNode_traversEnsuresConstraints(snode);
 251
 252   DPRINTF ((message ("smtlist constraints are: pre: %s \n and \t post %s\n",
 253                       constraintList_print(e->requiresConstraints),
 254                       constraintList_print(e->ensuresConstraints))));
 255
 256   return;
 257 }
 258
 259 static void exprNode_stmtList  (/*@dependent@*/ exprNode e)
 260 {
 261   exprNode stmt1, stmt2;
 262   if (exprNode_isError (e))
 263     {
 264       return;
 265     }
 266
 267   /*
 268     Handle case of stmtList with only one statement:
 269     The parse tree stores this as stmt instead of stmtList
 270   */
 271
 272   if (e->kind != XPR_STMTLIST)
 273     {
 274       exprNode_stmt(e);
 275       return;
 276     }
 277   llassert (e->kind == XPR_STMTLIST);
 278   DPRINTF(("exprNode_stmtList STMTLIST:"));
 279   DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e))));
 280   stmt1 = exprData_getPairA (e->edata);
 281   stmt2 = exprData_getPairB (e->edata);
 282
 283
 284   DPRINTF(("exprNode_stmtlist       "));
 285   DPRINTF ((message("XW%s    |        %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2))));
 286
 287   exprNode_stmt (stmt1);
 288   DPRINTF(("\nstmt after stmtList call "));
 289
 290   exprNode_stmt (stmt2);
 291   exprNode_mergeResolve (e, stmt1, stmt2);
 292
 293   DPRINTF ((message ("smtlist constraints are: pre: %s \n and \t post %s\n",
 294                       constraintList_print(e->requiresConstraints),
 295                       constraintList_print(e->ensuresConstraints))));
 296   return;
 297 }
 298
 299 static exprNode doIf (/*@returned@*/  exprNode e, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body)
 300 {
 301   constraintList temp;
 302
 303   DPRINTF ((message ("doIf: %s ", exprNode_unparse(e))));
 304
 305   llassert(exprNode_isDefined(test));
 306   llassert (exprNode_isDefined (e));
 307   llassert (exprNode_isDefined (body));
 308
 309
 310       DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints))));
 311
 312       DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints))));
 313
 314       DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->trueEnsuresConstraints))));
 315
 316       DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->falseEnsuresConstraints))));
 317
 318
 319
 320       DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->ensuresConstraints))));
 321
 322       DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->ensuresConstraints))));
 323
 324       DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->trueEnsuresConstraints))));
 325
 326       DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->falseEnsuresConstraints))));
 327
 328
 329
 330       temp = test->trueEnsuresConstraints;
 331       test->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(test);
 332       constraintList_free(temp);
 333
 334   temp = test->ensuresConstraints;
 335   test->ensuresConstraints = exprNode_traversEnsuresConstraints (test);
 336   constraintList_free(temp);
 337
 338   temp = test->requiresConstraints;
 339   test->requiresConstraints = exprNode_traversRequiresConstraints (test);
 340   constraintList_free(temp);
 341
 342
 343   test->trueEnsuresConstraints = constraintList_substituteFreeTarget(test->trueEnsuresConstraints, test->ensuresConstraints);
 344
 345   DPRINTF ((message ("doIf: test ensures %s ", constraintList_print(test->ensuresConstraints))));
 346
 347   DPRINTF ((message ("doIf: test true ensures %s ", constraintList_print(test->trueEnsuresConstraints))));
 348
 349   constraintList_free(e->requiresConstraints);
 350
 351
 352   e->requiresConstraints = constraintList_reflectChanges(body->requiresConstraints, test->trueEnsuresConstraints);
 353
 354   e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints,
 355                                            test->ensuresConstraints);
 356   temp = e->requiresConstraints;
 357   e->requiresConstraints = constraintList_mergeRequires (e->requiresConstraints, test->requiresConstraints);
 358   constraintList_free(temp);
 359
 360
 361   /* drl possible problem : warning bad */
 362   constraintList_free(e->ensuresConstraints);
 363   e->ensuresConstraints = constraintList_copy (test->ensuresConstraints);
 364
 365   if (exprNode_mayEscape (body))
 366     {
 367       DPRINTF ((message("doIf: the if statement body %s returns or exits", exprNode_unparse(body))));
 368       e->ensuresConstraints = constraintList_mergeEnsuresFreeFirst (e->ensuresConstraints,
 369                                                         test->falseEnsuresConstraints);
 370     }
 371
 372   DPRINTF ((message ("doIf: if requiers %s ", constraintList_print(e->requiresConstraints))));
 373
 374   return e;
 375 }
 376
 377 /*drl added 3/4/2001
 378   Also used for condition i.e. ?: operation
 379
 380   Precondition
 381   This function assumes that p, trueBranch, falseBranch have have all been traversed
 382   for constraints i.e. we assume that exprNode_traversEnsuresConstraints,
 383   exprNode_traversRequiresConstraints,  exprNode_traversTrueEnsuresConstraints,
 384   exprNode_traversFalseEnsuresConstraints have all been run
 385 */
 386
 387 static exprNode doIfElse (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode p, /*@dependent@*/ exprNode trueBranch, /*@dependent@*/ exprNode falseBranch)
 388 {
 389   constraintList c1, cons, t, t2, f, f2;
 390
 391   llassert (exprNode_isDefined (e));
 392   llassert (exprNode_isDefined (p));
 393   llassert (exprNode_isDefined (trueBranch));
 394   llassert (exprNode_isDefined (falseBranch));
 395   DPRINTF ((message ("doIfElse: %s ", exprNode_unparse(e))));
 396
 397   /* do requires clauses */
 398   c1 = constraintList_copy (p->ensuresConstraints);
 399
 400   t = constraintList_reflectChanges(trueBranch->requiresConstraints, p->trueEnsuresConstraints);
 401   t = constraintList_reflectChangesFreePre (t, p->ensuresConstraints);
 402
 403   cons = constraintList_reflectChanges(falseBranch->requiresConstraints, p->falseEnsuresConstraints);
 404   cons  = constraintList_reflectChangesFreePre (cons, c1);
 405
 406   constraintList_free (e->requiresConstraints);
 407   e->requiresConstraints = constraintList_mergeRequiresFreeFirst (t, cons);
 408   e->requiresConstraints = constraintList_mergeRequiresFreeFirst (e->requiresConstraints, p->requiresConstraints);
 409
 410   /* do ensures clauses
 411      find the  the ensures lists for each subbranch
 412   */
 413
 414   t = constraintList_mergeEnsures (p->trueEnsuresConstraints, trueBranch->ensuresConstraints);
 415   t2 = t;
 416   t = constraintList_mergeEnsures (p->ensuresConstraints, t);
 417   constraintList_free(t2);
 418
 419   f = constraintList_mergeEnsures (p->falseEnsuresConstraints, falseBranch->ensuresConstraints);
 420   f2 = f;
 421   f = constraintList_mergeEnsures (p->ensuresConstraints, f);
 422   constraintList_free(f2);
 423
 424   /* find ensures for whole if/else statement */
 425
 426   constraintList_free(e->ensuresConstraints);
 427
 428   e->ensuresConstraints = constraintList_logicalOr (t, f);
 429
 430   constraintList_free(t);
 431   constraintList_free(f);
 432   constraintList_free(cons);
 433   constraintList_free(c1);
 434
 435   DPRINTF ((message ("doIfElse: if requires %q ", constraintList_print(e->requiresConstraints))));
 436   DPRINTF ((message ("doIfElse: if ensures %q ", constraintList_print(e->ensuresConstraints))));
 437
 438   return e;
 439 }
 440
 441 static exprNode doWhile (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body)
 442 {
 443   DPRINTF ((message ("doWhile: %s ", exprNode_unparse(e))));
 444   return doIf (e, test, body);
 445 }
 446
 447 /*@only@*/ constraintList constraintList_makeFixedArrayConstraints (/*@observer@*/ sRefSet s)
 448 {
 449   constraintList ret;
 450   constraint con;
 451   ret = constraintList_makeNew();
 452
 453   sRefSet_elements (s, el)
 454     {
 455       if (sRef_isFixedArray(el))
 456         {
 457           size_t size;
 458           DPRINTF((message("%s is a fixed array",
 459                             sRef_unparse(el))));
 460           size = sRef_getArraySize(el);
 461           DPRINTF((message("%s is a fixed array with size %d",
 462                             sRef_unparse(el), (int)size)));
 463           con = constraint_makeSRefSetBufferSize (el, (size - 1));
 464           ret = constraintList_add(ret, con);
 465         }
 466       else
 467         {
 468           DPRINTF((message("%s is not a fixed array",
 469                             sRef_unparse(el))));
 470
 471
 472           if (sRef_isExternallyVisible (el))
 473             {
 474               /*
 475                 DPRINTF((message("%s is externally visible",
 476                 sRef_unparse(el))));
 477                 con = constraint_makeSRefWriteSafeInt(el, 0);
 478                 ret = constraintList_add(ret, con);
 479
 480                 con = constraint_makeSRefReadSafeInt(el, 0);
 481
 482                 ret = constraintList_add(ret, con);
 483               */
 484             }
 485         }
 486     }
 487   end_sRefSet_elements ;
 488
 489   DPRINTF((message("constraintList_makeFixedArrayConstraints returning %s",
 490                     constraintList_print(ret))));
 491   return ret;
 492 }
 493
 494 # if 0
 495 exprNode makeDataTypeConstraints (/*@returned@*/ exprNode e)
 496 {
 497   constraintList c;
 498   DPRINTF(("makeDataTypeConstraints"));
 499
 500   c = constraintList_makeFixedArrayConstraints (e->uses);
 501
 502   e->ensuresConstraints = constraintList_addListFree (e->ensuresConstraints, c);
 503
 504  return e;
 505 }
 506 # endif
 507
 508 static void doFor (/*@dependent@*/ exprNode e, /*@dependent@*/ exprNode forPred, /*@dependent@*/ exprNode forBody)
 509 {
 510   exprNode init, test, inc;
 511   /* merge the constraints: modle as if statement */
 512
 513   /* init
 514      if (test)
 515      for body
 516      inc        */
 517
 518   llassert (exprNode_isDefined (e));
 519   llassert (exprNode_isDefined (forPred));
 520   llassert (exprNode_isDefined (forBody));
 521
 522   init = exprData_getTripleInit (forPred->edata);
 523   test = exprData_getTripleTest (forPred->edata);
 524   inc = exprData_getTripleInc (forPred->edata);
 525
 526   if (((exprNode_isError (test) /*|| (exprNode_isError(init))*/) || (exprNode_isError (inc))))
 527     {
 528       DPRINTF ((message ("strange for statement:%s, ignoring it", exprNode_unparse(e))));
 529       return;
 530     }
 531
 532   exprNode_forLoopHeuristics(e, forPred, forBody);
 533
 534   constraintList_free(e->requiresConstraints);
 535   e->requiresConstraints = constraintList_reflectChanges(forBody->requiresConstraints, test->ensuresConstraints);
 536   e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, test->trueEnsuresConstraints);
 537   e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, forPred->ensuresConstraints);
 538
 539   if (!forBody->canBreak)
 540     {
 541       e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints, constraintList_copy(forPred->ensuresConstraints));
 542       e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints,constraintList_copy(test->falseEnsuresConstraints));
 543     }
 544   else
 545     {
 546       DPRINTF(("Can break"));
 547     }
 548 }
 549
 550 /*@i2323*/
 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       /* drl -04-06-2002 fixed to handle unary + */
1400       else if (lltok_isPlus_Op (tok) )
1401         {
1402           break;
1403         }
1404       else if ( lltok_isExcl_Op (tok) )
1405         {
1406           break;
1407         }
1408       else if (lltok_isTilde_Op (tok))
1409         {
1410           break;
1411         }
1412       else
1413         {
1414           llcontbug (message("Unsupported preop in %s", exprNode_unparse(e)));
1415           BADEXIT;
1416         }
1417       break;
1418
1419     case XPR_POSTOP:
1420       exprNode_exprTraverse (exprData_getUopNode (data), TRUE,
1421                              definaterv, sequencePoint);
1422
1423       if (lltok_isInc_Op (exprData_getUopTok (data)))
1424         {
1425           DPRINTF(("doing ++"));
1426           t1 = exprData_getUopNode (data);
1427           cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint);
1428           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1429         }
1430        if (lltok_isDec_Op (exprData_getUopTok (data)))
1431         {
1432           DPRINTF(("doing --"));
1433           t1 = exprData_getUopNode (data);
1434           cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint);
1435           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1436         }
1437       break;
1438     case XPR_CAST:
1439       {
1440         t2 =  exprData_getCastNode (data);
1441         DPRINTF ((message ("Examining cast (%q)%s",
1442                             qtype_unparse (exprData_getCastType (data)),
1443                             exprNode_unparse (t2))
1444                   ));
1445         exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint);
1446       }
1447       break;
1448
1449     case XPR_COND:
1450       {
1451         exprNode pred, trueBranch, falseBranch;
1452         llassert(FALSE);
1453         pred = exprData_getTriplePred (data);
1454         trueBranch = exprData_getTripleTrue (data);
1455         falseBranch = exprData_getTripleFalse (data);
1456
1457         llassert (exprNode_isDefined (pred));
1458         llassert (exprNode_isDefined (trueBranch));
1459         llassert (exprNode_isDefined (falseBranch));
1460
1461         exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint);
1462
1463         temp = pred->ensuresConstraints;
1464         pred->ensuresConstraints = exprNode_traversEnsuresConstraints(pred);
1465         constraintList_free(temp);
1466
1467         temp = pred->requiresConstraints;
1468         pred->requiresConstraints = exprNode_traversRequiresConstraints(pred);
1469         constraintList_free(temp);
1470
1471         temp = pred->trueEnsuresConstraints;
1472         pred->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(pred);
1473         constraintList_free(temp);
1474
1475         temp = pred->falseEnsuresConstraints;
1476         pred->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(pred);
1477         constraintList_free(temp);
1478
1479         exprNode_exprTraverse (trueBranch, FALSE, TRUE, sequencePoint);
1480
1481         temp = trueBranch->ensuresConstraints;
1482         trueBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(trueBranch);
1483         constraintList_free(temp);
1484
1485         temp = trueBranch->requiresConstraints;
1486         trueBranch->requiresConstraints = exprNode_traversRequiresConstraints(trueBranch);
1487         constraintList_free(temp);
1488
1489
1490         temp =       trueBranch->trueEnsuresConstraints;
1491         trueBranch->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(trueBranch);
1492         constraintList_free(temp);
1493
1494         temp =       trueBranch->falseEnsuresConstraints;
1495         trueBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(trueBranch);
1496         constraintList_free(temp);
1497
1498         exprNode_exprTraverse (falseBranch, FALSE, TRUE, sequencePoint);
1499
1500         temp = falseBranch->ensuresConstraints;
1501         falseBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(falseBranch);
1502         constraintList_free(temp);
1503
1504
1505         temp = falseBranch->requiresConstraints;
1506         falseBranch->requiresConstraints = exprNode_traversRequiresConstraints(falseBranch);
1507         constraintList_free(temp);
1508
1509         temp = falseBranch->trueEnsuresConstraints;
1510         falseBranch->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(falseBranch);
1511         constraintList_free(temp);
1512
1513         temp = falseBranch->falseEnsuresConstraints;
1514         falseBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(falseBranch);
1515         constraintList_free(temp);
1516
1517         /* if pred is true e equals true otherwise pred equals false */
1518
1519         cons =  constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
1520         trueBranch->ensuresConstraints = constraintList_add(trueBranch->ensuresConstraints, cons);
1521
1522         cons =  constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
1523         falseBranch->ensuresConstraints = constraintList_add(falseBranch->ensuresConstraints, cons);
1524
1525         e = doIfElse (e, pred, trueBranch, falseBranch);
1526       }
1527       break;
1528     case XPR_COMMA:
1529       llassert(FALSE);
1530       t1 = exprData_getPairA (data);
1531       t2 = exprData_getPairB (data);
1532     /* we essiantially treat this like expr1; expr2
1533      of course sequencePoint isn't adjusted so this isn't completely accurate
1534     problems../  */
1535       exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint);
1536       exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint);
1537       exprNode_mergeResolve (e, t1, t2);
1538       break;
1539
1540     default:
1541       handledExprNode = FALSE;
1542     }
1543
1544   e->requiresConstraints =  constraintList_preserveOrig (e->requiresConstraints);
1545   e->ensuresConstraints  =  constraintList_preserveOrig (e->ensuresConstraints);
1546   e->requiresConstraints = constraintList_addGeneratingExpr (e->requiresConstraints, e);
1547
1548   e->ensuresConstraints  = constraintList_addGeneratingExpr (e->ensuresConstraints, e);
1549
1550
1551   e->requiresConstraints = constraintList_removeSurpressed(e->requiresConstraints);
1552
1553   DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints))));
1554
1555   DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints))));
1556
1557   DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->trueEnsuresConstraints))));
1558
1559   DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->falseEnsuresConstraints))));
1560
1561   return;
1562 }
1563
1564
1565 constraintList exprNode_traversTrueEnsuresConstraints (exprNode e)
1566 {
1567   exprNode t1;
1568
1569   bool handledExprNode;
1570   exprData data;
1571   constraintList ret;
1572
1573   if (exprNode_handleError (e))
1574     {
1575       ret = constraintList_makeNew();
1576       return ret;
1577     }
1578
1579   ret = constraintList_copy (e->trueEnsuresConstraints);
1580
1581   handledExprNode = TRUE;
1582
1583   data = e->edata;
1584
1585   switch (e->kind)
1586     {
1587     case XPR_WHILEPRED:
1588       t1 = exprData_getSingle (data);
1589       ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (t1));
1590       break;
1591
1592     case XPR_FETCH:
1593
1594       ret = constraintList_addListFree (ret,
1595                                     exprNode_traversTrueEnsuresConstraints
1596                                     (exprData_getPairA (data)));
1597
1598       ret = constraintList_addListFree (ret,
1599                                     exprNode_traversTrueEnsuresConstraints
1600                                     (exprData_getPairB (data)));
1601       break;
1602     case XPR_PREOP:
1603
1604       ret = constraintList_addListFree (ret,
1605                                     exprNode_traversTrueEnsuresConstraints
1606                                     (exprData_getUopNode (data)));
1607       break;
1608
1609     case XPR_PARENS:
1610       ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints
1611                                     (exprData_getUopNode (data)));
1612       break;
1613
1614     case XPR_INIT:
1615       ret = constraintList_addListFree (ret,
1616                                         exprNode_traversTrueEnsuresConstraints
1617                                         (exprData_getInitNode (data)));
1618         break;
1619
1620
1621     case XPR_ASSIGN:
1622         ret = constraintList_addListFree (ret,
1623                                     exprNode_traversTrueEnsuresConstraints
1624                                     (exprData_getOpA (data)));
1625
1626        ret = constraintList_addListFree (ret,
1627                                     exprNode_traversTrueEnsuresConstraints
1628                                     (exprData_getOpB (data)));
1629        break;
1630     case XPR_OP:
1631        ret = constraintList_addListFree (ret,
1632                                     exprNode_traversTrueEnsuresConstraints
1633                                     (exprData_getOpA (data)));
1634
1635        ret = constraintList_addListFree (ret,
1636                                     exprNode_traversTrueEnsuresConstraints
1637                                     (exprData_getOpB (data)));
1638        break;
1639     case XPR_SIZEOFT:
1640       break;
1641
1642     case XPR_SIZEOF:
1643
1644        ret = constraintList_addListFree (ret,
1645                                          exprNode_traversTrueEnsuresConstraints
1646                                          (exprData_getSingle (data)));
1647        break;
1648
1649     case XPR_CALL:
1650       ret = constraintList_addListFree (ret,
1651                                      exprNode_traversTrueEnsuresConstraints
1652                                     (exprData_getFcn (data)));
1653       /*@i11*/  /* exprNodeList_unparse (exprData_getArgs (data)); */
1654       break;
1655
1656     case XPR_RETURN:
1657       ret = constraintList_addListFree (ret,
1658                                     exprNode_traversTrueEnsuresConstraints
1659                                     (exprData_getSingle (data)));
1660       break;
1661
1662     case XPR_NULLRETURN:
1663       break;
1664
1665     case XPR_FACCESS:
1666       ret = constraintList_addListFree (ret,
1667                                         exprNode_traversTrueEnsuresConstraints
1668                                         (exprData_getFieldNode (data)));
1669       break;
1670
1671     case XPR_ARROW:
1672       ret = constraintList_addListFree (ret,
1673                                         exprNode_traversTrueEnsuresConstraints
1674                                         (exprData_getFieldNode (data)));
1675       break;
1676
1677     case XPR_STRINGLITERAL:
1678       break;
1679
1680     case XPR_NUMLIT:
1681       break;
1682     case XPR_POSTOP:
1683
1684            ret = constraintList_addListFree (ret,
1685                                     exprNode_traversTrueEnsuresConstraints
1686                                     (exprData_getUopNode (data)));
1687            break;
1688
1689     case XPR_CAST:
1690
1691       ret = constraintList_addListFree (ret,
1692                                     exprNode_traversTrueEnsuresConstraints
1693                                     (exprData_getCastNode (data)));
1694       break;
1695
1696     default:
1697       break;
1698     }
1699
1700   return ret;
1701 }
1702
1703 constraintList exprNode_traversFalseEnsuresConstraints (exprNode e)
1704 {
1705   exprNode t1;
1706   bool handledExprNode;
1707   exprData data;
1708   constraintList ret;
1709
1710   if (exprNode_handleError (e))
1711     {
1712       ret = constraintList_makeNew();
1713       return ret;
1714     }
1715
1716   ret = constraintList_copy (e->falseEnsuresConstraints);
1717   handledExprNode = TRUE;
1718   data = e->edata;
1719
1720   switch (e->kind)
1721     {
1722    case XPR_WHILEPRED:
1723       t1 = exprData_getSingle (data);
1724       ret = constraintList_addListFree (ret,exprNode_traversFalseEnsuresConstraints (t1));
1725       break;
1726
1727     case XPR_FETCH:
1728
1729       ret = constraintList_addListFree (ret,
1730                                     exprNode_traversFalseEnsuresConstraints
1731                                     (exprData_getPairA (data)));
1732
1733       ret = constraintList_addListFree (ret,
1734                                     exprNode_traversFalseEnsuresConstraints
1735                                     (exprData_getPairB (data)));
1736       break;
1737     case XPR_PREOP:
1738
1739       ret = constraintList_addListFree (ret,
1740                                     exprNode_traversFalseEnsuresConstraints
1741                                     (exprData_getUopNode (data)));
1742       break;
1743
1744     case XPR_PARENS:
1745       ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints
1746                                     (exprData_getUopNode (data)));
1747       break;
1748     case XPR_INIT:
1749         ret = constraintList_addListFree (ret,
1750                                     exprNode_traversFalseEnsuresConstraints
1751                                     (   exprData_getInitNode (data)));
1752         break;
1753
1754     case XPR_ASSIGN:
1755         ret = constraintList_addListFree (ret,
1756                                     exprNode_traversFalseEnsuresConstraints
1757                                     (exprData_getOpA (data)));
1758
1759        ret = constraintList_addListFree (ret,
1760                                     exprNode_traversFalseEnsuresConstraints
1761                                     (exprData_getOpB (data)));
1762        break;
1763     case XPR_OP:
1764        ret = constraintList_addListFree (ret,
1765                                     exprNode_traversFalseEnsuresConstraints
1766                                     (exprData_getOpA (data)));
1767
1768        ret = constraintList_addListFree (ret,
1769                                     exprNode_traversFalseEnsuresConstraints
1770                                     (exprData_getOpB (data)));
1771        break;
1772     case XPR_SIZEOFT:
1773       break;
1774
1775     case XPR_SIZEOF:
1776
1777        ret = constraintList_addListFree (ret,
1778                                     exprNode_traversFalseEnsuresConstraints
1779                                      (exprData_getSingle (data)));
1780        break;
1781
1782     case XPR_CALL:
1783       ret = constraintList_addListFree (ret,
1784                                      exprNode_traversFalseEnsuresConstraints
1785                                     (exprData_getFcn (data)));
1786       /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */
1787       break;
1788
1789     case XPR_RETURN:
1790       ret = constraintList_addListFree (ret,
1791                                     exprNode_traversFalseEnsuresConstraints
1792                                     (exprData_getSingle (data)));
1793       break;
1794
1795     case XPR_NULLRETURN:
1796       break;
1797
1798     case XPR_FACCESS:
1799       ret = constraintList_addListFree (ret,
1800                                         exprNode_traversFalseEnsuresConstraints
1801                                         (exprData_getFieldNode (data)));
1802       break;
1803
1804     case XPR_ARROW:
1805       ret = constraintList_addListFree (ret,
1806                                         exprNode_traversFalseEnsuresConstraints
1807                                         (exprData_getFieldNode (data)));
1808       break;
1809
1810     case XPR_STRINGLITERAL:
1811       break;
1812
1813     case XPR_NUMLIT:
1814       break;
1815     case XPR_POSTOP:
1816
1817            ret = constraintList_addListFree (ret,
1818                                     exprNode_traversFalseEnsuresConstraints
1819                                     (exprData_getUopNode (data)));
1820            break;
1821
1822     case XPR_CAST:
1823
1824       ret = constraintList_addListFree (ret,
1825                                     exprNode_traversFalseEnsuresConstraints
1826                                     (exprData_getCastNode (data)));
1827       break;
1828
1829     default:
1830       break;
1831     }
1832
1833   return ret;
1834 }
1835
1836
1837 /* walk down the tree and get all requires Constraints in each subexpression*/
1838 /*@only@*/ constraintList exprNode_traversRequiresConstraints (exprNode e)
1839 {
1840   exprNode t1;
1841
1842   bool handledExprNode;
1843   exprData data;
1844   constraintList ret;
1845
1846    if (exprNode_handleError (e))
1847      {
1848        ret = constraintList_makeNew();
1849        return ret;
1850      }
1851
1852   ret = constraintList_copy (e->requiresConstraints);
1853   handledExprNode = TRUE;
1854   data = e->edata;
1855
1856   switch (e->kind)
1857     {
1858    case XPR_WHILEPRED:
1859       t1 = exprData_getSingle (data);
1860       ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (t1));
1861       break;
1862
1863     case XPR_FETCH:
1864
1865       ret = constraintList_addListFree (ret,
1866                                     exprNode_traversRequiresConstraints
1867                                     (exprData_getPairA (data)));
1868
1869       ret = constraintList_addListFree (ret,
1870                                     exprNode_traversRequiresConstraints
1871                                     (exprData_getPairB (data)));
1872       break;
1873     case XPR_PREOP:
1874
1875       ret = constraintList_addListFree (ret,
1876                                     exprNode_traversRequiresConstraints
1877                                     (exprData_getUopNode (data)));
1878       break;
1879
1880     case XPR_PARENS:
1881       ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints
1882                                     (exprData_getUopNode (data)));
1883       break;
1884     case XPR_INIT:
1885       ret = constraintList_addListFree (ret,
1886                                         exprNode_traversRequiresConstraints
1887                                         (exprData_getInitNode (data)));
1888         break;
1889
1890     case XPR_ASSIGN:
1891         ret = constraintList_addListFree (ret,
1892                                     exprNode_traversRequiresConstraints
1893                                     (exprData_getOpA (data)));
1894
1895        ret = constraintList_addListFree (ret,
1896                                     exprNode_traversRequiresConstraints
1897                                     (exprData_getOpB (data)));
1898        break;
1899     case XPR_OP:
1900        ret = constraintList_addListFree (ret,
1901                                     exprNode_traversRequiresConstraints
1902                                     (exprData_getOpA (data)));
1903
1904        ret = constraintList_addListFree (ret,
1905                                     exprNode_traversRequiresConstraints
1906                                     (exprData_getOpB (data)));
1907        break;
1908     case XPR_SIZEOFT:
1909       break;
1910
1911     case XPR_SIZEOF:
1912
1913        ret = constraintList_addListFree (ret,
1914                                     exprNode_traversRequiresConstraints
1915                                      (exprData_getSingle (data)));
1916        break;
1917
1918     case XPR_CALL:
1919       ret = constraintList_addListFree (ret,
1920                                      exprNode_traversRequiresConstraints
1921                                     (exprData_getFcn (data)));
1922       /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */
1923       break;
1924
1925     case XPR_RETURN:
1926       ret = constraintList_addListFree (ret,
1927                                     exprNode_traversRequiresConstraints
1928                                     (exprData_getSingle (data)));
1929       break;
1930
1931     case XPR_NULLRETURN:
1932       break;
1933
1934     case XPR_FACCESS:
1935       ret = constraintList_addListFree (ret,
1936                                         exprNode_traversRequiresConstraints
1937                                         (exprData_getFieldNode (data)));
1938       break;
1939
1940     case XPR_ARROW:
1941       ret = constraintList_addListFree (ret,
1942                                         exprNode_traversRequiresConstraints
1943                                         (exprData_getFieldNode (data)));
1944       break;
1945
1946     case XPR_STRINGLITERAL:
1947       break;
1948
1949     case XPR_NUMLIT:
1950       break;
1951     case XPR_POSTOP:
1952
1953            ret = constraintList_addListFree (ret,
1954                                     exprNode_traversRequiresConstraints
1955                                     (exprData_getUopNode (data)));
1956            break;
1957
1958     case XPR_CAST:
1959
1960       ret = constraintList_addListFree (ret,
1961                                     exprNode_traversRequiresConstraints
1962                                     (exprData_getCastNode (data)));
1963       break;
1964
1965     default:
1966       break;
1967     }
1968
1969   return ret;
1970 }
1971
1972
1973 /* walk down the tree and get all Ensures Constraints in each subexpression*/
1974 /*@only@*/ constraintList exprNode_traversEnsuresConstraints (exprNode e)
1975 {
1976   exprNode t1;
1977
1978   bool handledExprNode;
1979   exprData data;
1980   constraintList ret;
1981
1982   if (exprNode_handleError (e))
1983     {
1984       ret = constraintList_makeNew();
1985       return ret;
1986     }
1987
1988   ret = constraintList_copy (e->ensuresConstraints);
1989   handledExprNode = TRUE;
1990
1991   data = e->edata;
1992
1993   DPRINTF ((message ("exprnode_traversEnsuresConstraints call for %s with "
1994                      "constraintList of %s",
1995                      exprNode_unparse (e),
1996                      constraintList_print(e->ensuresConstraints)
1997                      )
1998             ));
1999
2000
2001   switch (e->kind)
2002     {
2003     case XPR_WHILEPRED:
2004       t1 = exprData_getSingle (data);
2005       ret = constraintList_addListFree (ret,exprNode_traversEnsuresConstraints (t1));
2006       break;
2007
2008     case XPR_FETCH:
2009       ret = constraintList_addListFree (ret,
2010                                         exprNode_traversEnsuresConstraints
2011                                         (exprData_getPairA (data)));
2012
2013       ret = constraintList_addListFree (ret,
2014                                         exprNode_traversEnsuresConstraints
2015                                         (exprData_getPairB (data)));
2016       break;
2017     case XPR_PREOP:
2018       ret = constraintList_addListFree (ret,
2019                                         exprNode_traversEnsuresConstraints
2020                                         (exprData_getUopNode (data)));
2021       break;
2022
2023     case XPR_PARENS:
2024       ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints
2025                                         (exprData_getUopNode (data)));
2026       break;
2027
2028     case XPR_INIT:
2029       ret = constraintList_addListFree (ret,
2030                                         exprNode_traversEnsuresConstraints
2031                                         (exprData_getInitNode (data)));
2032       break;
2033
2034
2035     case XPR_ASSIGN:
2036       ret = constraintList_addListFree (ret,
2037                                         exprNode_traversEnsuresConstraints
2038                                         (exprData_getOpA (data)));
2039
2040       ret = constraintList_addListFree (ret,
2041                                         exprNode_traversEnsuresConstraints
2042                                         (exprData_getOpB (data)));
2043       break;
2044     case XPR_OP:
2045       ret = constraintList_addListFree (ret,
2046                                         exprNode_traversEnsuresConstraints
2047                                         (exprData_getOpA (data)));
2048
2049       ret = constraintList_addListFree (ret,
2050                                         exprNode_traversEnsuresConstraints
2051                                         (exprData_getOpB (data)));
2052       break;
2053     case XPR_SIZEOFT:
2054       break;
2055
2056     case XPR_SIZEOF:
2057       ret = constraintList_addListFree (ret,
2058                                         exprNode_traversEnsuresConstraints
2059                                         (exprData_getSingle (data)));
2060       break;
2061     case XPR_CALL:
2062       ret = constraintList_addListFree (ret,
2063                                         exprNode_traversEnsuresConstraints
2064                                         (exprData_getFcn (data)));
2065       /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */
2066       break;
2067     case XPR_RETURN:
2068       ret = constraintList_addListFree (ret,
2069                                         exprNode_traversEnsuresConstraints
2070                                         (exprData_getSingle (data)));
2071       break;
2072     case XPR_NULLRETURN:
2073       break;
2074     case XPR_FACCESS:
2075       ret = constraintList_addListFree (ret,
2076                                         exprNode_traversEnsuresConstraints
2077                                         (exprData_getFieldNode (data)));
2078       break;
2079     case XPR_ARROW:
2080       ret = constraintList_addListFree (ret,
2081                                         exprNode_traversEnsuresConstraints
2082                                         (exprData_getFieldNode (data)));
2083       break;
2084     case XPR_STRINGLITERAL:
2085       break;
2086     case XPR_NUMLIT:
2087       break;
2088     case XPR_POSTOP:
2089       ret = constraintList_addListFree (ret,
2090                                         exprNode_traversEnsuresConstraints
2091                                         (exprData_getUopNode (data)));
2092       break;
2093     case XPR_CAST:
2094       ret = constraintList_addListFree (ret,
2095                                         exprNode_traversEnsuresConstraints
2096                                         (exprData_getCastNode (data)));
2097       break;
2098     default:
2099       break;
2100     }
2101
2102   DPRINTF((message ("exprnode_traversEnsuresConstraints call for %s with "
2103                     "constraintList of  is returning %s",
2104                     exprNode_unparse (e),
2105                     constraintList_print(ret))));
2106
2107   return ret;
2108 }
2109
2110 /*drl moved out of constraintResolve.c 07-02-001 */
2111 void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist,
2112                         fileloc sequencePoint)
2113 {
2114   temp->requiresConstraints = constraintList_makeNew();
2115   temp->ensuresConstraints = constraintList_makeNew();
2116   temp->trueEnsuresConstraints = constraintList_makeNew();
2117   temp->falseEnsuresConstraints = constraintList_makeNew();
2118
2119   exprNodeList_elements (arglist, el)
2120     {
2121       constraintList temp2;
2122       exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint);
2123       temp2 = el->requiresConstraints;
2124       el->requiresConstraints = exprNode_traversRequiresConstraints(el);
2125       constraintList_free(temp2);
2126
2127       temp2 = el->ensuresConstraints;
2128       el->ensuresConstraints  = exprNode_traversEnsuresConstraints(el);
2129       constraintList_free(temp2);
2130
2131       temp->requiresConstraints = constraintList_addList(temp->requiresConstraints,
2132                                                             el->requiresConstraints);
2133
2134       temp->ensuresConstraints = constraintList_addList(temp->ensuresConstraints,
2135                                                            el->ensuresConstraints);
2136     }
2137   end_exprNodeList_elements;
2138
2139 }
2140
2141 /*drl moved out of constraintResolve.c 07-03-001 */
2142 constraintList exprNode_getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall)
2143 {
2144   constraintList postconditions;
2145   uentry temp;
2146   DPRINTF((message ("Got call that %s (%s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (arglist))));
2147
2148   temp = exprNode_getUentry (fcn);
2149
2150   postconditions = uentry_getFcnPostconditions (temp);
2151
2152   if (constraintList_isDefined (postconditions))
2153     {
2154       postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist);
2155       postconditions = constraintList_doFixResult (postconditions, fcnCall);
2156     }
2157   else
2158     {
2159       postconditions = constraintList_makeNew();
2160     }
2161
2162   return postconditions;
2163 }
2164
2165 /*
2166 comment this out for now
2167 we'll include it in a production release when its stable...
2168
2169   void findStructs (exprNodeList arglist)
2170 {
2171
2172   ctype ct, rt;
2173
2174   DPRINTF((
2175            message("doing findStructs: %s", exprNodeList_unparse(arglist))
2176           ));
2177
2178
2179   exprNodeList_elements(arglist, expr)
2180     {
2181       ct = exprNode_getType(expr);
2182
2183       rt =  ctype_realType (ct);
2184
2185       if (ctype_isStruct (rt))
2186         TPRINTF((message("Found structure %s", exprNode_unparse(expr))
2187                  ));
2188       if (hasInvariants(ct))
2189         {
2190           constraintList invars;
2191
2192           invars = getInvariants(ct);
2193
2194
2195           TPRINTF((message ("findStructs has invariants %s ", constraintList_print (invars))
2196                    ));
2197
2198           invars = constraintList_doSRefFixStructConstraint(invars, exprNode_getSref(expr), ct);
2199
2200
2201           TPRINTF((message ("findStructs finded invariants to be %s ", constraintList_print (invars))
2202                    ));
2203         }
2204     }
2205   end_exprNodeList_elements;
2206 }
2207
2208 */
2209
2210 /*drl moved out of constraintResolve.c 07-02-001 */
2211 constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist)
2212 {
2213   constraintList preconditions;
2214   uentry temp;
2215   DPRINTF((message ("Got call that %s (%s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (arglist))));
2216
2217   temp = exprNode_getUentry (fcn);
2218
2219   preconditions = uentry_getFcnPreconditions (temp);
2220
2221   if (constraintList_isDefined(preconditions))
2222     {
2223       preconditions = constraintList_togglePost (preconditions);
2224       preconditions = constraintList_preserveCallInfo(preconditions, fcn);
2225       preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist);
2226     }
2227   else
2228     {
2229       if (constraintList_isUndefined(preconditions))
2230         preconditions = constraintList_makeNew();
2231     }
2232   DPRINTF ((message("Done checkCall\n")));
2233   DPRINTF ((message("Returning list %q ", constraintList_printDetailed(preconditions))));
2234
2235   /*
2236     drl we're going to comment this out for now
2237     we'll include it if we're sure it's working
2238
2239     findStructs(arglist);
2240   */
2241
2242   return preconditions;
2243 }
2244
2245 /*drl added this function 10.29.001
2246   takes an exprNode of the form const + const
2247   and sets the value
2248 */
2249 /*drl
2250   I'm a bit nervous about modifying the exprNode
2251   but this is the easy way to do this
2252   If I have time I'd like to cause the exprNode to get created correctly in the first place */
2253 /*@i223*/
2254 void exprNode_findValue(exprNode e)
2255 {
2256   exprData data;
2257
2258   exprNode t1, t2;
2259   lltok tok;
2260
2261   data = e->edata;
2262
2263   if (exprNode_hasValue(e))
2264     return;
2265
2266   if (e->kind == XPR_OP)
2267     {
2268       t1 = exprData_getOpA (data);
2269      t2 = exprData_getOpB (data);
2270      tok = exprData_getOpTok (data);
2271
2272      exprNode_findValue(t1);
2273      exprNode_findValue(t2);
2274
2275      if (!(exprNode_knownIntValue(t1) && (exprNode_knownIntValue(t2))))
2276        return;
2277
2278      if (lltok_isPlus_Op (tok))
2279        {
2280          long v1, v2;
2281
2282          v1 = exprNode_getLongValue(t1);
2283          v2 = exprNode_getLongValue(t2);
2284
2285          if (multiVal_isDefined(e->val))
2286            multiVal_free (e->val);
2287
2288          e->val = multiVal_makeInt (v1 + v2);
2289        }
2290
2291      if (lltok_isMinus_Op (tok))
2292        {
2293          long v1, v2;
2294
2295          v1 = exprNode_getLongValue(t1);
2296          v2 = exprNode_getLongValue(t2);
2297
2298          if (multiVal_isDefined(e->val))
2299            {
2300              multiVal_free (e->val);
2301            }
2302
2303          e->val = multiVal_makeInt (v1 - v2);
2304        }
2305
2306      /*drl I should really do * and / at some point */
2307
2308     }
2309
2310 }
2311