src/constraintGeneration.c

   1
   2 /*
   3 ** constraintList.c
   4 */
   5
   6 # include <ctype.h> /* for isdigit */
   7 # include "lclintMacros.nf"
   8 # include "basic.h"
   9 # include "cgrammar.h"
  10 # include "cgrammar_tokens.h"
  11
  12 # include "exprChecks.h"
  13 # include "aliasChecks.h"
  14 # include "exprNodeSList.h"
  15 # include "exprData.i"
  16
  17 void /*@alt bool@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e);
  18 static bool exprNode_handleError( exprNode p_e);
  19
  20 //static cstring exprNode_findConstraints ( exprNode p_e);
  21 static bool exprNode_isMultiStatement(exprNode p_e);
  22 static bool exprNode_multiStatement (exprNode p_e);
  23 bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv,  fileloc sequencePoint);
  24 //static void exprNode_constraintPropagateUp (exprNode p_e);
  25 constraintList exprNode_traversRequiresConstraints (exprNode e);
  26 constraintList exprNode_traversEnsuresConstraints (exprNode e);
  27 void mergeResolve (exprNode parent, exprNode child1, exprNode child2);
  28
  29
  30
  31 bool exprNode_isUnhandled (exprNode e)
  32 {
  33   llassert( exprNode_isDefined(e) );
  34   switch (e->kind)
  35     {
  36     case XPR_INITBLOCK:
  37     case XPR_EMPTY:
  38     case XPR_LABEL:
  39     case XPR_CONST:
  40     case XPR_VAR:
  41     case XPR_BODY:
  42     case XPR_OFFSETOF:
  43     case XPR_ALIGNOFT:
  44     case XPR_ALIGNOF:
  45     case XPR_VAARG:
  46     case XPR_ITERCALL:
  47     case XPR_ITER:
  48     case XPR_CAST:
  49     case XPR_GOTO:
  50     case XPR_CONTINUE:
  51     case XPR_BREAK:
  52     case XPR_COMMA:
  53     case XPR_COND:
  54     case XPR_TOK:
  55     case XPR_FTDEFAULT:
  56     case XPR_DEFAULT:
  57     case XPR_SWITCH:
  58     case XPR_FTCASE:
  59     case XPR_CASE:
  60     case XPR_INIT:
  61     case XPR_NODE:
  62       DPRINTF((message ("Warning current constraint generation does not handle expression %s", exprNode_unparse(e)) ) );
  63       return FALSE;
  64       /*@notreached@*/
  65       break;
  66     default:
  67       return TRUE;
  68
  69     }
  70   /*not reached*/
  71   return FALSE;
  72 }
  73
  74 bool exprNode_handleError( exprNode e)
  75 {
  76    if (exprNode_isError (e) || !exprNode_isUnhandled(e) )
  77     {
  78       static /*@only@*/ cstring error = cstring_undefined;
  79
  80       if (!cstring_isDefined (error))
  81         {
  82           error = cstring_makeLiteral ("<error>");
  83         }
  84
  85       /*@-unqualifiedtrans*/ return TRUE; /*@=unqualifiedtrans*/
  86     }
  87    return FALSE;
  88 }
  89
  90 void /*@alt bool@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e)
  91 {
  92   DPRINTF((message ("exprNode_gnerateConstraints Analysising %s %s at", exprNode_unparse( e),
  93                     fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
  94
  95   if (exprNode_isMultiStatement ( e) )
  96     {
  97       exprNode_multiStatement(e);
  98     }
  99   else
 100     {
 101       llassert(FALSE);
 102     }
 103   printf ("%s", (message ("%s", constraintList_printDetailed (e->requiresConstraints) ) ) );
 104   printf ("%s", (message ("%s", constraintList_printDetailed (e->ensuresConstraints) ) ) );
 105   return FALSE;
 106 }
 107
 108
 109 /* handles multiple statements */
 110
 111 bool exprNode_isMultiStatement(exprNode e)
 112 {
 113 if (exprNode_handleError (e) != NULL)
 114   return FALSE;
 115
 116   switch (e->kind)
 117     {
 118     case XPR_FOR:
 119     case XPR_FORPRED:
 120     case XPR_IF:
 121     case XPR_IFELSE:
 122     case XPR_WHILE:
 123     case XPR_WHILEPRED:
 124     case XPR_DOWHILE:
 125     case XPR_BLOCK:
 126     case XPR_STMT:
 127     case XPR_STMTLIST:
 128       return TRUE;
 129     default:
 130       return FALSE;
 131     }
 132
 133 }
 134
 135 bool exprNode_stmt (exprNode e)
 136 {
 137   exprNode snode;
 138   fileloc loc;
 139   bool notError;
 140
 141   if (exprNode_isError(e) )
 142     {
 143       return FALSE;
 144     }
 145   e->requiresConstraints = constraintList_new();
 146   e->ensuresConstraints  = constraintList_new();
 147
 148
 149   DPRINTF(( "STMT:") );
 150   DPRINTF ( ( cstring_toCharsSafe ( exprNode_unparse(e)) )
 151            );
 152   if (e->kind != XPR_STMT)
 153     {
 154
 155       DPRINTF (("Not Stmt") );
 156       DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
 157       if (exprNode_isMultiStatement (e) )
 158         {
 159           return exprNode_multiStatement (e );
 160         }
 161       llassert(FALSE);
 162     }
 163
 164   DPRINTF (("Stmt") );
 165   DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
 166
 167   snode = exprData_getUopNode (e->edata);
 168
 169   /* could be stmt involving multiple statements:
 170      i.e. if, while for ect.
 171   */
 172
 173   if (exprNode_isMultiStatement (snode))
 174     {
 175       llassert(FALSE);
 176       return exprNode_multiStatement (snode);
 177     }
 178
 179   loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
 180   notError = exprNode_exprTraverse (snode, FALSE, FALSE, loc);
 181   e->requiresConstraints = exprNode_traversRequiresConstraints(snode);
 182   printf ("For: %s \n", exprNode_unparse (e) );
 183   printf ("%s\n", constraintList_print(e->requiresConstraints) );
 184   e->ensuresConstraints  = exprNode_traversEnsuresConstraints(snode);
 185   printf ("Ensures that:\n %s\n", constraintList_print(e->ensuresConstraints) );
 186   llassert(notError);
 187   return notError;
 188
 189 }
 190
 191
 192 bool exprNode_stmtList  (exprNode e)
 193 {
 194   exprNode stmt1, stmt2;
 195   if (exprNode_isError (e) )
 196     {
 197       return FALSE;
 198     }
 199
 200   e->requiresConstraints = constraintList_new();
 201   e->ensuresConstraints  = constraintList_new();
 202
 203   /*Handle case of stmtList with only one statement:
 204    The parse tree stores this as stmt instead of stmtList*/
 205   if (e->kind != XPR_STMTLIST)
 206     {
 207       return exprNode_stmt(e);
 208     }
 209   llassert (e->kind == XPR_STMTLIST);
 210   DPRINTF(( "STMTLIST:") );
 211   DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)) ) );
 212   stmt1 = exprData_getPairA (e->edata);
 213   stmt2 = exprData_getPairB (e->edata);
 214
 215
 216   DPRINTF(("XW        stmtlist       ") );
 217   DPRINTF ((message("XW%s    |        %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2) ) ) );
 218
 219   exprNode_stmt (stmt1);
 220   DPRINTF(("\nstmt after stmtList call " ));
 221
 222   exprNode_stmt (stmt2);
 223   mergeResolve (e, stmt1, stmt2 );
 224
 225   DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n",
 226                       constraintList_print(e->requiresConstraints),
 227                       constraintList_print(e->ensuresConstraints) ) ) );
 228   return TRUE;
 229 }
 230
 231
 232 bool exprNode_multiStatement (exprNode e)
 233 {
 234
 235   bool ret;
 236   exprData data;
 237
 238
 239   DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse( e),
 240                     fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
 241
 242   if (exprNode_handleError (e))
 243     {
 244       return FALSE;
 245     }
 246
 247   data = e->edata;
 248
 249   ret = TRUE;
 250
 251   switch (e->kind)
 252     {
 253
 254     case XPR_FOR:
 255       // ret = message ("%s %s",
 256                      exprNode_generateConstraints (exprData_getPairA (data));
 257                      exprNode_generateConstraints (exprData_getPairB (data));
 258       break;
 259
 260     case XPR_FORPRED:
 261       //            ret = message ("for (%s; %s; %s)",
 262                      exprNode_generateConstraints (exprData_getTripleInit (data));
 263                      exprNode_generateConstraints (exprData_getTripleTest (data));
 264                      exprNode_generateConstraints (exprData_getTripleInc (data));
 265       break;
 266     case XPR_IF:
 267       DPRINTF(( "IF:") );
 268       DPRINTF ((exprNode_unparse(e) ) );
 269       //      ret = message ("if (%s) %s",
 270                      exprNode_generateConstraints (exprData_getPairA (data));
 271                      exprNode_generateConstraints (exprData_getPairB (data));
 272                      //      e->constraints = constraintList_exprNodemerge (exprData_getPairA (data),exprData_getPairB(data));
 273       break;
 274
 275     case XPR_IFELSE:
 276       //      ret = message ("if (%s) %s else %s",
 277                      exprNode_generateConstraints (exprData_getTriplePred (data));
 278                      exprNode_generateConstraints (exprData_getTripleTrue (data));
 279                      exprNode_generateConstraints (exprData_getTripleFalse (data));
 280       break;
 281     case XPR_WHILE:
 282       //      ret = message ("while (%s) %s",
 283                      exprNode_generateConstraints (exprData_getPairA (data));
 284                      exprNode_generateConstraints (exprData_getPairB (data));
 285                      //      e->constraints = constraintList_exprNodemerge (exprData_getPairA (data), exprData_getPairB (data) );
 286       break;
 287
 288     case XPR_WHILEPRED:
 289       // ret =
 290       //        cstring_copy (
 291                       exprNode_generateConstraints (exprData_getSingle (data));
 292       break;
 293
 294     case XPR_DOWHILE:
 295       // ret = message ("do { %s } while (%s)",
 296                      exprNode_generateConstraints (exprData_getPairB (data));
 297                      exprNode_generateConstraints (exprData_getPairA (data));
 298       break;
 299
 300     case XPR_BLOCK:
 301       //      ret = message ("{ %s }",
 302                      exprNode_generateConstraints (exprData_getSingle (data));
 303                      e->requiresConstraints = constraintList_copy ( (exprData_getSingle (data))->requiresConstraints );
 304                      e->ensuresConstraints = constraintList_copy ( (exprData_getSingle (data))->ensuresConstraints );
 305                      //      e->constraints = (exprData_getSingle (data))->constraints;
 306       break;
 307
 308     case XPR_STMT:
 309     case XPR_STMTLIST:
 310       return exprNode_stmtList (e);
 311       /*@notreached@*/
 312       break;
 313     default:
 314       ret=FALSE;
 315     }
 316   return ret;
 317 }
 318
 319
 320 bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv,  fileloc sequencePoint)
 321 {
 322   exprNode t1, t2;
 323
 324   bool handledExprNode;
 325   exprData data;
 326   constraint cons;
 327
 328    DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e),
 329                     fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
 330
 331    e->requiresConstraints = constraintList_new();
 332    e->ensuresConstraints = constraintList_new();
 333
 334    if (exprNode_handleError (e))
 335      {
 336        return FALSE;
 337      }
 338
 339    handledExprNode = TRUE;
 340
 341   data = e->edata;
 342
 343   switch (e->kind)
 344     {
 345
 346     case XPR_FETCH:
 347
 348       if (definatelv )
 349         {
 350           t1 =  (exprData_getPairA (data) );
 351           t2 =  (exprData_getPairB (data) );
 352           cons =  constraint_makeWriteSafeExprNode (t1, t2);
 353         }
 354       else
 355         {
 356           t1 =  (exprData_getPairA (data) );
 357           t2 =  (exprData_getPairB (data) );
 358           cons = constraint_makeReadSafeExprNode (t1, t2 );
 359         }
 360
 361       e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
 362       cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint);
 363       e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
 364       //      cons = constraint_makeEnsureMinReadAtMost (t1, t2, sequencePoint);
 365       // e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
 366
 367       exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
 368       exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
 369
 370             /*@i325 Should check which is array/index. */
 371       break;
 372     case XPR_PREOP:
 373       t1 = exprData_getUopNode(data);
 374       lltok_unparse (exprData_getUopTok (data));
 375       exprNode_exprTraverse (exprData_getUopNode (data), definatelv, definaterv, sequencePoint );
 376       /*handle * pointer access */
 377
 378       /*@ i 325 do ++ and -- */
 379       if (lltok_isMult( exprData_getUopTok (data) ) )
 380         {
 381           if (definatelv)
 382             {
 383               cons = constraint_makeWriteSafeInt (t1, 0);
 384             }
 385           else
 386             {
 387               cons = constraint_makeReadSafeInt (t1, 0);
 388             }
 389               e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
 390         }
 391       if (lltok_isInc_Op (exprData_getUopTok (data) ) )
 392         {
 393           //      cons = constraint_makeSideEffectPostIncrement (t1, sequencePoint);
 394           // e->ensuresConstraints = constraintList_add(e->requiresConstraints, cons);
 395         }
 396       break;
 397
 398     case XPR_PARENS:
 399       exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint);
 400       //    e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined);
 401       break;
 402     case XPR_ASSIGN:
 403       exprNode_exprTraverse (exprData_getOpA (data), TRUE, definaterv, sequencePoint );
 404       lltok_unparse (exprData_getOpTok (data));
 405       exprNode_exprTraverse (exprData_getOpB (data), definatelv, TRUE, sequencePoint );
 406       //  e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data) );
 407       break;
 408     case XPR_OP:
 409       exprNode_exprTraverse (exprData_getOpA (data), definatelv, definaterv, sequencePoint );
 410       lltok_unparse (exprData_getOpTok (data));
 411       exprNode_exprTraverse (exprData_getOpB  (data), definatelv, definaterv, sequencePoint );
 412
 413       //      e->constraints  = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data));
 414       break;
 415     case XPR_SIZEOFT:
 416       ctype_unparse (qtype_getType (exprData_getType (data) ) );
 417
 418       break;
 419
 420     case XPR_SIZEOF:
 421       exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
 422       //      e->constraints = constraintList_exprNodemerge (exprData_getSingle (e->edata), exprNode_undefined);
 423       break;
 424
 425     case XPR_CALL:
 426       exprNode_exprTraverse (exprData_getFcn (data), definatelv, definaterv, sequencePoint );
 427       exprNodeList_unparse (exprData_getArgs (data) );
 428       //      e->constraints = constraintList_add (e->constraints, constraint_create (e,exprNode_undefined, GT,  CALLSAFE ) );
 429       break;
 430
 431     case XPR_RETURN:
 432       exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
 433       break;
 434
 435     case XPR_NULLRETURN:
 436       cstring_makeLiteral ("return");;
 437       break;
 438
 439
 440     case XPR_FACCESS:
 441       exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
 442       exprData_getFieldName (data) ;
 443       break;
 444
 445     case XPR_ARROW:
 446       exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
 447       exprData_getFieldName (data);
 448       break;
 449
 450     case XPR_STRINGLITERAL:
 451       cstring_copy (exprData_getLiteral (data));
 452       break;
 453
 454     case XPR_NUMLIT:
 455       cstring_copy (exprData_getLiteral (data));
 456       break;
 457     case XPR_POSTOP:
 458
 459       exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint );
 460       lltok_unparse (exprData_getUopTok (data));
 461       if (lltok_isInc_Op (exprData_getUopTok (data) ) )
 462         {
 463           DPRINTF(("doing ++"));
 464           t1 = exprData_getUopNode (data);
 465           cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
 466           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
 467           //      cons = constraint_makeMaxReadSideEffectPostIncrement (t1, sequencePoint );
 468           //e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
 469         }
 470       break;
 471     default:
 472       handledExprNode = FALSE;
 473     }
 474
 475   e->requiresConstraints =  constraintList_preserveOrig ( e->requiresConstraints);
 476   e->ensuresConstraints  =  constraintList_preserveOrig ( e->ensuresConstraints);
 477
 478   return handledExprNode;
 479 }
 480
 481 /* walk down the tree and get all requires Constraints in each subexpression*/
 482 constraintList exprNode_traversRequiresConstraints (exprNode e)
 483 {
 484   //  exprNode t1, t2;
 485
 486   bool handledExprNode;
 487   //  char * mes;
 488   exprData data;
 489   constraintList ret;
 490   ret = constraintList_copy (e->requiresConstraints );
 491    if (exprNode_handleError (e))
 492      {
 493        return ret;
 494      }
 495
 496    handledExprNode = TRUE;
 497
 498   data = e->edata;
 499
 500   switch (e->kind)
 501     {
 502
 503     case XPR_FETCH:
 504
 505       ret = constraintList_addList (ret,
 506                                     exprNode_traversRequiresConstraints
 507                                     (exprData_getPairA (data) ) );
 508
 509       ret = constraintList_addList (ret,
 510                                     exprNode_traversRequiresConstraints
 511                                     (exprData_getPairB (data) ) );
 512       break;
 513     case XPR_PREOP:
 514
 515       ret = constraintList_addList (ret,
 516                                     exprNode_traversRequiresConstraints
 517                                     (exprData_getUopNode (data) ) );
 518       break;
 519
 520     case XPR_PARENS:
 521       ret = constraintList_addList (ret, exprNode_traversRequiresConstraints
 522                                     (exprData_getUopNode (data) ) );
 523       break;
 524     case XPR_ASSIGN:
 525         ret = constraintList_addList (ret,
 526                                     exprNode_traversRequiresConstraints
 527                                     (exprData_getOpA (data) ) );
 528
 529        ret = constraintList_addList (ret,
 530                                     exprNode_traversRequiresConstraints
 531                                     (exprData_getOpB (data) ) );
 532        break;
 533     case XPR_OP:
 534        ret = constraintList_addList (ret,
 535                                     exprNode_traversRequiresConstraints
 536                                     (exprData_getOpA (data) ) );
 537
 538        ret = constraintList_addList (ret,
 539                                     exprNode_traversRequiresConstraints
 540                                     (exprData_getOpB (data) ) );
 541        break;
 542     case XPR_SIZEOFT:
 543
 544       //      ctype_unparse (qtype_getType (exprData_getType (data) ) );
 545
 546       break;
 547
 548     case XPR_SIZEOF:
 549
 550        ret = constraintList_addList (ret,
 551                                     exprNode_traversRequiresConstraints
 552                                      (exprData_getSingle (data) ) );
 553        break;
 554
 555     case XPR_CALL:
 556       ret = constraintList_addList (ret,
 557                                      exprNode_traversRequiresConstraints
 558                                     (exprData_getFcn (data) ) );
 559       /*@i11*/      //   exprNodeList_unparse (exprData_getArgs (data) );
 560          break;
 561
 562     case XPR_RETURN:
 563       ret = constraintList_addList (ret,
 564                                     exprNode_traversRequiresConstraints
 565                                     (exprData_getSingle (data) ) );
 566       break;
 567
 568     case XPR_NULLRETURN:
 569       //      cstring_makeLiteral ("return");;
 570       break;
 571
 572     case XPR_FACCESS:
 573           ret = constraintList_addList (ret,
 574                                     exprNode_traversRequiresConstraints
 575                                     (exprData_getFieldNode (data) ) );
 576        //exprData_getFieldName (data) ;
 577       break;
 578
 579     case XPR_ARROW:
 580         ret = constraintList_addList (ret,
 581                                     exprNode_traversRequiresConstraints
 582                                     (exprData_getFieldNode (data) ) );
 583         //      exprData_getFieldName (data);
 584       break;
 585
 586     case XPR_STRINGLITERAL:
 587       //      cstring_copy (exprData_getLiteral (data));
 588       break;
 589
 590     case XPR_NUMLIT:
 591       //      cstring_copy (exprData_getLiteral (data));
 592       break;
 593     case XPR_POSTOP:
 594
 595            ret = constraintList_addList (ret,
 596                                     exprNode_traversRequiresConstraints
 597                                     (exprData_getUopNode (data) ) );
 598            break;
 599     default:
 600       break;
 601     }
 602
 603   return ret;
 604 }
 605
 606
 607 /* walk down the tree and get all Ensures Constraints in each subexpression*/
 608 constraintList exprNode_traversEnsuresConstraints (exprNode e)
 609 {
 610   //  exprNode t1, t2;
 611
 612   bool handledExprNode;
 613   //  char * mes;
 614   exprData data;
 615   //  constraintExpr tmp;
 616   //  constraint cons;
 617   constraintList ret;
 618   ret = constraintList_copy (e->ensuresConstraints );
 619    if (exprNode_handleError (e))
 620      {
 621        return ret;
 622      }
 623
 624    handledExprNode = TRUE;
 625
 626   data = e->edata;
 627
 628   DPRINTF( (message (
 629                      "exprnode_traversEnsuresConstraints call for %s with constraintList of %s",
 630                      exprNode_unparse (e),
 631                      constraintList_print(e->ensuresConstraints)
 632                      )
 633             ));
 634
 635
 636   switch (e->kind)
 637     {
 638
 639     case XPR_FETCH:
 640
 641       ret = constraintList_addList (ret,
 642                                     exprNode_traversEnsuresConstraints
 643                                     (exprData_getPairA (data) ) );
 644
 645       ret = constraintList_addList (ret,
 646                                     exprNode_traversEnsuresConstraints
 647                                     (exprData_getPairB (data) ) );
 648       break;
 649     case XPR_PREOP:
 650
 651       ret = constraintList_addList (ret,
 652                                     exprNode_traversEnsuresConstraints
 653                                     (exprData_getUopNode (data) ) );
 654       break;
 655
 656     case XPR_PARENS:
 657       ret = constraintList_addList (ret, exprNode_traversEnsuresConstraints
 658                                     (exprData_getUopNode (data) ) );
 659       break;
 660     case XPR_ASSIGN:
 661         ret = constraintList_addList (ret,
 662                                     exprNode_traversEnsuresConstraints
 663                                     (exprData_getOpA (data) ) );
 664
 665        ret = constraintList_addList (ret,
 666                                     exprNode_traversEnsuresConstraints
 667                                     (exprData_getOpB (data) ) );
 668        break;
 669     case XPR_OP:
 670        ret = constraintList_addList (ret,
 671                                     exprNode_traversEnsuresConstraints
 672                                     (exprData_getOpA (data) ) );
 673
 674        ret = constraintList_addList (ret,
 675                                     exprNode_traversEnsuresConstraints
 676                                     (exprData_getOpB (data) ) );
 677        break;
 678     case XPR_SIZEOFT:
 679
 680       //      ctype_unparse (qtype_getType (exprData_getType (data) ) );
 681
 682       break;
 683
 684     case XPR_SIZEOF:
 685
 686        ret = constraintList_addList (ret,
 687                                     exprNode_traversEnsuresConstraints
 688                                      (exprData_getSingle (data) ) );
 689        break;
 690
 691     case XPR_CALL:
 692       ret = constraintList_addList (ret,
 693                                      exprNode_traversEnsuresConstraints
 694                                     (exprData_getFcn (data) ) );
 695       /*@i11*/      //   exprNodeList_unparse (exprData_getArgs (data) );
 696          break;
 697
 698     case XPR_RETURN:
 699       ret = constraintList_addList (ret,
 700                                     exprNode_traversEnsuresConstraints
 701                                     (exprData_getSingle (data) ) );
 702       break;
 703
 704     case XPR_NULLRETURN:
 705       //      cstring_makeLiteral ("return");;
 706       break;
 707
 708     case XPR_FACCESS:
 709           ret = constraintList_addList (ret,
 710                                     exprNode_traversEnsuresConstraints
 711                                     (exprData_getFieldNode (data) ) );
 712        //exprData_getFieldName (data) ;
 713       break;
 714
 715     case XPR_ARROW:
 716         ret = constraintList_addList (ret,
 717                                     exprNode_traversEnsuresConstraints
 718                                     (exprData_getFieldNode (data) ) );
 719         //      exprData_getFieldName (data);
 720       break;
 721
 722     case XPR_STRINGLITERAL:
 723       //      cstring_copy (exprData_getLiteral (data));
 724       break;
 725
 726     case XPR_NUMLIT:
 727       //      cstring_copy (exprData_getLiteral (data));
 728       break;
 729     case XPR_POSTOP:
 730
 731            ret = constraintList_addList (ret,
 732                                     exprNode_traversEnsuresConstraints
 733                                     (exprData_getUopNode (data) ) );
 734            break;
 735     default:
 736       break;
 737     }
 738 DPRINTF( (message (
 739                      "exprnode_traversEnsuresConstraints call for %s with constraintList of  is returning %s",
 740                      exprNode_unparse (e),
 741              //              constraintList_print(e->ensuresConstraints),
 742                      constraintList_print(ret)
 743                      )
 744             ));
 745
 746
 747   return ret;
 748 }
 749