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 ("%s\n", constraintList_print(e->requiresConstraints) );
 183   e->ensuresConstraints  = exprNode_traversEnsuresConstraints(snode);
 184   // printf ("Ensures that:\n %s\n", constraintList_print(e->ensuresConstraints) );
 185   llassert(notError);
 186   return notError;
 187
 188 }
 189
 190
 191 bool exprNode_stmtList  (exprNode e)
 192 {
 193   exprNode stmt1, stmt2;
 194   if (exprNode_isError (e) )
 195     {
 196       return FALSE;
 197     }
 198
 199   e->requiresConstraints = constraintList_new();
 200   e->ensuresConstraints  = constraintList_new();
 201
 202   /*Handle case of stmtList with only one statement:
 203    The parse tree stores this as stmt instead of stmtList*/
 204   if (e->kind != XPR_STMTLIST)
 205     {
 206       return exprNode_stmt(e);
 207     }
 208   llassert (e->kind == XPR_STMTLIST);
 209   DPRINTF(( "STMTLIST:") );
 210   DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)) ) );
 211   stmt1 = exprData_getPairA (e->edata);
 212   stmt2 = exprData_getPairB (e->edata);
 213
 214
 215   DPRINTF(("XW        stmtlist       ") );
 216   DPRINTF ((message("XW%s    |        %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2) ) ) );
 217
 218   exprNode_stmt (stmt1);
 219   DPRINTF(("\nstmt after stmtList call " ));
 220
 221   exprNode_stmt (stmt2);
 222   mergeResolve (e, stmt1, stmt2 );
 223   DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n",
 224                       constraintList_print(e->requiresConstraints),
 225                       constraintList_print(e->ensuresConstraints) ) ) );
 226   return TRUE;
 227 }
 228
 229
 230 bool exprNode_multiStatement (exprNode e)
 231 {
 232
 233   bool ret;
 234   exprData data;
 235
 236
 237   DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse( e),
 238                     fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
 239
 240   if (exprNode_handleError (e))
 241     {
 242       return FALSE;
 243     }
 244
 245   data = e->edata;
 246
 247   ret = TRUE;
 248
 249   switch (e->kind)
 250     {
 251
 252     case XPR_FOR:
 253       // ret = message ("%s %s",
 254                      exprNode_generateConstraints (exprData_getPairA (data));
 255                      exprNode_generateConstraints (exprData_getPairB (data));
 256       break;
 257
 258     case XPR_FORPRED:
 259       //            ret = message ("for (%s; %s; %s)",
 260                      exprNode_generateConstraints (exprData_getTripleInit (data));
 261                      exprNode_generateConstraints (exprData_getTripleTest (data));
 262                      exprNode_generateConstraints (exprData_getTripleInc (data));
 263       break;
 264     case XPR_IF:
 265       DPRINTF(( "IF:") );
 266       DPRINTF ((exprNode_unparse(e) ) );
 267       //      ret = message ("if (%s) %s",
 268                      exprNode_generateConstraints (exprData_getPairA (data));
 269                      exprNode_generateConstraints (exprData_getPairB (data));
 270                      //      e->constraints = constraintList_exprNodemerge (exprData_getPairA (data),exprData_getPairB(data));
 271       break;
 272
 273     case XPR_IFELSE:
 274       //      ret = message ("if (%s) %s else %s",
 275                      exprNode_generateConstraints (exprData_getTriplePred (data));
 276                      exprNode_generateConstraints (exprData_getTripleTrue (data));
 277                      exprNode_generateConstraints (exprData_getTripleFalse (data));
 278       break;
 279     case XPR_WHILE:
 280       //      ret = message ("while (%s) %s",
 281                      exprNode_generateConstraints (exprData_getPairA (data));
 282                      exprNode_generateConstraints (exprData_getPairB (data));
 283                      //      e->constraints = constraintList_exprNodemerge (exprData_getPairA (data), exprData_getPairB (data) );
 284       break;
 285
 286     case XPR_WHILEPRED:
 287       // ret =
 288       //        cstring_copy (
 289                       exprNode_generateConstraints (exprData_getSingle (data));
 290       break;
 291
 292     case XPR_DOWHILE:
 293       // ret = message ("do { %s } while (%s)",
 294                      exprNode_generateConstraints (exprData_getPairB (data));
 295                      exprNode_generateConstraints (exprData_getPairA (data));
 296       break;
 297
 298     case XPR_BLOCK:
 299       //      ret = message ("{ %s }",
 300                      exprNode_generateConstraints (exprData_getSingle (data));
 301                      e->requiresConstraints = constraintList_copy ( (exprData_getSingle (data))->requiresConstraints );
 302                      e->ensuresConstraints = constraintList_copy ( (exprData_getSingle (data))->ensuresConstraints );
 303                      //      e->constraints = (exprData_getSingle (data))->constraints;
 304       break;
 305
 306     case XPR_STMT:
 307     case XPR_STMTLIST:
 308       return exprNode_stmtList (e);
 309       /*@notreached@*/
 310       break;
 311     default:
 312       ret=FALSE;
 313     }
 314   return ret;
 315 }
 316
 317
 318 bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv,  fileloc sequencePoint)
 319 {
 320   exprNode t1, t2;
 321
 322   bool handledExprNode;
 323   exprData data;
 324   constraint cons;
 325
 326    DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e),
 327                     fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
 328
 329    e->requiresConstraints = constraintList_new();
 330    e->ensuresConstraints = constraintList_new();
 331
 332    if (exprNode_handleError (e))
 333      {
 334        return FALSE;
 335      }
 336
 337    handledExprNode = TRUE;
 338
 339   data = e->edata;
 340
 341   switch (e->kind)
 342     {
 343
 344     case XPR_FETCH:
 345
 346       if (definatelv )
 347         {
 348           t1 =  (exprData_getPairA (data) );
 349           t2 =  (exprData_getPairB (data) );
 350           cons =  constraint_makeWriteSafeExprNode (t1, t2);
 351         }
 352       else
 353         {
 354           t1 =  (exprData_getPairA (data) );
 355           t2 =  (exprData_getPairB (data) );
 356           cons = constraint_makeReadSafeExprNode (t1, t2 );
 357         }
 358
 359       e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
 360       cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint);
 361       e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
 362       //      cons = constraint_makeEnsureMinReadAtMost (t1, t2, sequencePoint);
 363       // e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
 364
 365       exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
 366       exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
 367
 368             /*@i325 Should check which is array/index. */
 369       break;
 370     case XPR_PREOP:
 371       t1 = exprData_getUopNode(data);
 372       lltok_unparse (exprData_getUopTok (data));
 373       exprNode_exprTraverse (exprData_getUopNode (data), definatelv, definaterv, sequencePoint );
 374       /*handle * pointer access */
 375
 376       /*@ i 325 do ++ and -- */
 377       if (lltok_isMult( exprData_getUopTok (data) ) )
 378         {
 379           if (definatelv)
 380             {
 381               cons = constraint_makeWriteSafeInt (t1, 0);
 382             }
 383           else
 384             {
 385               cons = constraint_makeReadSafeInt (t1, 0);
 386             }
 387               e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
 388         }
 389       if (lltok_isInc_Op (exprData_getUopTok (data) ) )
 390         {
 391           //      cons = constraint_makeSideEffectPostIncrement (t1, sequencePoint);
 392           // e->ensuresConstraints = constraintList_add(e->requiresConstraints, cons);
 393         }
 394       break;
 395
 396     case XPR_PARENS:
 397       exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint);
 398       //    e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined);
 399       break;
 400     case XPR_ASSIGN:
 401       exprNode_exprTraverse (exprData_getOpA (data), TRUE, definaterv, sequencePoint );
 402       lltok_unparse (exprData_getOpTok (data));
 403       exprNode_exprTraverse (exprData_getOpB (data), definatelv, TRUE, sequencePoint );
 404       //  e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data) );
 405       break;
 406     case XPR_OP:
 407       exprNode_exprTraverse (exprData_getOpA (data), definatelv, definaterv, sequencePoint );
 408       lltok_unparse (exprData_getOpTok (data));
 409       exprNode_exprTraverse (exprData_getOpB  (data), definatelv, definaterv, sequencePoint );
 410
 411       //      e->constraints  = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data));
 412       break;
 413     case XPR_SIZEOFT:
 414       ctype_unparse (qtype_getType (exprData_getType (data) ) );
 415
 416       break;
 417
 418     case XPR_SIZEOF:
 419       exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
 420       //      e->constraints = constraintList_exprNodemerge (exprData_getSingle (e->edata), exprNode_undefined);
 421       break;
 422
 423     case XPR_CALL:
 424       exprNode_exprTraverse (exprData_getFcn (data), definatelv, definaterv, sequencePoint );
 425       exprNodeList_unparse (exprData_getArgs (data) );
 426       //      e->constraints = constraintList_add (e->constraints, constraint_create (e,exprNode_undefined, GT,  CALLSAFE ) );
 427       break;
 428
 429     case XPR_RETURN:
 430       exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
 431       break;
 432
 433     case XPR_NULLRETURN:
 434       cstring_makeLiteral ("return");;
 435       break;
 436
 437
 438     case XPR_FACCESS:
 439       exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
 440       exprData_getFieldName (data) ;
 441       break;
 442
 443     case XPR_ARROW:
 444       exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
 445       exprData_getFieldName (data);
 446       break;
 447
 448     case XPR_STRINGLITERAL:
 449       cstring_copy (exprData_getLiteral (data));
 450       break;
 451
 452     case XPR_NUMLIT:
 453       cstring_copy (exprData_getLiteral (data));
 454       break;
 455     case XPR_POSTOP:
 456
 457       exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint );
 458       lltok_unparse (exprData_getUopTok (data));
 459       if (lltok_isInc_Op (exprData_getUopTok (data) ) )
 460         {
 461           DPRINTF(("doing ++"));
 462           t1 = exprData_getUopNode (data);
 463           cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
 464           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
 465           //      cons = constraint_makeMaxReadSideEffectPostIncrement (t1, sequencePoint );
 466           //e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
 467         }
 468       break;
 469     default:
 470       handledExprNode = FALSE;
 471     }
 472
 473   e->requiresConstraints =  constraintList_preserveOrig ( e->requiresConstraints);
 474   e->ensuresConstraints  =  constraintList_preserveOrig ( e->ensuresConstraints);
 475
 476   return handledExprNode;
 477 }
 478
 479 /* walk down the tree and get all requires Constraints in each subexpression*/
 480 constraintList exprNode_traversRequiresConstraints (exprNode e)
 481 {
 482   //  exprNode t1, t2;
 483
 484   bool handledExprNode;
 485   //  char * mes;
 486   exprData data;
 487   constraintList ret;
 488   ret = constraintList_copy (e->requiresConstraints );
 489    if (exprNode_handleError (e))
 490      {
 491        return ret;
 492      }
 493
 494    handledExprNode = TRUE;
 495
 496   data = e->edata;
 497
 498   switch (e->kind)
 499     {
 500
 501     case XPR_FETCH:
 502
 503       ret = constraintList_addList (ret,
 504                                     exprNode_traversRequiresConstraints
 505                                     (exprData_getPairA (data) ) );
 506
 507       ret = constraintList_addList (ret,
 508                                     exprNode_traversRequiresConstraints
 509                                     (exprData_getPairB (data) ) );
 510       break;
 511     case XPR_PREOP:
 512
 513       ret = constraintList_addList (ret,
 514                                     exprNode_traversRequiresConstraints
 515                                     (exprData_getUopNode (data) ) );
 516       break;
 517
 518     case XPR_PARENS:
 519       ret = constraintList_addList (ret, exprNode_traversRequiresConstraints
 520                                     (exprData_getUopNode (data) ) );
 521       break;
 522     case XPR_ASSIGN:
 523         ret = constraintList_addList (ret,
 524                                     exprNode_traversRequiresConstraints
 525                                     (exprData_getOpA (data) ) );
 526
 527        ret = constraintList_addList (ret,
 528                                     exprNode_traversRequiresConstraints
 529                                     (exprData_getOpB (data) ) );
 530        break;
 531     case XPR_OP:
 532        ret = constraintList_addList (ret,
 533                                     exprNode_traversRequiresConstraints
 534                                     (exprData_getOpA (data) ) );
 535
 536        ret = constraintList_addList (ret,
 537                                     exprNode_traversRequiresConstraints
 538                                     (exprData_getOpB (data) ) );
 539        break;
 540     case XPR_SIZEOFT:
 541
 542       //      ctype_unparse (qtype_getType (exprData_getType (data) ) );
 543
 544       break;
 545
 546     case XPR_SIZEOF:
 547
 548        ret = constraintList_addList (ret,
 549                                     exprNode_traversRequiresConstraints
 550                                      (exprData_getSingle (data) ) );
 551        break;
 552
 553     case XPR_CALL:
 554       ret = constraintList_addList (ret,
 555                                      exprNode_traversRequiresConstraints
 556                                     (exprData_getFcn (data) ) );
 557       /*@i11*/      //   exprNodeList_unparse (exprData_getArgs (data) );
 558          break;
 559
 560     case XPR_RETURN:
 561       ret = constraintList_addList (ret,
 562                                     exprNode_traversRequiresConstraints
 563                                     (exprData_getSingle (data) ) );
 564       break;
 565
 566     case XPR_NULLRETURN:
 567       //      cstring_makeLiteral ("return");;
 568       break;
 569
 570     case XPR_FACCESS:
 571           ret = constraintList_addList (ret,
 572                                     exprNode_traversRequiresConstraints
 573                                     (exprData_getFieldNode (data) ) );
 574        //exprData_getFieldName (data) ;
 575       break;
 576
 577     case XPR_ARROW:
 578         ret = constraintList_addList (ret,
 579                                     exprNode_traversRequiresConstraints
 580                                     (exprData_getFieldNode (data) ) );
 581         //      exprData_getFieldName (data);
 582       break;
 583
 584     case XPR_STRINGLITERAL:
 585       //      cstring_copy (exprData_getLiteral (data));
 586       break;
 587
 588     case XPR_NUMLIT:
 589       //      cstring_copy (exprData_getLiteral (data));
 590       break;
 591     case XPR_POSTOP:
 592
 593            ret = constraintList_addList (ret,
 594                                     exprNode_traversRequiresConstraints
 595                                     (exprData_getUopNode (data) ) );
 596            break;
 597     default:
 598       break;
 599     }
 600
 601   return ret;
 602 }
 603
 604
 605 /* walk down the tree and get all Ensures Constraints in each subexpression*/
 606 constraintList exprNode_traversEnsuresConstraints (exprNode e)
 607 {
 608   //  exprNode t1, t2;
 609
 610   bool handledExprNode;
 611   //  char * mes;
 612   exprData data;
 613   //  constraintExpr tmp;
 614   //  constraint cons;
 615   constraintList ret;
 616   ret = constraintList_copy (e->ensuresConstraints );
 617    if (exprNode_handleError (e))
 618      {
 619        return ret;
 620      }
 621
 622    handledExprNode = TRUE;
 623
 624   data = e->edata;
 625
 626   DPRINTF( (message (
 627                      "exprnode_traversEnsuresConstraints call for %s with constraintList of %s",
 628                      exprNode_unparse (e),
 629                      constraintList_print(e->ensuresConstraints)
 630                      )
 631             ));
 632
 633
 634   switch (e->kind)
 635     {
 636
 637     case XPR_FETCH:
 638
 639       ret = constraintList_addList (ret,
 640                                     exprNode_traversEnsuresConstraints
 641                                     (exprData_getPairA (data) ) );
 642
 643       ret = constraintList_addList (ret,
 644                                     exprNode_traversEnsuresConstraints
 645                                     (exprData_getPairB (data) ) );
 646       break;
 647     case XPR_PREOP:
 648
 649       ret = constraintList_addList (ret,
 650                                     exprNode_traversEnsuresConstraints
 651                                     (exprData_getUopNode (data) ) );
 652       break;
 653
 654     case XPR_PARENS:
 655       ret = constraintList_addList (ret, exprNode_traversEnsuresConstraints
 656                                     (exprData_getUopNode (data) ) );
 657       break;
 658     case XPR_ASSIGN:
 659         ret = constraintList_addList (ret,
 660                                     exprNode_traversEnsuresConstraints
 661                                     (exprData_getOpA (data) ) );
 662
 663        ret = constraintList_addList (ret,
 664                                     exprNode_traversEnsuresConstraints
 665                                     (exprData_getOpB (data) ) );
 666        break;
 667     case XPR_OP:
 668        ret = constraintList_addList (ret,
 669                                     exprNode_traversEnsuresConstraints
 670                                     (exprData_getOpA (data) ) );
 671
 672        ret = constraintList_addList (ret,
 673                                     exprNode_traversEnsuresConstraints
 674                                     (exprData_getOpB (data) ) );
 675        break;
 676     case XPR_SIZEOFT:
 677
 678       //      ctype_unparse (qtype_getType (exprData_getType (data) ) );
 679
 680       break;
 681
 682     case XPR_SIZEOF:
 683
 684        ret = constraintList_addList (ret,
 685                                     exprNode_traversEnsuresConstraints
 686                                      (exprData_getSingle (data) ) );
 687        break;
 688
 689     case XPR_CALL:
 690       ret = constraintList_addList (ret,
 691                                      exprNode_traversEnsuresConstraints
 692                                     (exprData_getFcn (data) ) );
 693       /*@i11*/      //   exprNodeList_unparse (exprData_getArgs (data) );
 694          break;
 695
 696     case XPR_RETURN:
 697       ret = constraintList_addList (ret,
 698                                     exprNode_traversEnsuresConstraints
 699                                     (exprData_getSingle (data) ) );
 700       break;
 701
 702     case XPR_NULLRETURN:
 703       //      cstring_makeLiteral ("return");;
 704       break;
 705
 706     case XPR_FACCESS:
 707           ret = constraintList_addList (ret,
 708                                     exprNode_traversEnsuresConstraints
 709                                     (exprData_getFieldNode (data) ) );
 710        //exprData_getFieldName (data) ;
 711       break;
 712
 713     case XPR_ARROW:
 714         ret = constraintList_addList (ret,
 715                                     exprNode_traversEnsuresConstraints
 716                                     (exprData_getFieldNode (data) ) );
 717         //      exprData_getFieldName (data);
 718       break;
 719
 720     case XPR_STRINGLITERAL:
 721       //      cstring_copy (exprData_getLiteral (data));
 722       break;
 723
 724     case XPR_NUMLIT:
 725       //      cstring_copy (exprData_getLiteral (data));
 726       break;
 727     case XPR_POSTOP:
 728
 729            ret = constraintList_addList (ret,
 730                                     exprNode_traversEnsuresConstraints
 731                                     (exprData_getUopNode (data) ) );
 732            break;
 733     default:
 734       break;
 735     }
 736 DPRINTF( (message (
 737                      "exprnode_traversEnsuresConstraints call for %s with constraintList of  is returning %s",
 738                      exprNode_unparse (e),
 739              //              constraintList_print(e->ensuresConstraints),
 740                      constraintList_print(ret)
 741                      )
 742             ));
 743
 744
 745   return ret;
 746 }
 747