src/constraintGeneration.c

   1 /*
   2 ** LCLint - annotation-assisted static program checker
   3 ** Copyright (C) 1994-2001 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 lclint: lclint-request@cs.virginia.edu
  21 ** To report a bug: lclint-bug@cs.virginia.edu
  22 ** For more information: http://lclint.cs.virginia.edu
  23 */
  24
  25 /*
  26 ** constraintGeneration.c
  27 */
  28
  29 /* #define DEBUGPRINT 1 */
  30
  31 # include <ctype.h> /* for isdigit */
  32 # include "lclintMacros.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 exprNode_doGenerateConstraintSwitch (/*@dependent@*/ exprNode switchExpr,
 557                                                   /*@dependent@*/ exprNode body, /*@special@*/ constraintList * currentRequires, /*@special@*/  constraintList *
 558                                                   currentEnsures,  /*@special@*/  constraintList * savedRequires, /*@special@*/ constraintList *
 559                                                   savedEnsures)
 560      /*@post:only *currentRequires,  *currentEnsures,  *savedRequires, *savedEnsures @*/ /*@defines *currentRequires,  *currentEnsures,  *savedRequires, *savedEnsures @*/
 561 {
 562   exprNode stmt, stmtList;
 563
 564   DPRINTF(( message("exprNode_doGenerateConstraintSwitch: (switch %s) %s",
 565                     exprNode_unparse(switchExpr), exprNode_unparse(body)
 566                     ) ));
 567
 568   if (exprNode_isError(body) )
 569     {
 570       *currentRequires = constraintList_makeNew();
 571       *currentEnsures = constraintList_makeNew();
 572
 573       *savedRequires = constraintList_makeNew();
 574       *savedEnsures = constraintList_makeNew();
 575       /*@-onlytrans@*/
 576       return;
 577       /*@=onlytrans@*/
 578     }
 579
 580   if (body->kind != XPR_STMTLIST )
 581     {
 582       DPRINTF((message("exprNode_doGenerateConstraintSwitch: non stmtlist: %s",
 583                        exprNode_unparse(body) )));
 584       stmt = body;
 585       stmtList = exprNode_undefined;
 586       stmt = exprNode_makeDependent(stmt);
 587       stmtList = exprNode_makeDependent(stmtList);
 588     }
 589   else
 590     {
 591       stmt     = exprData_getPairB(body->edata);
 592       stmtList = exprData_getPairA(body->edata);
 593       stmt = exprNode_makeDependent(stmt);
 594       stmtList = exprNode_makeDependent(stmtList);
 595     }
 596
 597   DPRINTF((message("exprNode_doGenerateConstraintSwitch: stmtlist: %s stmt: %s",
 598                    exprNode_unparse(stmtList), exprNode_unparse(stmt) )
 599            ));
 600
 601
 602   exprNode_doGenerateConstraintSwitch (switchExpr, stmtList, currentRequires, currentEnsures,
 603                                        savedRequires, savedEnsures );
 604
 605   if (exprNode_isError(stmt) )
 606     /*@-onlytrans@*/
 607     return;
 608     /*@=onlytrans@*/
 609
 610   exprNode_stmt(stmt);
 611
 612   switchExpr = exprNode_makeDependent (switchExpr);
 613
 614   if (! exprNode_isCaseMarker(stmt) )
 615     {
 616
 617       constraintList temp;
 618
 619       DPRINTF (( message("Got normal statement %s (requires %s ensures %s)", exprNode_unparse(stmt),
 620                          constraintList_unparse(stmt->requiresConstraints), constraintList_unparse(stmt->ensuresConstraints) ) ));
 621
 622       temp = constraintList_reflectChanges (stmt->requiresConstraints,
 623                                             *currentEnsures);
 624
 625             *currentRequires = constraintList_mergeRequiresFreeFirst(
 626                                                                      *currentRequires,
 627                                                                      temp);
 628
 629             constraintList_free(temp);
 630
 631                   *currentEnsures = constraintList_mergeEnsuresFreeFirst
 632                     (*currentEnsures,
 633                      stmt->ensuresConstraints);
 634                   DPRINTF(( message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
 635                                     "%s currentEnsures:%s",
 636                                     exprNode_unparse(switchExpr), exprNode_unparse(body),
 637                                     constraintList_print(*currentRequires), constraintList_print(*currentEnsures)
 638                                     ) ));
 639                   /*@-onlytrans@*/
 640                   return;
 641                   /*@=onlytrans@*/
 642
 643     }
 644
 645   if (exprNode_isCaseMarker(stmt) && exprNode_mustEscape(stmtList) )
 646     {
 647       /*
 648       ** merge current and saved constraint with Logical Or...
 649       ** make a constraint for ensures
 650       */
 651
 652       constraintList temp;
 653       constraint con;
 654
 655       DPRINTF (( message("Got case marker") ));
 656
 657       if (constraintList_isUndefined(*savedEnsures) &&
 658           constraintList_isUndefined(*savedRequires) )
 659         {
 660           llassert(constraintList_isUndefined(*savedEnsures) );
 661           llassert(constraintList_isUndefined(*savedRequires) );
 662           *savedEnsures  = constraintList_copy(*currentEnsures);
 663           *savedRequires = constraintList_copy(*currentRequires);
 664         }
 665       else
 666         {
 667           DPRINTF (( message("Doing logical or") ));
 668           temp = constraintList_logicalOr (*savedEnsures, *currentEnsures);
 669           constraintList_free (*savedEnsures);
 670           *savedEnsures = temp;
 671
 672           *savedRequires = constraintList_mergeRequiresFreeFirst (*savedRequires, *currentRequires);
 673         }
 674
 675       con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle
 676                                         (stmt->edata), exprNode_getfileloc(stmt) );
 677
 678
 679       constraintList_free(*currentEnsures);
 680       *currentEnsures = constraintList_makeNew();
 681       *currentEnsures = constraintList_add(*currentEnsures, con);
 682
 683       constraintList_free(*currentRequires);
 684       *currentRequires = constraintList_makeNew();
 685       DPRINTF(( message("exprNode_doGenerateConstraintSwitch: (switch %s) %s savedRequires:"
 686                         "%s savedEnsures:%s",
 687                         exprNode_unparse(switchExpr), exprNode_unparse(body),
 688                         constraintList_print(*savedRequires), constraintList_print(*savedEnsures)
 689                         ) ));
 690
 691     }
 692
 693   else if (exprNode_isCaseMarker(stmt) )
 694     /* prior case has no break. */
 695     {
 696       /*
 697          We don't do anything to the sved constraints because the case hasn't ended
 698          The new ensures constraints for the case will be:
 699          the constraint for the case statement (CASE_LABEL == SWITCH_EXPR) logicalOr currentEnsures
 700       */
 701
 702       constraintList temp;
 703       constraint con;
 704
 705       constraintList ensuresTemp;
 706
 707       DPRINTF (( message("Got case marker with no prior break") ));
 708
 709       con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle
 710                                         (stmt->edata), exprNode_getfileloc(stmt) );
 711
 712       ensuresTemp = constraintList_makeNew();
 713
 714       ensuresTemp = constraintList_add (ensuresTemp, con);
 715
 716       if (exprNode_isError(stmtList) )
 717         {
 718           constraintList_free(*currentEnsures);
 719
 720           *currentEnsures = constraintList_copy(ensuresTemp);
 721           constraintList_free(ensuresTemp);
 722
 723         }
 724       else
 725         {
 726
 727           temp = constraintList_logicalOr (*currentEnsures, ensuresTemp);
 728
 729           constraintList_free(*currentEnsures);
 730           constraintList_free(ensuresTemp);
 731
 732           *currentEnsures = temp;
 733         }
 734       constraintList_free(*currentRequires);
 735
 736       *currentRequires = constraintList_makeNew();
 737     }
 738   else
 739     {
 740       /*
 741         we handle the case of ! exprNode_isCaseMarker above
 742         the else if clause should always be true.
 743       */
 744       BADEXIT;
 745     }
 746
 747   DPRINTF(( message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
 748                     "%s currentEnsures:%s",
 749                     exprNode_unparse(switchExpr), exprNode_unparse(body),
 750                     constraintList_print(*currentRequires), constraintList_print(*currentEnsures)
 751                     ) ));
 752   /*@-onlytrans@*/
 753   return;
 754   /*@=onlytrans@*/
 755
 756 }
 757
 758
 759 static void exprNode_generateConstraintSwitch ( exprNode switchStmt)
 760 {
 761   constraintList constraintsRequires;
 762   constraintList constraintsEnsures;
 763   constraintList lastRequires;
 764   constraintList lastEnsures;
 765
 766   exprNode body;
 767   exprNode switchExpr;
 768
 769   switchExpr = exprData_getPairA(switchStmt->edata);
 770   body = exprData_getPairB(switchStmt->edata);
 771
 772   /*@i22*/
 773   DPRINTF((message("") ));
 774
 775   if ( body->kind == XPR_BLOCK)
 776     body = exprData_getSingle(body->edata);
 777
 778   /*
 779   constraintsRequires = constraintList_undefined;
 780   constraintsEnsures = constraintList_undefined;
 781
 782   lastRequires = constraintList_makeNew();
 783   lastEnsures = constraintList_makeNew();
 784   */
 785
 786   exprNode_doGenerateConstraintSwitch (switchExpr, body, &lastRequires, &lastEnsures, &constraintsRequires, &constraintsEnsures);
 787
 788   /*
 789     merge current and saved constraint with Logical Or...
 790     make a constraint for ensures
 791   */
 792
 793   constraintList_free(switchStmt->requiresConstraints);
 794   constraintList_free(switchStmt->ensuresConstraints);
 795
 796   if (constraintList_isDefined(constraintsEnsures) && constraintList_isDefined(constraintsRequires) )
 797     {
 798       switchStmt->ensuresConstraints = constraintList_logicalOr(constraintsEnsures, lastEnsures);
 799       switchStmt->requiresConstraints =   constraintList_mergeRequires(constraintsRequires, lastRequires);
 800       constraintList_free (constraintsRequires);
 801       constraintList_free (constraintsEnsures);
 802     }
 803   else
 804     {
 805       switchStmt->ensuresConstraints =    constraintList_copy(lastEnsures);
 806       switchStmt->requiresConstraints =   constraintList_copy(lastRequires);
 807     }
 808
 809   constraintList_free (lastRequires);
 810   constraintList_free (lastEnsures);
 811
 812   DPRINTF(( (message(" exprNode_generateConstraintSwitch returning requires: %s and ensures %s",
 813                      constraintList_print( switchStmt->requiresConstraints),
 814                      constraintList_print( switchStmt->ensuresConstraints)
 815                      )
 816              ) ));
 817 }
 818
 819 static exprNode doSwitch (/*@returned@*/ exprNode e)
 820 {
 821   exprNode body;
 822   exprData data;
 823
 824   data = e->edata;
 825   DPRINTF (( message ("doSwitch for: switch (%s) %s",
 826                       exprNode_unparse (exprData_getPairA (data)),
 827                       exprNode_unparse (exprData_getPairB (data))) ));
 828
 829   body = exprData_getPairB (data);
 830   exprNode_generateConstraintSwitch (e);
 831   return e;
 832 }
 833
 834 void exprNode_multiStatement (/*@dependent@*/ exprNode e)
 835 {
 836
 837   bool ret;
 838   exprData data;
 839   exprNode e1, e2;
 840   exprNode p, trueBranch, falseBranch;
 841   exprNode forPred, forBody;
 842   exprNode test;
 843
 844   constraintList temp;
 845
 846   DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse( e),
 847                     fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
 848
 849   if (exprNode_handleError (e))
 850     {
 851       return;
 852     }
 853
 854   data = e->edata;
 855
 856   ret = TRUE;
 857
 858   switch (e->kind)
 859     {
 860
 861     case XPR_FOR:
 862       forPred = exprData_getPairA (data);
 863       forBody = exprData_getPairB (data);
 864
 865       /* First generate the constraints */
 866       exprNode_generateConstraints (forPred);
 867       exprNode_generateConstraints (forBody);
 868
 869
 870       doFor (e, forPred, forBody);
 871
 872       break;
 873
 874     case XPR_FORPRED:
 875       exprNode_generateConstraints (exprData_getTripleInit (data) );
 876       test = exprData_getTripleTest (data);
 877       exprNode_exprTraverse (test,FALSE, FALSE, exprNode_loc(e));
 878       exprNode_generateConstraints (exprData_getTripleInc (data) );
 879
 880       if (!exprNode_isError(test) )
 881         {
 882           constraintList temp2;
 883           temp2 = test->trueEnsuresConstraints;
 884           test->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(test);
 885           constraintList_free(temp2);
 886         }
 887
 888       exprNode_generateConstraints (exprData_getTripleInc (data));
 889       break;
 890
 891     case XPR_WHILE:
 892       e1 = exprData_getPairA (data);
 893       e2 = exprData_getPairB (data);
 894
 895        exprNode_exprTraverse (e1,
 896                               FALSE, FALSE, exprNode_loc(e1));
 897
 898        exprNode_generateConstraints (e2);
 899
 900        e = doWhile (e, e1, e2);
 901
 902       break;
 903
 904     case XPR_IF:
 905       DPRINTF(( "IF:") );
 906       DPRINTF ((exprNode_unparse(e) ) );
 907       e1 = exprData_getPairA (data);
 908       e2 = exprData_getPairB (data);
 909
 910       exprNode_exprTraverse (e1, FALSE, FALSE, exprNode_loc(e1));
 911
 912       exprNode_generateConstraints (e2);
 913       e = doIf (e, e1, e2);
 914       break;
 915
 916     case XPR_IFELSE:
 917       DPRINTF(("Starting IFELSE"));
 918       p = exprData_getTriplePred (data);
 919       trueBranch = exprData_getTripleTrue (data);
 920       falseBranch = exprData_getTripleFalse (data);
 921
 922       exprNode_exprTraverse (p,
 923                              FALSE, FALSE, exprNode_loc(p));
 924       exprNode_generateConstraints (trueBranch);
 925       exprNode_generateConstraints (falseBranch);
 926
 927       temp = p->ensuresConstraints;
 928       p->ensuresConstraints = exprNode_traversEnsuresConstraints (p);
 929       constraintList_free(temp);
 930
 931       temp = p->requiresConstraints;
 932       p->requiresConstraints = exprNode_traversRequiresConstraints (p);
 933       constraintList_free(temp);
 934
 935       temp = p->trueEnsuresConstraints;
 936       p->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(p);
 937       constraintList_free(temp);
 938
 939       temp = p->falseEnsuresConstraints;
 940       p->falseEnsuresConstraints =  exprNode_traversFalseEnsuresConstraints(p);
 941       constraintList_free(temp);
 942
 943           e = doIfElse (e, p, trueBranch, falseBranch);
 944       DPRINTF( ("Done IFELSE") );
 945       break;
 946
 947     case XPR_DOWHILE:
 948
 949       e2 = (exprData_getPairB (data));
 950       e1 = (exprData_getPairA (data));
 951
 952       DPRINTF((message ("do { %s } while (%s)", exprNode_unparse(e2), exprNode_unparse(e1) ) ));
 953       exprNode_generateConstraints (e2);
 954       exprNode_generateConstraints (e1);
 955       e = exprNode_copyConstraints (e, e2);
 956       DPRINTF ((message ("e = %s  ", constraintList_print(e->requiresConstraints) ) ));
 957
 958       break;
 959
 960     case XPR_BLOCK:
 961       exprNode_generateConstraints (exprData_getSingle (data));
 962
 963       constraintList_free(e->requiresConstraints);
 964       e->requiresConstraints = constraintList_copy ( (exprData_getSingle (data))->requiresConstraints );
 965
 966       constraintList_free(e->ensuresConstraints);
 967       e->ensuresConstraints = constraintList_copy ( (exprData_getSingle (data))->ensuresConstraints );
 968       break;
 969
 970     case XPR_SWITCH:
 971       e = doSwitch (e);
 972       break;
 973     case XPR_STMT:
 974     case XPR_STMTLIST:
 975       exprNode_stmtList (e);
 976       return ;
 977       /*@notreached@*/
 978       break;
 979     default:
 980       ret=FALSE;
 981     }
 982   return;
 983 }
 984
 985 static bool lltok_isBoolean_Op (lltok tok)
 986 {
 987   /*this should really be a switch statement but
 988     I don't want to violate the abstraction
 989     maybe this should go in lltok.c */
 990
 991   if (lltok_isEq_Op (tok) )
 992         {
 993           return TRUE;
 994         }
 995       if (lltok_isAnd_Op (tok) )
 996
 997         {
 998
 999           return TRUE;
1000         }
1001    if (lltok_isOr_Op (tok) )
1002         {
1003           return TRUE;
1004         }
1005
1006    if (lltok_isGt_Op (tok) )
1007      {
1008        return TRUE;
1009      }
1010    if (lltok_isLt_Op (tok) )
1011      {
1012        return TRUE;
1013      }
1014
1015    if (lltok_isLe_Op (tok) )
1016      {
1017        return TRUE;
1018      }
1019
1020    if (lltok_isGe_Op (tok) )
1021      {
1022        return TRUE;
1023      }
1024
1025    return FALSE;
1026
1027 }
1028
1029
1030 static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ bool definatelv, /*@unused@*/ bool definaterv,  fileloc sequencePoint)
1031 {
1032   constraint cons;
1033   exprNode t1, t2;
1034   exprData data;
1035   lltok tok;
1036   constraintList tempList, temp;
1037   data = e->edata;
1038
1039   tok = exprData_getOpTok (data);
1040   t1 = exprData_getOpA (data);
1041   t2 = exprData_getOpB (data);
1042
1043   tempList = constraintList_undefined;
1044
1045   /* arithmetic tests */
1046
1047   if (lltok_isEq_Op (tok) )
1048     {
1049       cons =  constraint_makeEnsureEqual (t1, t2, sequencePoint);
1050       e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1051     }
1052
1053
1054   if (lltok_isLt_Op (tok) )
1055     {
1056       cons =  constraint_makeEnsureLessThan (t1, t2, sequencePoint);
1057       e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1058       cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
1059       e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1060     }
1061
1062   if (lltok_isGe_Op (tok) )
1063     {
1064       cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
1065       e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1066
1067       cons =  constraint_makeEnsureLessThan (t1, t2, sequencePoint);
1068       e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1069     }
1070
1071   if (lltok_isGt_Op (tok) )
1072     {
1073       cons =  constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
1074       e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1075       cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
1076       e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1077     }
1078
1079   if (lltok_isLe_Op (tok) )
1080     {
1081       cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
1082       e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1083
1084       cons =  constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
1085       e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1086     }
1087
1088   /* Logical operations */
1089
1090   if (lltok_isAnd_Op (tok) )
1091     {
1092       /* true ensures  */
1093       tempList = constraintList_copy (t1->trueEnsuresConstraints);
1094       tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
1095       e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList);
1096
1097       /* false ensures: fens t1 or tens t1 and fens t2 */
1098       tempList = constraintList_copy (t1->trueEnsuresConstraints);
1099       tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
1100       temp = tempList;
1101       tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints);
1102       constraintList_free (temp);
1103
1104       /* evans - was constraintList_addList - memory leak detected by lclint */
1105       e->falseEnsuresConstraints = constraintList_addListFree (e->falseEnsuresConstraints, tempList);
1106     }
1107   else if (lltok_isOr_Op (tok) )
1108     {
1109       /* false ensures */
1110       tempList = constraintList_copy (t1->falseEnsuresConstraints);
1111       tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
1112       e->falseEnsuresConstraints = constraintList_addListFree(e->falseEnsuresConstraints, tempList);
1113
1114       /* true ensures: tens t1 or fens t1 and tens t2 */
1115       tempList = constraintList_copy (t1->falseEnsuresConstraints);
1116       tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
1117
1118       temp = tempList;
1119       tempList = constraintList_logicalOr (tempList, t1->trueEnsuresConstraints);
1120       constraintList_free(temp);
1121
1122       e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList);
1123       tempList = constraintList_undefined;
1124     }
1125   else
1126     {
1127       DPRINTF((message("%s is not a boolean operation", lltok_unparse(tok) ) ));
1128     }
1129 }
1130
1131 void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv,  /*@observer@*/ /*@temp@*/ fileloc sequencePoint)
1132 {
1133   exprNode t1, t2, fcn;
1134   lltok tok;
1135   bool handledExprNode;
1136   exprData data;
1137   constraint cons;
1138
1139   constraintList temp;
1140
1141   if (exprNode_isError(e) )
1142     {
1143       return;
1144     }
1145
1146   DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e),
1147                     fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
1148
1149   /*e->requiresConstraints = constraintList_makeNew();
1150   e->ensuresConstraints = constraintList_makeNew();
1151   e->trueEnsuresConstraints = constraintList_makeNew();;
1152   e->falseEnsuresConstraints = constraintList_makeNew();;
1153   */
1154
1155   if (exprNode_isUnhandled (e) )
1156      {
1157        return;
1158      }
1159
1160   handledExprNode = TRUE;
1161
1162   data = e->edata;
1163
1164   switch (e->kind)
1165     {
1166     case XPR_WHILEPRED:
1167       t1 = exprData_getSingle (data);
1168       exprNode_exprTraverse (t1,  definatelv, definaterv, sequencePoint);
1169       e = exprNode_copyConstraints (e, t1);
1170       break;
1171
1172     case XPR_FETCH:
1173
1174       if (definatelv )
1175         {
1176           t1 =  (exprData_getPairA (data) );
1177           t2 =  (exprData_getPairB (data) );
1178           cons =  constraint_makeWriteSafeExprNode (t1, t2);
1179         }
1180       else
1181         {
1182           t1 =  (exprData_getPairA (data) );
1183           t2 =  (exprData_getPairB (data) );
1184           cons = constraint_makeReadSafeExprNode (t1, t2 );
1185         }
1186
1187       e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
1188       cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint);
1189       e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1190
1191       cons = constraint_makeEnsureLteMaxRead (t2, t1);
1192       e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1193
1194       exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
1195       exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
1196
1197       /*@i325 Should check which is array/index. */
1198       break;
1199
1200     case XPR_PARENS:
1201       exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint);
1202       break;
1203     case XPR_INIT:
1204       {
1205         /*
1206         idDecl t;
1207
1208         uentry ue;
1209         exprNode lhs;
1210
1211         t = exprData_getInitId (data);
1212         ue = usymtab_lookup (idDecl_observeId (t));
1213         lhs = exprNode_createId (ue);
1214         */
1215         t2 = exprData_getInitNode (data);
1216
1217         /*      DPRINTF(( (message("initialization: %s = %s",
1218                            exprNode_unparse(lhs),
1219                            exprNode_unparse(t2)
1220                            )
1221                    ) ));        */
1222
1223         exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
1224
1225         /* this test is nessecary because some expressions generate a null expression node.  function pointer do that -- drl */
1226         if ( (!exprNode_isError (e))  &&  (!exprNode_isError(t2)) )
1227           {
1228             cons =  constraint_makeEnsureEqual (e, t2, sequencePoint);
1229             e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1230           }
1231       }
1232
1233       break;
1234     case XPR_ASSIGN:
1235       t1 = exprData_getOpA (data);
1236       t2 = exprData_getOpB (data);
1237       exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
1238       exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
1239
1240       /* this test is nessecary because some expressions generate a null expression node.  function pointer do that -- drl */
1241       if ( (!exprNode_isError (t1))  &&  (!exprNode_isError(t2)) )
1242         {
1243           cons =  constraint_makeEnsureEqual (t1, t2, sequencePoint);
1244           e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1245         }
1246       break;
1247     case XPR_OP:
1248       t1 = exprData_getOpA (data);
1249       t2 = exprData_getOpB (data);
1250       tok = exprData_getOpTok (data);
1251
1252
1253       if (tok.tok == ADD_ASSIGN)
1254         {
1255           exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
1256           exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
1257
1258           cons = constraint_makeAddAssign (t1, t2,  sequencePoint );
1259           e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1260         }
1261       else if (tok.tok == SUB_ASSIGN)
1262         {
1263           exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
1264           exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
1265
1266           cons = constraint_makeSubtractAssign (t1, t2,  sequencePoint );
1267           e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1268         }
1269       else
1270         {
1271           exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
1272           exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
1273         }
1274
1275       if (lltok_isBoolean_Op (tok) )
1276         exprNode_booleanTraverse (e, definatelv, definaterv, sequencePoint);
1277
1278       break;
1279     case XPR_SIZEOFT:
1280       /*@i43 drl possible problem : warning make sure the case can be ignored.. */
1281
1282       break;
1283
1284     case XPR_SIZEOF:
1285       /* drl  7-16-01
1286          C standard says operand to sizeof isn't evaluated unless
1287          its a variable length array.  So we don't generate constraints.
1288       */
1289
1290       break;
1291
1292     case XPR_CALL:
1293       fcn = exprData_getFcn(data);
1294
1295       exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint );
1296       DPRINTF ( (message ("Got call that %s ( %s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (exprData_getArgs (data) ) ) ) );
1297
1298       fcn->requiresConstraints = constraintList_addListFree (fcn->requiresConstraints,
1299                                                  checkCall (fcn, exprData_getArgs (data)  ) );
1300
1301       fcn->ensuresConstraints = constraintList_addListFree (fcn->ensuresConstraints,
1302                                                  exprNode_getPostConditions(fcn, exprData_getArgs (data),e  ) );
1303
1304       t1 = exprNode_createNew (exprNode_getType (e) );
1305       checkArgumentList (t1, exprData_getArgs(data), sequencePoint);
1306       exprNode_mergeResolve (e, t1, fcn);
1307       exprNode_free(t1);
1308       break;
1309
1310     case XPR_RETURN:
1311       exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
1312       break;
1313
1314     case XPR_NULLRETURN:
1315
1316       break;
1317
1318
1319     case XPR_FACCESS:
1320       exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
1321       break;
1322
1323     case XPR_ARROW:
1324       exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
1325       break;
1326
1327     case XPR_STRINGLITERAL:
1328
1329       break;
1330
1331     case XPR_NUMLIT:
1332
1333       break;
1334
1335     case XPR_PREOP:
1336       t1 = exprData_getUopNode(data);
1337       tok = (exprData_getUopTok (data));
1338       exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
1339       /*handle * pointer access */
1340       if (lltok_isInc_Op (tok) )
1341         {
1342           DPRINTF(("doing ++(var)"));
1343           t1 = exprData_getUopNode (data);
1344           cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
1345           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1346         }
1347       else if (lltok_isDec_Op (tok) )
1348         {
1349           DPRINTF(("doing --(var)"));
1350           t1 = exprData_getUopNode (data);
1351           cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint );
1352           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1353         }
1354       else if (lltok_isMult( tok  ) )
1355         {
1356           if (definatelv)
1357             {
1358               cons = constraint_makeWriteSafeInt (t1, 0);
1359             }
1360           else
1361             {
1362               cons = constraint_makeReadSafeInt (t1, 0);
1363             }
1364               e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
1365         }
1366       else if (lltok_isNot_Op (tok) )
1367         /* ! expr */
1368         {
1369           constraintList_free(e->trueEnsuresConstraints);
1370
1371           e->trueEnsuresConstraints  = constraintList_copy (t1->falseEnsuresConstraints);
1372           constraintList_free(e->falseEnsuresConstraints);
1373           e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints);
1374         }
1375
1376       else if (lltok_isAmpersand_Op (tok) )
1377         {
1378           break;
1379         }
1380       else if (lltok_isMinus_Op (tok) )
1381         {
1382           break;
1383         }
1384       else if ( lltok_isExcl_Op (tok) )
1385         {
1386           break;
1387         }
1388       else if (lltok_isTilde_Op (tok) )
1389         {
1390           break;
1391         }
1392       else
1393         {
1394           llcontbug((message("Unsupported preop in %s", exprNode_unparse(e) ) ));
1395           BADEXIT;
1396         }
1397       break;
1398
1399     case XPR_POSTOP:
1400
1401       exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint );
1402
1403       if (lltok_isInc_Op (exprData_getUopTok (data) ) )
1404         {
1405           DPRINTF(("doing ++"));
1406           t1 = exprData_getUopNode (data);
1407           cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
1408           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1409         }
1410        if (lltok_isDec_Op (exprData_getUopTok (data) ) )
1411         {
1412           DPRINTF(("doing --"));
1413           t1 = exprData_getUopNode (data);
1414           cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint );
1415           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1416         }
1417       break;
1418     case XPR_CAST:
1419       {
1420         t2 =  exprData_getCastNode (data);
1421         DPRINTF (( message ("Examining cast (%q)%s",
1422                             qtype_unparse (exprData_getCastType (data)),
1423                             exprNode_unparse (t2) )
1424                    ));
1425         exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
1426       }
1427       break;
1428
1429     case XPR_COND:
1430       {
1431         exprNode pred, trueBranch, falseBranch;
1432            llassert(FALSE);
1433       pred = exprData_getTriplePred (data);
1434       trueBranch = exprData_getTripleTrue (data);
1435       falseBranch = exprData_getTripleFalse (data);
1436
1437       exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint );
1438
1439       temp =       pred->ensuresConstraints;
1440       pred->ensuresConstraints = exprNode_traversEnsuresConstraints(pred);
1441       constraintList_free(temp);
1442
1443       temp =       pred->requiresConstraints;
1444       pred->requiresConstraints = exprNode_traversRequiresConstraints(pred);
1445       constraintList_free(temp);
1446
1447       temp =       pred->trueEnsuresConstraints;
1448       pred->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(pred);
1449       constraintList_free(temp);
1450
1451       temp =       pred->falseEnsuresConstraints;
1452       pred->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(pred);
1453       constraintList_free(temp);
1454
1455
1456       exprNode_exprTraverse (trueBranch, FALSE, TRUE, sequencePoint );
1457
1458       temp =       trueBranch->ensuresConstraints;
1459       trueBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(trueBranch);
1460       constraintList_free(temp);
1461
1462
1463       temp =       trueBranch->requiresConstraints;
1464       trueBranch->requiresConstraints = exprNode_traversRequiresConstraints(trueBranch);
1465       constraintList_free(temp);
1466
1467
1468       temp =       trueBranch->trueEnsuresConstraints;
1469       trueBranch->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(trueBranch);
1470       constraintList_free(temp);
1471
1472       temp =       trueBranch->falseEnsuresConstraints;
1473       trueBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(trueBranch);
1474       constraintList_free(temp);
1475
1476       exprNode_exprTraverse (falseBranch, FALSE, TRUE, sequencePoint );
1477
1478       temp =       falseBranch->ensuresConstraints;
1479       falseBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(falseBranch);
1480       constraintList_free(temp);
1481
1482
1483       temp =       falseBranch->requiresConstraints;
1484       falseBranch->requiresConstraints = exprNode_traversRequiresConstraints(falseBranch);
1485       constraintList_free(temp);
1486
1487
1488       temp =       falseBranch->trueEnsuresConstraints;
1489       falseBranch->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(falseBranch);
1490       constraintList_free(temp);
1491
1492       temp =       falseBranch->falseEnsuresConstraints;
1493       falseBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(falseBranch);
1494       constraintList_free(temp);
1495
1496       /* if pred is true e equals true otherwise pred equals false */
1497
1498       cons =  constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
1499       trueBranch->ensuresConstraints = constraintList_add(trueBranch->ensuresConstraints, cons);
1500
1501       cons =  constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
1502       falseBranch->ensuresConstraints = constraintList_add(falseBranch->ensuresConstraints, cons);
1503
1504       e = doIfElse (e, pred, trueBranch, falseBranch);
1505
1506       }
1507       break;
1508     case XPR_COMMA:
1509       llassert(FALSE);
1510       t1 = exprData_getPairA (data);
1511       t2 = exprData_getPairB (data);
1512     /* we essiantially treat this like expr1; expr2
1513      of course sequencePoint isn't adjusted so this isn't completely accurate
1514     problems../  */
1515       exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint );
1516       exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
1517       exprNode_mergeResolve (e, t1, t2);
1518       break;
1519
1520     default:
1521       handledExprNode = FALSE;
1522     }
1523
1524   e->requiresConstraints =  constraintList_preserveOrig ( e->requiresConstraints);
1525   e->ensuresConstraints  =  constraintList_preserveOrig ( e->ensuresConstraints);
1526   e->requiresConstraints = constraintList_addGeneratingExpr ( e->requiresConstraints, e);
1527
1528   e->ensuresConstraints  = constraintList_addGeneratingExpr ( e->ensuresConstraints, e);
1529
1530
1531   e->requiresConstraints = constraintList_removeSurpressed( e->requiresConstraints);
1532
1533   DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) ));
1534
1535   DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) ));
1536
1537   DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->trueEnsuresConstraints) ) ));
1538
1539   DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->falseEnsuresConstraints) ) ));
1540
1541   return;
1542 }
1543
1544
1545 constraintList exprNode_traversTrueEnsuresConstraints (exprNode e)
1546 {
1547   exprNode t1;
1548
1549   bool handledExprNode;
1550   exprData data;
1551   constraintList ret;
1552
1553   if (exprNode_handleError (e))
1554     {
1555       ret = constraintList_makeNew();
1556       return ret;
1557     }
1558   ret = constraintList_copy (e->trueEnsuresConstraints );
1559
1560   handledExprNode = TRUE;
1561
1562   data = e->edata;
1563
1564   switch (e->kind)
1565     {
1566     case XPR_WHILEPRED:
1567       t1 = exprData_getSingle (data);
1568       ret = constraintList_addListFree ( ret, exprNode_traversTrueEnsuresConstraints (t1) );
1569       break;
1570
1571     case XPR_FETCH:
1572
1573       ret = constraintList_addListFree (ret,
1574                                     exprNode_traversTrueEnsuresConstraints
1575                                     (exprData_getPairA (data) ) );
1576
1577       ret = constraintList_addListFree (ret,
1578                                     exprNode_traversTrueEnsuresConstraints
1579                                     (exprData_getPairB (data) ) );
1580       break;
1581     case XPR_PREOP:
1582
1583       ret = constraintList_addListFree (ret,
1584                                     exprNode_traversTrueEnsuresConstraints
1585                                     (exprData_getUopNode (data) ) );
1586       break;
1587
1588     case XPR_PARENS:
1589       ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints
1590                                     (exprData_getUopNode (data) ) );
1591       break;
1592
1593     case XPR_INIT:
1594       ret = constraintList_addListFree (ret,
1595                                         exprNode_traversTrueEnsuresConstraints
1596                                         (exprData_getInitNode (data) ) );
1597         break;
1598
1599
1600     case XPR_ASSIGN:
1601         ret = constraintList_addListFree (ret,
1602                                     exprNode_traversTrueEnsuresConstraints
1603                                     (exprData_getOpA (data) ) );
1604
1605        ret = constraintList_addListFree (ret,
1606                                     exprNode_traversTrueEnsuresConstraints
1607                                     (exprData_getOpB (data) ) );
1608        break;
1609     case XPR_OP:
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_SIZEOFT:
1619       break;
1620
1621     case XPR_SIZEOF:
1622
1623        ret = constraintList_addListFree (ret,
1624                                          exprNode_traversTrueEnsuresConstraints
1625                                          (exprData_getSingle (data) ) );
1626        break;
1627
1628     case XPR_CALL:
1629       ret = constraintList_addListFree (ret,
1630                                      exprNode_traversTrueEnsuresConstraints
1631                                     (exprData_getFcn (data) ) );
1632       /*@i11*/  /* exprNodeList_unparse (exprData_getArgs (data) ); */
1633       break;
1634
1635     case XPR_RETURN:
1636       ret = constraintList_addListFree (ret,
1637                                     exprNode_traversTrueEnsuresConstraints
1638                                     (exprData_getSingle (data) ) );
1639       break;
1640
1641     case XPR_NULLRETURN:
1642       break;
1643
1644     case XPR_FACCESS:
1645       ret = constraintList_addListFree (ret,
1646                                         exprNode_traversTrueEnsuresConstraints
1647                                         (exprData_getFieldNode (data) ) );
1648       break;
1649
1650     case XPR_ARROW:
1651       ret = constraintList_addListFree (ret,
1652                                         exprNode_traversTrueEnsuresConstraints
1653                                         (exprData_getFieldNode (data) ) );
1654       break;
1655
1656     case XPR_STRINGLITERAL:
1657       break;
1658
1659     case XPR_NUMLIT:
1660       break;
1661     case XPR_POSTOP:
1662
1663            ret = constraintList_addListFree (ret,
1664                                     exprNode_traversTrueEnsuresConstraints
1665                                     (exprData_getUopNode (data) ) );
1666            break;
1667
1668     case XPR_CAST:
1669
1670       ret = constraintList_addListFree (ret,
1671                                     exprNode_traversTrueEnsuresConstraints
1672                                     (exprData_getCastNode (data) ) );
1673       break;
1674
1675     default:
1676       break;
1677     }
1678
1679   return ret;
1680 }
1681
1682 constraintList exprNode_traversFalseEnsuresConstraints (exprNode e)
1683 {
1684   exprNode t1;
1685   bool handledExprNode;
1686   exprData data;
1687   constraintList ret;
1688
1689    if (exprNode_handleError (e))
1690      {
1691        ret = constraintList_makeNew();
1692        return ret;
1693      }
1694
1695   ret = constraintList_copy (e->falseEnsuresConstraints );
1696
1697    handledExprNode = TRUE;
1698
1699   data = e->edata;
1700
1701   switch (e->kind)
1702     {
1703    case XPR_WHILEPRED:
1704       t1 = exprData_getSingle (data);
1705       ret = constraintList_addListFree ( ret,exprNode_traversFalseEnsuresConstraints (t1) );
1706       break;
1707
1708     case XPR_FETCH:
1709
1710       ret = constraintList_addListFree (ret,
1711                                     exprNode_traversFalseEnsuresConstraints
1712                                     (exprData_getPairA (data) ) );
1713
1714       ret = constraintList_addListFree (ret,
1715                                     exprNode_traversFalseEnsuresConstraints
1716                                     (exprData_getPairB (data) ) );
1717       break;
1718     case XPR_PREOP:
1719
1720       ret = constraintList_addListFree (ret,
1721                                     exprNode_traversFalseEnsuresConstraints
1722                                     (exprData_getUopNode (data) ) );
1723       break;
1724
1725     case XPR_PARENS:
1726       ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints
1727                                     (exprData_getUopNode (data) ) );
1728       break;
1729     case XPR_INIT:
1730         ret = constraintList_addListFree (ret,
1731                                     exprNode_traversFalseEnsuresConstraints
1732                                     (   exprData_getInitNode (data) ) );
1733         break;
1734
1735     case XPR_ASSIGN:
1736         ret = constraintList_addListFree (ret,
1737                                     exprNode_traversFalseEnsuresConstraints
1738                                     (exprData_getOpA (data) ) );
1739
1740        ret = constraintList_addListFree (ret,
1741                                     exprNode_traversFalseEnsuresConstraints
1742                                     (exprData_getOpB (data) ) );
1743        break;
1744     case XPR_OP:
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_SIZEOFT:
1754       break;
1755
1756     case XPR_SIZEOF:
1757
1758        ret = constraintList_addListFree (ret,
1759                                     exprNode_traversFalseEnsuresConstraints
1760                                      (exprData_getSingle (data) ) );
1761        break;
1762
1763     case XPR_CALL:
1764       ret = constraintList_addListFree (ret,
1765                                      exprNode_traversFalseEnsuresConstraints
1766                                     (exprData_getFcn (data) ) );
1767       /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data) ); */
1768       break;
1769
1770     case XPR_RETURN:
1771       ret = constraintList_addListFree (ret,
1772                                     exprNode_traversFalseEnsuresConstraints
1773                                     (exprData_getSingle (data) ) );
1774       break;
1775
1776     case XPR_NULLRETURN:
1777       break;
1778
1779     case XPR_FACCESS:
1780       ret = constraintList_addListFree (ret,
1781                                         exprNode_traversFalseEnsuresConstraints
1782                                         (exprData_getFieldNode (data) ) );
1783       break;
1784
1785     case XPR_ARROW:
1786       ret = constraintList_addListFree (ret,
1787                                         exprNode_traversFalseEnsuresConstraints
1788                                         (exprData_getFieldNode (data) ) );
1789       break;
1790
1791     case XPR_STRINGLITERAL:
1792       break;
1793
1794     case XPR_NUMLIT:
1795       break;
1796     case XPR_POSTOP:
1797
1798            ret = constraintList_addListFree (ret,
1799                                     exprNode_traversFalseEnsuresConstraints
1800                                     (exprData_getUopNode (data) ) );
1801            break;
1802
1803     case XPR_CAST:
1804
1805       ret = constraintList_addListFree (ret,
1806                                     exprNode_traversFalseEnsuresConstraints
1807                                     (exprData_getCastNode (data) ) );
1808       break;
1809
1810     default:
1811       break;
1812     }
1813
1814   return ret;
1815 }
1816
1817
1818 /* walk down the tree and get all requires Constraints in each subexpression*/
1819 /*@only@*/ constraintList exprNode_traversRequiresConstraints (exprNode e)
1820 {
1821   exprNode t1;
1822
1823   bool handledExprNode;
1824   exprData data;
1825   constraintList ret;
1826
1827    if (exprNode_handleError (e))
1828      {
1829        ret = constraintList_makeNew();
1830        return ret;
1831      }
1832   ret = constraintList_copy (e->requiresConstraints );
1833
1834    handledExprNode = TRUE;
1835
1836   data = e->edata;
1837
1838   switch (e->kind)
1839     {
1840    case XPR_WHILEPRED:
1841       t1 = exprData_getSingle (data);
1842       ret = constraintList_addListFree ( ret, exprNode_traversRequiresConstraints (t1) );
1843       break;
1844
1845     case XPR_FETCH:
1846
1847       ret = constraintList_addListFree (ret,
1848                                     exprNode_traversRequiresConstraints
1849                                     (exprData_getPairA (data) ) );
1850
1851       ret = constraintList_addListFree (ret,
1852                                     exprNode_traversRequiresConstraints
1853                                     (exprData_getPairB (data) ) );
1854       break;
1855     case XPR_PREOP:
1856
1857       ret = constraintList_addListFree (ret,
1858                                     exprNode_traversRequiresConstraints
1859                                     (exprData_getUopNode (data) ) );
1860       break;
1861
1862     case XPR_PARENS:
1863       ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints
1864                                     (exprData_getUopNode (data) ) );
1865       break;
1866     case XPR_INIT:
1867       ret = constraintList_addListFree (ret,
1868                                         exprNode_traversRequiresConstraints
1869                                         (exprData_getInitNode (data) ) );
1870         break;
1871
1872     case XPR_ASSIGN:
1873         ret = constraintList_addListFree (ret,
1874                                     exprNode_traversRequiresConstraints
1875                                     (exprData_getOpA (data) ) );
1876
1877        ret = constraintList_addListFree (ret,
1878                                     exprNode_traversRequiresConstraints
1879                                     (exprData_getOpB (data) ) );
1880        break;
1881     case XPR_OP:
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_SIZEOFT:
1891       break;
1892
1893     case XPR_SIZEOF:
1894
1895        ret = constraintList_addListFree (ret,
1896                                     exprNode_traversRequiresConstraints
1897                                      (exprData_getSingle (data) ) );
1898        break;
1899
1900     case XPR_CALL:
1901       ret = constraintList_addListFree (ret,
1902                                      exprNode_traversRequiresConstraints
1903                                     (exprData_getFcn (data) ) );
1904       /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data) ); */
1905       break;
1906
1907     case XPR_RETURN:
1908       ret = constraintList_addListFree (ret,
1909                                     exprNode_traversRequiresConstraints
1910                                     (exprData_getSingle (data) ) );
1911       break;
1912
1913     case XPR_NULLRETURN:
1914       break;
1915
1916     case XPR_FACCESS:
1917       ret = constraintList_addListFree (ret,
1918                                         exprNode_traversRequiresConstraints
1919                                         (exprData_getFieldNode (data) ) );
1920       break;
1921
1922     case XPR_ARROW:
1923       ret = constraintList_addListFree (ret,
1924                                         exprNode_traversRequiresConstraints
1925                                         (exprData_getFieldNode (data) ) );
1926       break;
1927
1928     case XPR_STRINGLITERAL:
1929       break;
1930
1931     case XPR_NUMLIT:
1932       break;
1933     case XPR_POSTOP:
1934
1935            ret = constraintList_addListFree (ret,
1936                                     exprNode_traversRequiresConstraints
1937                                     (exprData_getUopNode (data) ) );
1938            break;
1939
1940     case XPR_CAST:
1941
1942       ret = constraintList_addListFree (ret,
1943                                     exprNode_traversRequiresConstraints
1944                                     (exprData_getCastNode (data) ) );
1945       break;
1946
1947     default:
1948       break;
1949     }
1950
1951   return ret;
1952 }
1953
1954
1955 /* walk down the tree and get all Ensures Constraints in each subexpression*/
1956 /*@only@*/ constraintList exprNode_traversEnsuresConstraints (exprNode e)
1957 {
1958   exprNode t1;
1959
1960   bool handledExprNode;
1961   exprData data;
1962   constraintList ret;
1963
1964
1965    if (exprNode_handleError (e))
1966      {
1967        ret = constraintList_makeNew();
1968        return ret;
1969      }
1970
1971   ret = constraintList_copy (e->ensuresConstraints );
1972    handledExprNode = TRUE;
1973
1974   data = e->edata;
1975
1976   DPRINTF( (message (
1977                      "exprnode_traversEnsuresConstraints call for %s with constraintList of %s",
1978                      exprNode_unparse (e),
1979                      constraintList_print(e->ensuresConstraints)
1980                      )
1981             ));
1982
1983
1984   switch (e->kind)
1985     {
1986    case XPR_WHILEPRED:
1987       t1 = exprData_getSingle (data);
1988       ret = constraintList_addListFree ( ret,exprNode_traversEnsuresConstraints (t1) );
1989       break;
1990
1991     case XPR_FETCH:
1992
1993       ret = constraintList_addListFree (ret,
1994                                     exprNode_traversEnsuresConstraints
1995                                     (exprData_getPairA (data) ) );
1996
1997       ret = constraintList_addListFree (ret,
1998                                     exprNode_traversEnsuresConstraints
1999                                     (exprData_getPairB (data) ) );
2000       break;
2001     case XPR_PREOP:
2002
2003       ret = constraintList_addListFree (ret,
2004                                     exprNode_traversEnsuresConstraints
2005                                     (exprData_getUopNode (data) ) );
2006       break;
2007
2008     case XPR_PARENS:
2009       ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints
2010                                     (exprData_getUopNode (data) ) );
2011       break;
2012
2013     case XPR_INIT:
2014       ret = constraintList_addListFree (ret,
2015                                         exprNode_traversEnsuresConstraints
2016                                         (exprData_getInitNode (data) ) );
2017         break;
2018
2019
2020     case XPR_ASSIGN:
2021         ret = constraintList_addListFree (ret,
2022                                     exprNode_traversEnsuresConstraints
2023                                     (exprData_getOpA (data) ) );
2024
2025        ret = constraintList_addListFree (ret,
2026                                     exprNode_traversEnsuresConstraints
2027                                     (exprData_getOpB (data) ) );
2028        break;
2029     case XPR_OP:
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_SIZEOFT:
2039       break;
2040
2041     case XPR_SIZEOF:
2042
2043        ret = constraintList_addListFree (ret,
2044                                     exprNode_traversEnsuresConstraints
2045                                      (exprData_getSingle (data) ) );
2046        break;
2047
2048     case XPR_CALL:
2049       ret = constraintList_addListFree (ret,
2050                                      exprNode_traversEnsuresConstraints
2051                                     (exprData_getFcn (data) ) );
2052       /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data) ); */
2053       break;
2054
2055     case XPR_RETURN:
2056       ret = constraintList_addListFree (ret,
2057                                     exprNode_traversEnsuresConstraints
2058                                     (exprData_getSingle (data) ) );
2059       break;
2060
2061     case XPR_NULLRETURN:
2062       break;
2063
2064     case XPR_FACCESS:
2065       ret = constraintList_addListFree (ret,
2066                                         exprNode_traversEnsuresConstraints
2067                                         (exprData_getFieldNode (data) ) );
2068       break;
2069
2070     case XPR_ARROW:
2071       ret = constraintList_addListFree (ret,
2072                                         exprNode_traversEnsuresConstraints
2073                                         (exprData_getFieldNode (data) ) );
2074       break;
2075
2076     case XPR_STRINGLITERAL:
2077       break;
2078
2079     case XPR_NUMLIT:
2080       break;
2081     case XPR_POSTOP:
2082
2083            ret = constraintList_addListFree (ret,
2084                                     exprNode_traversEnsuresConstraints
2085                                     (exprData_getUopNode (data) ) );
2086            break;
2087     case XPR_CAST:
2088
2089       ret = constraintList_addListFree (ret,
2090                                     exprNode_traversEnsuresConstraints
2091                                     (exprData_getCastNode (data) ) );
2092       break;
2093
2094     default:
2095       break;
2096     }
2097
2098   DPRINTF( (message (
2099                      "exprnode_traversEnsuresConstraints call for %s with constraintList of  is returning %s",
2100                      exprNode_unparse (e),
2101                      constraintList_print(ret))));
2102
2103   return ret;
2104 }
2105
2106 /*drl moved out of constraintResolve.c 07-02-001 */
2107 void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist, fileloc sequencePoint)
2108 {
2109   temp->requiresConstraints = constraintList_makeNew();
2110   temp->ensuresConstraints = constraintList_makeNew();
2111   temp->trueEnsuresConstraints = constraintList_makeNew();
2112   temp->falseEnsuresConstraints = constraintList_makeNew();
2113
2114   exprNodeList_elements (arglist, el)
2115     {
2116       constraintList temp2;
2117       exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint);
2118       temp2 = el->requiresConstraints;
2119       el->requiresConstraints = exprNode_traversRequiresConstraints(el);
2120       constraintList_free(temp2);
2121
2122       temp2 = el->ensuresConstraints;
2123       el->ensuresConstraints  = exprNode_traversEnsuresConstraints(el);
2124       constraintList_free(temp2);
2125
2126       temp->requiresConstraints = constraintList_addList(temp->requiresConstraints,
2127                                                             el->requiresConstraints);
2128
2129       temp->ensuresConstraints = constraintList_addList(temp->ensuresConstraints,
2130                                                            el->ensuresConstraints);
2131     }
2132   end_exprNodeList_elements;
2133
2134 }
2135
2136 /*drl moved out of constraintResolve.c 07-03-001 */
2137 constraintList exprNode_getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall)
2138 {
2139   constraintList postconditions;
2140   uentry temp;
2141   DPRINTF( (message ("Got call that %s ( %s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (arglist ) ) ) );
2142
2143   temp = exprNode_getUentry (fcn);
2144
2145   postconditions = uentry_getFcnPostconditions (temp);
2146
2147   if (constraintList_isDefined (postconditions))
2148     {
2149       postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist);
2150       postconditions = constraintList_doFixResult (postconditions, fcnCall);
2151     }
2152   else
2153     {
2154       postconditions = constraintList_makeNew();
2155     }
2156
2157   return postconditions;
2158 }
2159
2160
2161 /*drl moved out of constraintResolve.c 07-02-001 */
2162 constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist)
2163 {
2164   constraintList preconditions;
2165   uentry temp;
2166   DPRINTF( (message ("Got call that %s ( %s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (arglist ) ) ) );
2167
2168   temp = exprNode_getUentry (fcn);
2169
2170   preconditions = uentry_getFcnPreconditions (temp);
2171
2172   if (constraintList_isDefined(preconditions) )
2173     {
2174       preconditions = constraintList_togglePost (preconditions);
2175       preconditions = constraintList_preserveCallInfo(preconditions, fcn);
2176       preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist);
2177     }
2178   else
2179     {
2180       if (constraintList_isUndefined(preconditions) )
2181         preconditions = constraintList_makeNew();
2182     }
2183   DPRINTF (( message("Done checkCall\n") ));
2184   DPRINTF (( message("Returning list %q ", constraintList_printDetailed(preconditions) ) ));
2185   return preconditions;
2186 }