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