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
1208   if (exprNode_isUnhandled (e) )
1209      {
1210        return; // FALSE;
1211      }
1212    //   e = makeDataTypeConstraints (e);
1213
1214    handledExprNode = TRUE;
1215
1216   data = e->edata;
1217
1218   switch (e->kind)
1219     {
1220     case XPR_WHILEPRED:
1221       t1 = exprData_getSingle (data);
1222       exprNode_exprTraverse (t1,  definatelv, definaterv, sequencePoint);
1223       e = exprNode_copyConstraints (e, t1);
1224       break;
1225
1226     case XPR_FETCH:
1227
1228       if (definatelv )
1229         {
1230           t1 =  (exprData_getPairA (data) );
1231           t2 =  (exprData_getPairB (data) );
1232           cons =  constraint_makeWriteSafeExprNode (t1, t2);
1233         }
1234       else
1235         {
1236           t1 =  (exprData_getPairA (data) );
1237           t2 =  (exprData_getPairB (data) );
1238           cons = constraint_makeReadSafeExprNode (t1, t2 );
1239         }
1240
1241       e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
1242       cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint);
1243       e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1244
1245       cons = constraint_makeEnsureLteMaxRead (t2, t1);
1246       e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1247
1248       //      cons = constraint_makeEnsureMinReadAtMost (t1, t2, sequencePoint);
1249       // e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1250
1251       exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
1252       exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
1253
1254             /*@i325 Should check which is array/index. */
1255       break;
1256
1257     case XPR_PARENS:
1258       exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint);
1259       //    e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined);
1260       break;
1261     case XPR_INIT:
1262       {
1263         /*
1264         idDecl t;
1265
1266         uentry ue;
1267         exprNode lhs;
1268
1269         t = exprData_getInitId (data);
1270         ue = usymtab_lookup (idDecl_observeId (t));
1271         lhs = exprNode_createId (ue);
1272         */
1273         t2 = exprData_getInitNode (data);
1274
1275         /*      DPRINTF(( (message("initialization: %s = %s",
1276                            exprNode_unparse(lhs),
1277                            exprNode_unparse(t2)
1278                            )
1279                    ) ));        */
1280
1281         //exprNode_exprTraverse (t1, TRUE, FALSE, sequencePoint );
1282
1283         exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
1284
1285         /* this test is nessecary because some expressions generate a null expression node.  function pointer do that -- drl */
1286         if ( (!exprNode_isError (e))  &&  (!exprNode_isError(t2)) )
1287           {
1288             cons =  constraint_makeEnsureEqual (e, t2, sequencePoint);
1289             e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1290           }
1291       }
1292
1293       break;
1294     case XPR_ASSIGN:
1295       t1 = exprData_getOpA (data);
1296       t2 = exprData_getOpB (data);
1297       exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
1298       //lltok_unparse (exprData_getOpTok (data));
1299
1300       exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
1301
1302       /* this test is nessecary because some expressions generate a null expression node.  function pointer do that -- drl */
1303       if ( (!exprNode_isError (t1))  &&  (!exprNode_isError(t2)) )
1304         {
1305           cons =  constraint_makeEnsureEqual (t1, t2, sequencePoint);
1306           e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1307         }
1308       break;
1309     case XPR_OP:
1310       t1 = exprData_getOpA (data);
1311       t2 = exprData_getOpB (data);
1312       tok = exprData_getOpTok (data);
1313
1314
1315       if (tok.tok == ADD_ASSIGN)
1316         {
1317           exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
1318           exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
1319
1320           cons = constraint_makeAddAssign (t1, t2,  sequencePoint );
1321           e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1322         }
1323       else if (tok.tok == SUB_ASSIGN)
1324         {
1325           exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
1326           exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
1327
1328           cons = constraint_makeSubtractAssign (t1, t2,  sequencePoint );
1329           e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1330         }
1331       else
1332         {
1333           exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
1334           exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
1335         }
1336
1337       if (lltok_isBoolean_Op (tok) )
1338         exprNode_booleanTraverse (e, definatelv, definaterv, sequencePoint);
1339
1340       //      e->constraints  = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data));
1341       break;
1342     case XPR_SIZEOFT:
1343       //drl possible problem : warning make sure the case can be ignored..
1344
1345       break;
1346
1347     case XPR_SIZEOF:
1348       /* drl  7-16-01
1349          C standard says operand to sizeof isn't evaluated unless
1350          its a variable length array.  So we don't generate constraints.
1351       */
1352
1353       //      exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
1354       //      e->constraints = constraintList_exprNodemerge (exprData_getSingle (e->edata), exprNode_undefined);
1355       break;
1356
1357     case XPR_CALL:
1358       fcn = exprData_getFcn(data);
1359
1360       exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint );
1361       DPRINTF ( (message ("Got call that %s ( %s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (exprData_getArgs (data) ) ) ) );
1362
1363       fcn->requiresConstraints = constraintList_addListFree (fcn->requiresConstraints,
1364                                                  checkCall (fcn, exprData_getArgs (data)  ) );
1365
1366       fcn->ensuresConstraints = constraintList_addListFree (fcn->ensuresConstraints,
1367                                                  exprNode_getPostConditions(fcn, exprData_getArgs (data),e  ) );
1368
1369       t1 = exprNode_createNew (exprNode_getType (e) );
1370
1371       checkArgumentList (t1, exprData_getArgs(data), sequencePoint);
1372
1373
1374       exprNode_mergeResolve (e, t1, fcn);
1375
1376       exprNode_free(t1);
1377
1378       //      e->constraints = constraintList_add (e->constraints, constraint_create (e,exprNode_undefined, GT,  CALLSAFE ) );
1379
1380       break;
1381
1382     case XPR_RETURN:
1383       exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
1384       break;
1385
1386     case XPR_NULLRETURN:
1387
1388       break;
1389
1390
1391     case XPR_FACCESS:
1392       exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
1393       break;
1394
1395     case XPR_ARROW:
1396       exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
1397       break;
1398
1399     case XPR_STRINGLITERAL:
1400
1401       break;
1402
1403     case XPR_NUMLIT:
1404
1405       break;
1406
1407     case XPR_PREOP:
1408       t1 = exprData_getUopNode(data);
1409       tok = (exprData_getUopTok (data));
1410       //lltok_unparse (exprData_getUopTok (data));
1411       exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
1412       /*handle * pointer access */
1413       if (lltok_isInc_Op (tok) )
1414         {
1415           DPRINTF(("doing ++(var)"));
1416           t1 = exprData_getUopNode (data);
1417           cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
1418           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1419         }
1420       else if (lltok_isDec_Op (tok) )
1421         {
1422           DPRINTF(("doing --(var)"));
1423           t1 = exprData_getUopNode (data);
1424           cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint );
1425           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1426         }
1427       else if (lltok_isMult( tok  ) )
1428         {
1429           if (definatelv)
1430             {
1431               cons = constraint_makeWriteSafeInt (t1, 0);
1432             }
1433           else
1434             {
1435               cons = constraint_makeReadSafeInt (t1, 0);
1436             }
1437               e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
1438         }
1439       else if (lltok_isNot_Op (tok) )
1440         /* ! expr */
1441         {
1442           constraintList_free(e->trueEnsuresConstraints);
1443
1444           e->trueEnsuresConstraints  = constraintList_copy (t1->falseEnsuresConstraints);
1445           constraintList_free(e->falseEnsuresConstraints);
1446           e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints);
1447         }
1448
1449       else if (lltok_isAmpersand_Op (tok) )
1450         {
1451           break;
1452         }
1453       else if (lltok_isMinus_Op (tok) )
1454         {
1455           break;
1456         }
1457       else if ( lltok_isExcl_Op (tok) )
1458         {
1459           break;
1460         }
1461       else if (lltok_isTilde_Op (tok) )
1462         {
1463           break;
1464         }
1465       else
1466         {
1467           llcontbug((message("Unsupported preop in %s", exprNode_unparse(e) ) ));
1468           BADEXIT;
1469         }
1470       break;
1471
1472     case XPR_POSTOP:
1473
1474       exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint );
1475
1476       if (lltok_isInc_Op (exprData_getUopTok (data) ) )
1477         {
1478           DPRINTF(("doing ++"));
1479           t1 = exprData_getUopNode (data);
1480           cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
1481           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1482         }
1483        if (lltok_isDec_Op (exprData_getUopTok (data) ) )
1484         {
1485           DPRINTF(("doing --"));
1486           t1 = exprData_getUopNode (data);
1487           cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint );
1488           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1489         }
1490       break;
1491     case XPR_CAST:
1492       {
1493         t2 =  exprData_getCastNode (data);
1494         DPRINTF (( message ("Examining cast (%q)%s",
1495                             qtype_unparse (exprData_getCastType (data)),
1496                             exprNode_unparse (t2) )
1497                    ));
1498         exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
1499       }
1500       break;
1501
1502     case XPR_COND:
1503       {
1504         exprNode pred, trueBranch, falseBranch;
1505            llassert(FALSE);
1506       pred = exprData_getTriplePred (data);
1507       trueBranch = exprData_getTripleTrue (data);
1508       falseBranch = exprData_getTripleFalse (data);
1509
1510       exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint );
1511
1512       temp =       pred->ensuresConstraints;
1513       pred->ensuresConstraints = exprNode_traversEnsuresConstraints(pred);
1514       constraintList_free(temp);
1515
1516       temp =       pred->requiresConstraints;
1517       pred->requiresConstraints = exprNode_traversRequiresConstraints(pred);
1518       constraintList_free(temp);
1519
1520       temp =       pred->trueEnsuresConstraints;
1521       pred->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(pred);
1522       constraintList_free(temp);
1523
1524       temp =       pred->falseEnsuresConstraints;
1525       pred->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(pred);
1526       constraintList_free(temp);
1527
1528
1529       exprNode_exprTraverse (trueBranch, FALSE, TRUE, sequencePoint );
1530
1531       temp =       trueBranch->ensuresConstraints;
1532       trueBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(trueBranch);
1533       constraintList_free(temp);
1534
1535
1536       temp =       trueBranch->requiresConstraints;
1537       trueBranch->requiresConstraints = exprNode_traversRequiresConstraints(trueBranch);
1538       constraintList_free(temp);
1539
1540
1541       temp =       trueBranch->trueEnsuresConstraints;
1542       trueBranch->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(trueBranch);
1543       constraintList_free(temp);
1544
1545       temp =       trueBranch->falseEnsuresConstraints;
1546       trueBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(trueBranch);
1547       constraintList_free(temp);
1548
1549       //dfdf
1550       exprNode_exprTraverse (falseBranch, FALSE, TRUE, sequencePoint );
1551
1552       temp =       falseBranch->ensuresConstraints;
1553       falseBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(falseBranch);
1554       constraintList_free(temp);
1555
1556
1557       temp =       falseBranch->requiresConstraints;
1558       falseBranch->requiresConstraints = exprNode_traversRequiresConstraints(falseBranch);
1559       constraintList_free(temp);
1560
1561
1562       temp =       falseBranch->trueEnsuresConstraints;
1563       falseBranch->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(falseBranch);
1564       constraintList_free(temp);
1565
1566       temp =       falseBranch->falseEnsuresConstraints;
1567       falseBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(falseBranch);
1568       constraintList_free(temp);
1569
1570       /* if pred is true e equals true otherwise pred equals false */
1571
1572       cons =  constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
1573       trueBranch->ensuresConstraints = constraintList_add(trueBranch->ensuresConstraints, cons);
1574
1575       cons =  constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
1576       falseBranch->ensuresConstraints = constraintList_add(falseBranch->ensuresConstraints, cons);
1577
1578       e = doIfElse (e, pred, trueBranch, falseBranch);
1579
1580       }
1581       break;
1582     case XPR_COMMA:
1583       llassert(FALSE);
1584       t1 = exprData_getPairA (data);
1585       t2 = exprData_getPairB (data);
1586     /* we essiantially treat this like expr1; expr2
1587      of course sequencePoint isn't adjusted so this isn't completely accurate
1588     problems../  */
1589       exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint );
1590       exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
1591       exprNode_mergeResolve (e, t1, t2);
1592       break;
1593
1594     default:
1595       handledExprNode = FALSE;
1596     }
1597
1598   e->requiresConstraints =  constraintList_preserveOrig ( e->requiresConstraints);
1599   e->ensuresConstraints  =  constraintList_preserveOrig ( e->ensuresConstraints);
1600   e->requiresConstraints = constraintList_addGeneratingExpr ( e->requiresConstraints, e);
1601
1602   e->ensuresConstraints  = constraintList_addGeneratingExpr ( e->ensuresConstraints, e);
1603
1604
1605   e->requiresConstraints = constraintList_removeSurpressed( e->requiresConstraints);
1606
1607   DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) ));
1608
1609   DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) ));
1610
1611   DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->trueEnsuresConstraints) ) ));
1612
1613   DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->falseEnsuresConstraints) ) ));
1614
1615   return; // handledExprNode;
1616 }
1617
1618
1619 constraintList exprNode_traversTrueEnsuresConstraints (exprNode e)
1620 {
1621   exprNode t1;
1622
1623   bool handledExprNode;
1624   //  char * mes;
1625   exprData data;
1626   constraintList ret;
1627
1628   if (exprNode_handleError (e))
1629     {
1630       ret = constraintList_makeNew();
1631       return ret;
1632     }
1633   ret = constraintList_copy (e->trueEnsuresConstraints );
1634
1635   handledExprNode = TRUE;
1636
1637   data = e->edata;
1638
1639   switch (e->kind)
1640     {
1641     case XPR_WHILEPRED:
1642       t1 = exprData_getSingle (data);
1643       ret = constraintList_addListFree ( ret, exprNode_traversTrueEnsuresConstraints (t1) );
1644       break;
1645
1646     case XPR_FETCH:
1647
1648       ret = constraintList_addListFree (ret,
1649                                     exprNode_traversTrueEnsuresConstraints
1650                                     (exprData_getPairA (data) ) );
1651
1652       ret = constraintList_addListFree (ret,
1653                                     exprNode_traversTrueEnsuresConstraints
1654                                     (exprData_getPairB (data) ) );
1655       break;
1656     case XPR_PREOP:
1657
1658       ret = constraintList_addListFree (ret,
1659                                     exprNode_traversTrueEnsuresConstraints
1660                                     (exprData_getUopNode (data) ) );
1661       break;
1662
1663     case XPR_PARENS:
1664       ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints
1665                                     (exprData_getUopNode (data) ) );
1666       break;
1667
1668     case XPR_INIT:
1669       ret = constraintList_addListFree (ret,
1670                                         exprNode_traversTrueEnsuresConstraints
1671                                         (exprData_getInitNode (data) ) );
1672         break;
1673
1674
1675     case XPR_ASSIGN:
1676         ret = constraintList_addListFree (ret,
1677                                     exprNode_traversTrueEnsuresConstraints
1678                                     (exprData_getOpA (data) ) );
1679
1680        ret = constraintList_addListFree (ret,
1681                                     exprNode_traversTrueEnsuresConstraints
1682                                     (exprData_getOpB (data) ) );
1683        break;
1684     case XPR_OP:
1685        ret = constraintList_addListFree (ret,
1686                                     exprNode_traversTrueEnsuresConstraints
1687                                     (exprData_getOpA (data) ) );
1688
1689        ret = constraintList_addListFree (ret,
1690                                     exprNode_traversTrueEnsuresConstraints
1691                                     (exprData_getOpB (data) ) );
1692        break;
1693     case XPR_SIZEOFT:
1694
1695       //      ctype_unparse (qtype_getType (exprData_getType (data) ) );
1696
1697       break;
1698
1699     case XPR_SIZEOF:
1700
1701        ret = constraintList_addListFree (ret,
1702                                          exprNode_traversTrueEnsuresConstraints
1703                                          (exprData_getSingle (data) ) );
1704        break;
1705
1706     case XPR_CALL:
1707       ret = constraintList_addListFree (ret,
1708                                      exprNode_traversTrueEnsuresConstraints
1709                                     (exprData_getFcn (data) ) );
1710       /*@i11*/      //   exprNodeList_unparse (exprData_getArgs (data) );
1711          break;
1712
1713     case XPR_RETURN:
1714       ret = constraintList_addListFree (ret,
1715                                     exprNode_traversTrueEnsuresConstraints
1716                                     (exprData_getSingle (data) ) );
1717       break;
1718
1719     case XPR_NULLRETURN:
1720       //      cstring_makeLiteral ("return");;
1721       break;
1722
1723     case XPR_FACCESS:
1724           ret = constraintList_addListFree (ret,
1725                                     exprNode_traversTrueEnsuresConstraints
1726                                     (exprData_getFieldNode (data) ) );
1727        //exprData_getFieldName (data) ;
1728       break;
1729
1730     case XPR_ARROW:
1731         ret = constraintList_addListFree (ret,
1732                                     exprNode_traversTrueEnsuresConstraints
1733                                     (exprData_getFieldNode (data) ) );
1734         //      exprData_getFieldName (data);
1735       break;
1736
1737     case XPR_STRINGLITERAL:
1738       //      cstring_copy (exprData_getLiteral (data));
1739       break;
1740
1741     case XPR_NUMLIT:
1742       //      cstring_copy (exprData_getLiteral (data));
1743       break;
1744     case XPR_POSTOP:
1745
1746            ret = constraintList_addListFree (ret,
1747                                     exprNode_traversTrueEnsuresConstraints
1748                                     (exprData_getUopNode (data) ) );
1749            break;
1750
1751     case XPR_CAST:
1752
1753       ret = constraintList_addListFree (ret,
1754                                     exprNode_traversTrueEnsuresConstraints
1755                                     (exprData_getCastNode (data) ) );
1756       break;
1757
1758     default:
1759       break;
1760     }
1761
1762   return ret;
1763 }
1764
1765 constraintList exprNode_traversFalseEnsuresConstraints (exprNode e)
1766 {
1767    exprNode t1;
1768
1769   bool handledExprNode;
1770   //  char * mes;
1771   exprData data;
1772   constraintList ret;
1773
1774    if (exprNode_handleError (e))
1775      {
1776        ret = constraintList_makeNew();
1777        return ret;
1778      }
1779   ret = constraintList_copy (e->falseEnsuresConstraints );
1780
1781    handledExprNode = TRUE;
1782
1783   data = e->edata;
1784
1785   switch (e->kind)
1786     {
1787    case XPR_WHILEPRED:
1788       t1 = exprData_getSingle (data);
1789       ret = constraintList_addListFree ( ret,exprNode_traversFalseEnsuresConstraints (t1) );
1790       break;
1791
1792     case XPR_FETCH:
1793
1794       ret = constraintList_addListFree (ret,
1795                                     exprNode_traversFalseEnsuresConstraints
1796                                     (exprData_getPairA (data) ) );
1797
1798       ret = constraintList_addListFree (ret,
1799                                     exprNode_traversFalseEnsuresConstraints
1800                                     (exprData_getPairB (data) ) );
1801       break;
1802     case XPR_PREOP:
1803
1804       ret = constraintList_addListFree (ret,
1805                                     exprNode_traversFalseEnsuresConstraints
1806                                     (exprData_getUopNode (data) ) );
1807       break;
1808
1809     case XPR_PARENS:
1810       ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints
1811                                     (exprData_getUopNode (data) ) );
1812       break;
1813     case XPR_INIT:
1814         ret = constraintList_addListFree (ret,
1815                                     exprNode_traversFalseEnsuresConstraints
1816                                     (   exprData_getInitNode (data) ) );
1817         break;
1818
1819     case XPR_ASSIGN:
1820         ret = constraintList_addListFree (ret,
1821                                     exprNode_traversFalseEnsuresConstraints
1822                                     (exprData_getOpA (data) ) );
1823
1824        ret = constraintList_addListFree (ret,
1825                                     exprNode_traversFalseEnsuresConstraints
1826                                     (exprData_getOpB (data) ) );
1827        break;
1828     case XPR_OP:
1829        ret = constraintList_addListFree (ret,
1830                                     exprNode_traversFalseEnsuresConstraints
1831                                     (exprData_getOpA (data) ) );
1832
1833        ret = constraintList_addListFree (ret,
1834                                     exprNode_traversFalseEnsuresConstraints
1835                                     (exprData_getOpB (data) ) );
1836        break;
1837     case XPR_SIZEOFT:
1838
1839       //      ctype_unparse (qtype_getType (exprData_getType (data) ) );
1840
1841       break;
1842
1843     case XPR_SIZEOF:
1844
1845        ret = constraintList_addListFree (ret,
1846                                     exprNode_traversFalseEnsuresConstraints
1847                                      (exprData_getSingle (data) ) );
1848        break;
1849
1850     case XPR_CALL:
1851       ret = constraintList_addListFree (ret,
1852                                      exprNode_traversFalseEnsuresConstraints
1853                                     (exprData_getFcn (data) ) );
1854       /*@i11*/      //   exprNodeList_unparse (exprData_getArgs (data) );
1855          break;
1856
1857     case XPR_RETURN:
1858       ret = constraintList_addListFree (ret,
1859                                     exprNode_traversFalseEnsuresConstraints
1860                                     (exprData_getSingle (data) ) );
1861       break;
1862
1863     case XPR_NULLRETURN:
1864       //      cstring_makeLiteral ("return");;
1865       break;
1866
1867     case XPR_FACCESS:
1868           ret = constraintList_addListFree (ret,
1869                                     exprNode_traversFalseEnsuresConstraints
1870                                     (exprData_getFieldNode (data) ) );
1871        //exprData_getFieldName (data) ;
1872       break;
1873
1874     case XPR_ARROW:
1875         ret = constraintList_addListFree (ret,
1876                                     exprNode_traversFalseEnsuresConstraints
1877                                     (exprData_getFieldNode (data) ) );
1878         //      exprData_getFieldName (data);
1879       break;
1880
1881     case XPR_STRINGLITERAL:
1882       //      cstring_copy (exprData_getLiteral (data));
1883       break;
1884
1885     case XPR_NUMLIT:
1886       //      cstring_copy (exprData_getLiteral (data));
1887       break;
1888     case XPR_POSTOP:
1889
1890            ret = constraintList_addListFree (ret,
1891                                     exprNode_traversFalseEnsuresConstraints
1892                                     (exprData_getUopNode (data) ) );
1893            break;
1894
1895     case XPR_CAST:
1896
1897       ret = constraintList_addListFree (ret,
1898                                     exprNode_traversFalseEnsuresConstraints
1899                                     (exprData_getCastNode (data) ) );
1900       break;
1901
1902     default:
1903       break;
1904     }
1905
1906   return ret;
1907 }
1908
1909
1910 /* walk down the tree and get all requires Constraints in each subexpression*/
1911 /*@only@*/ constraintList exprNode_traversRequiresConstraints (exprNode e)
1912 {
1913   exprNode t1;
1914
1915   bool handledExprNode;
1916   //  char * mes;
1917   exprData data;
1918   constraintList ret;
1919
1920    if (exprNode_handleError (e))
1921      {
1922        ret = constraintList_makeNew();
1923        return ret;
1924      }
1925   ret = constraintList_copy (e->requiresConstraints );
1926
1927    handledExprNode = TRUE;
1928
1929   data = e->edata;
1930
1931   switch (e->kind)
1932     {
1933    case XPR_WHILEPRED:
1934       t1 = exprData_getSingle (data);
1935       ret = constraintList_addListFree ( ret, exprNode_traversRequiresConstraints (t1) );
1936       break;
1937
1938     case XPR_FETCH:
1939
1940       ret = constraintList_addListFree (ret,
1941                                     exprNode_traversRequiresConstraints
1942                                     (exprData_getPairA (data) ) );
1943
1944       ret = constraintList_addListFree (ret,
1945                                     exprNode_traversRequiresConstraints
1946                                     (exprData_getPairB (data) ) );
1947       break;
1948     case XPR_PREOP:
1949
1950       ret = constraintList_addListFree (ret,
1951                                     exprNode_traversRequiresConstraints
1952                                     (exprData_getUopNode (data) ) );
1953       break;
1954
1955     case XPR_PARENS:
1956       ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints
1957                                     (exprData_getUopNode (data) ) );
1958       break;
1959     case XPR_INIT:
1960       ret = constraintList_addListFree (ret,
1961                                         exprNode_traversRequiresConstraints
1962                                         (exprData_getInitNode (data) ) );
1963         break;
1964
1965     case XPR_ASSIGN:
1966         ret = constraintList_addListFree (ret,
1967                                     exprNode_traversRequiresConstraints
1968                                     (exprData_getOpA (data) ) );
1969
1970        ret = constraintList_addListFree (ret,
1971                                     exprNode_traversRequiresConstraints
1972                                     (exprData_getOpB (data) ) );
1973        break;
1974     case XPR_OP:
1975        ret = constraintList_addListFree (ret,
1976                                     exprNode_traversRequiresConstraints
1977                                     (exprData_getOpA (data) ) );
1978
1979        ret = constraintList_addListFree (ret,
1980                                     exprNode_traversRequiresConstraints
1981                                     (exprData_getOpB (data) ) );
1982        break;
1983     case XPR_SIZEOFT:
1984
1985       //      ctype_unparse (qtype_getType (exprData_getType (data) ) );
1986
1987       break;
1988
1989     case XPR_SIZEOF:
1990
1991        ret = constraintList_addListFree (ret,
1992                                     exprNode_traversRequiresConstraints
1993                                      (exprData_getSingle (data) ) );
1994        break;
1995
1996     case XPR_CALL:
1997       ret = constraintList_addListFree (ret,
1998                                      exprNode_traversRequiresConstraints
1999                                     (exprData_getFcn (data) ) );
2000       /*@i11*/      //   exprNodeList_unparse (exprData_getArgs (data) );
2001          break;
2002
2003     case XPR_RETURN:
2004       ret = constraintList_addListFree (ret,
2005                                     exprNode_traversRequiresConstraints
2006                                     (exprData_getSingle (data) ) );
2007       break;
2008
2009     case XPR_NULLRETURN:
2010       //      cstring_makeLiteral ("return");;
2011       break;
2012
2013     case XPR_FACCESS:
2014           ret = constraintList_addListFree (ret,
2015                                     exprNode_traversRequiresConstraints
2016                                     (exprData_getFieldNode (data) ) );
2017        //exprData_getFieldName (data) ;
2018       break;
2019
2020     case XPR_ARROW:
2021         ret = constraintList_addListFree (ret,
2022                                     exprNode_traversRequiresConstraints
2023                                     (exprData_getFieldNode (data) ) );
2024         //      exprData_getFieldName (data);
2025       break;
2026
2027     case XPR_STRINGLITERAL:
2028       //      cstring_copy (exprData_getLiteral (data));
2029       break;
2030
2031     case XPR_NUMLIT:
2032       //      cstring_copy (exprData_getLiteral (data));
2033       break;
2034     case XPR_POSTOP:
2035
2036            ret = constraintList_addListFree (ret,
2037                                     exprNode_traversRequiresConstraints
2038                                     (exprData_getUopNode (data) ) );
2039            break;
2040
2041     case XPR_CAST:
2042
2043       ret = constraintList_addListFree (ret,
2044                                     exprNode_traversRequiresConstraints
2045                                     (exprData_getCastNode (data) ) );
2046       break;
2047
2048     default:
2049       break;
2050     }
2051
2052   return ret;
2053 }
2054
2055
2056 /* walk down the tree and get all Ensures Constraints in each subexpression*/
2057 /*@only@*/ constraintList exprNode_traversEnsuresConstraints (exprNode e)
2058 {
2059   exprNode t1;
2060
2061   bool handledExprNode;
2062   //  char * mes;
2063   exprData data;
2064   //  constraintExpr tmp;
2065   //  constraint cons;
2066   constraintList ret;
2067
2068
2069    if (exprNode_handleError (e))
2070      {
2071        ret = constraintList_makeNew();
2072        return ret;
2073      }
2074
2075   ret = constraintList_copy (e->ensuresConstraints );
2076    handledExprNode = TRUE;
2077
2078   data = e->edata;
2079
2080   DPRINTF( (message (
2081                      "exprnode_traversEnsuresConstraints call for %s with constraintList of %s",
2082                      exprNode_unparse (e),
2083                      constraintList_print(e->ensuresConstraints)
2084                      )
2085             ));
2086
2087
2088   switch (e->kind)
2089     {
2090    case XPR_WHILEPRED:
2091       t1 = exprData_getSingle (data);
2092       ret = constraintList_addListFree ( ret,exprNode_traversEnsuresConstraints (t1) );
2093       break;
2094
2095     case XPR_FETCH:
2096
2097       ret = constraintList_addListFree (ret,
2098                                     exprNode_traversEnsuresConstraints
2099                                     (exprData_getPairA (data) ) );
2100
2101       ret = constraintList_addListFree (ret,
2102                                     exprNode_traversEnsuresConstraints
2103                                     (exprData_getPairB (data) ) );
2104       break;
2105     case XPR_PREOP:
2106
2107       ret = constraintList_addListFree (ret,
2108                                     exprNode_traversEnsuresConstraints
2109                                     (exprData_getUopNode (data) ) );
2110       break;
2111
2112     case XPR_PARENS:
2113       ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints
2114                                     (exprData_getUopNode (data) ) );
2115       break;
2116
2117     case XPR_INIT:
2118       ret = constraintList_addListFree (ret,
2119                                         exprNode_traversEnsuresConstraints
2120                                         (exprData_getInitNode (data) ) );
2121         break;
2122
2123
2124     case XPR_ASSIGN:
2125         ret = constraintList_addListFree (ret,
2126                                     exprNode_traversEnsuresConstraints
2127                                     (exprData_getOpA (data) ) );
2128
2129        ret = constraintList_addListFree (ret,
2130                                     exprNode_traversEnsuresConstraints
2131                                     (exprData_getOpB (data) ) );
2132        break;
2133     case XPR_OP:
2134        ret = constraintList_addListFree (ret,
2135                                     exprNode_traversEnsuresConstraints
2136                                     (exprData_getOpA (data) ) );
2137
2138        ret = constraintList_addListFree (ret,
2139                                     exprNode_traversEnsuresConstraints
2140                                     (exprData_getOpB (data) ) );
2141        break;
2142     case XPR_SIZEOFT:
2143
2144       //      ctype_unparse (qtype_getType (exprData_getType (data) ) );
2145
2146       break;
2147
2148     case XPR_SIZEOF:
2149
2150        ret = constraintList_addListFree (ret,
2151                                     exprNode_traversEnsuresConstraints
2152                                      (exprData_getSingle (data) ) );
2153        break;
2154
2155     case XPR_CALL:
2156       ret = constraintList_addListFree (ret,
2157                                      exprNode_traversEnsuresConstraints
2158                                     (exprData_getFcn (data) ) );
2159       /*@i11*/      //   exprNodeList_unparse (exprData_getArgs (data) );
2160          break;
2161
2162     case XPR_RETURN:
2163       ret = constraintList_addListFree (ret,
2164                                     exprNode_traversEnsuresConstraints
2165                                     (exprData_getSingle (data) ) );
2166       break;
2167
2168     case XPR_NULLRETURN:
2169       //      cstring_makeLiteral ("return");;
2170       break;
2171
2172     case XPR_FACCESS:
2173           ret = constraintList_addListFree (ret,
2174                                     exprNode_traversEnsuresConstraints
2175                                     (exprData_getFieldNode (data) ) );
2176        //exprData_getFieldName (data) ;
2177       break;
2178
2179     case XPR_ARROW:
2180         ret = constraintList_addListFree (ret,
2181                                     exprNode_traversEnsuresConstraints
2182                                     (exprData_getFieldNode (data) ) );
2183         //      exprData_getFieldName (data);
2184       break;
2185
2186     case XPR_STRINGLITERAL:
2187       //      cstring_copy (exprData_getLiteral (data));
2188       break;
2189
2190     case XPR_NUMLIT:
2191       //      cstring_copy (exprData_getLiteral (data));
2192       break;
2193     case XPR_POSTOP:
2194
2195            ret = constraintList_addListFree (ret,
2196                                     exprNode_traversEnsuresConstraints
2197                                     (exprData_getUopNode (data) ) );
2198            break;
2199     case XPR_CAST:
2200
2201       ret = constraintList_addListFree (ret,
2202                                     exprNode_traversEnsuresConstraints
2203                                     (exprData_getCastNode (data) ) );
2204       break;
2205
2206     default:
2207       break;
2208     }
2209 DPRINTF( (message (
2210                      "exprnode_traversEnsuresConstraints call for %s with constraintList of  is returning %s",
2211                      exprNode_unparse (e),
2212              //              constraintList_print(e->ensuresConstraints),
2213                      constraintList_print(ret)
2214                      )
2215             ));
2216
2217
2218   return ret;
2219 }
2220
2221 /*drl moved out of constraintResolve.c 07-02-001 */
2222 void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist, fileloc sequencePoint)
2223 {
2224   temp->requiresConstraints = constraintList_makeNew();
2225   temp->ensuresConstraints = constraintList_makeNew();
2226   temp->trueEnsuresConstraints = constraintList_makeNew();
2227   temp->falseEnsuresConstraints = constraintList_makeNew();
2228
2229   exprNodeList_elements (arglist, el)
2230     {
2231       constraintList temp2;
2232       exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint);
2233       temp2 = el->requiresConstraints;
2234       el->requiresConstraints = exprNode_traversRequiresConstraints(el);
2235       constraintList_free(temp2);
2236
2237       temp2 = el->ensuresConstraints;
2238       el->ensuresConstraints  = exprNode_traversEnsuresConstraints(el);
2239       constraintList_free(temp2);
2240
2241       temp->requiresConstraints = constraintList_addList(temp->requiresConstraints,
2242                                                             el->requiresConstraints);
2243
2244       temp->ensuresConstraints = constraintList_addList(temp->ensuresConstraints,
2245                                                            el->ensuresConstraints);
2246     }
2247   end_exprNodeList_elements;
2248
2249 }
2250
2251 /*drl moved out of constraintResolve.c 07-03-001 */
2252 constraintList exprNode_getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall)
2253 {
2254   constraintList postconditions;
2255   uentry temp;
2256   DPRINTF( (message ("Got call that %s ( %s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (arglist ) ) ) );
2257
2258   temp = exprNode_getUentry (fcn);
2259
2260   postconditions = uentry_getFcnPostconditions (temp);
2261
2262   if (constraintList_isDefined (postconditions))
2263     {
2264       postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist);
2265       postconditions = constraintList_doFixResult (postconditions, fcnCall);
2266     }
2267   else
2268     {
2269       postconditions = constraintList_makeNew();
2270     }
2271
2272   return postconditions;
2273 }
2274
2275
2276 /*drl moved out of constraintResolve.c 07-02-001 */
2277 constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist)
2278 {
2279   constraintList preconditions;
2280   uentry temp;
2281   DPRINTF( (message ("Got call that %s ( %s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (arglist ) ) ) );
2282
2283   temp = exprNode_getUentry (fcn);
2284
2285   preconditions = uentry_getFcnPreconditions (temp);
2286
2287   if (constraintList_isDefined(preconditions) )
2288     {
2289       preconditions = constraintList_togglePost (preconditions);
2290       preconditions = constraintList_preserveCallInfo(preconditions, fcn);
2291       preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist);
2292     }
2293   else
2294     {
2295       if (constraintList_isUndefined(preconditions) )
2296         preconditions = constraintList_makeNew();
2297     }
2298   DPRINTF (( message("Done checkCall\n") ));
2299   DPRINTF (( message("Returning list %q ", constraintList_printDetailed(preconditions) ) ));
2300   return preconditions;
2301 }