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