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