src/constraintGeneration.c

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