Fixed Makefile to create bin directory.

[splint.git] / src / constraintGeneration.c

/*
** constraintGeneration.c
*/

/* #define DEBUGPRINT 1 */

# include <ctype.h> /* for isdigit */
# include "lclintMacros.nf"
# include "basic.h"

# include "cgrammar_tokens.h"

# include "exprChecks.h"
# include "exprNodeSList.h"

/*@access exprNode @*/


static bool exprNode_handleError(/*@dependent@*/ exprNode p_e);

static bool exprNode_isMultiStatement(/*@dependent@*/ exprNode p_e);
static void  exprNode_multiStatement (/*@dependent@*/ exprNode p_e);

static constraintList exprNode_traversTrueEnsuresConstraints (/*@dependent@*/ exprNode p_e);
static constraintList exprNode_traversFalseEnsuresConstraints (/*@dependent@*/ exprNode p_e);

static void checkArgumentList (/*@out@*/ exprNode p_temp, exprNodeList p_arglist, fileloc p_sequencePoint) /*@modifies p_temp @*/;

static  constraintList checkCall (/*@dependent@*/ exprNode p_fcn, exprNodeList p_arglist);

static bool exprNode_isUnhandled (/*@dependent@*/ /*@observer@*/ exprNode e)
{
  llassert( exprNode_isDefined(e) );
  switch (e->kind)
    {
    case XPR_INITBLOCK:
    case XPR_EMPTY:
    case XPR_LABEL:
    case XPR_CONST:
    case XPR_VAR:
    case XPR_BODY:
    case XPR_OFFSETOF:
    case XPR_ALIGNOFT:
    case XPR_ALIGNOF:
    case XPR_VAARG:
    case XPR_ITERCALL:
    case XPR_ITER:
    case XPR_GOTO:
    case XPR_CONTINUE:
    case XPR_BREAK:
    case XPR_COMMA:
    case XPR_COND:
    case XPR_TOK:
    case XPR_FTDEFAULT:
    case XPR_DEFAULT:
    case XPR_FTCASE:
    case XPR_CASE:
    case XPR_NODE:
      DPRINTF((message ("Warning current constraint generation does not handle expression %s", exprNode_unparse(e)) ) );
      return TRUE;
      /*@notreached@*/
      break;
    default:
      return FALSE;
      
    }
  /*not reached*/
  return FALSE;
}

bool exprNode_handleError( exprNode e)
{
   if (exprNode_isError (e) || exprNode_isUnhandled(e) )
    {
      static /*@only@*/ cstring error = cstring_undefined;

      if (!cstring_isDefined (error))
	{
	  error = cstring_makeLiteral ("<error>");
	}
      
      /*@-unqualifiedtrans*/ return TRUE; /*@=unqualifiedtrans*/
    }
   return FALSE;
}

bool /*@alt void@*/ exprNode_generateConstraints (/*@dependent@*/ exprNode e)
{
  if (exprNode_isError (e) )
    return FALSE;

  if (exprNode_isUnhandled (e) )
    {
      DPRINTF( (message("Warning ignoring %s", exprNode_unparse (e) ) ) );
        return FALSE;
    }

  DPRINTF((message ("exprNode_generateConstraints Analysising %s at %s", exprNode_unparse( e),
		    fileloc_unparse(exprNode_getfileloc(e) ) ) ) );

  if (exprNode_isMultiStatement ( e) )
    {
      exprNode_multiStatement(e);
    }
  else
    {
      fileloc loc;
      
      loc = exprNode_getNextSequencePoint(e); 
      exprNode_exprTraverse(e, FALSE, FALSE, loc);
      
      fileloc_free(loc);
      return FALSE;
    }
  
  {
    constraintList c;

    c = constraintList_makeFixedArrayConstraints (e->uses);
    e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, c);
    constraintList_free(c);
  }    

  DPRINTF ( (message ("e->requiresConstraints %s", constraintList_printDetailed (e->requiresConstraints) ) ) );
  return FALSE;
}


/* handles multiple statements */

bool exprNode_isMultiStatement(exprNode e)
{
if (exprNode_handleError (e) != NULL)
  return FALSE;
 
  switch (e->kind)
    {
    case XPR_FOR:
    case XPR_FORPRED:
    case XPR_IF:
    case XPR_IFELSE:
    case XPR_WHILE:
    case XPR_WHILEPRED:
    case XPR_DOWHILE:
    case XPR_BLOCK:
    case XPR_STMT:
    case XPR_STMTLIST:
    case XPR_SWITCH:
      return TRUE;
    default:
      return FALSE;
    }

}

static void exprNode_stmt ( /*@dependent@*/ /*@temp@*/ exprNode e)
{
  exprNode snode;
  fileloc loc;
  cstring s;
  
  if (exprNode_isError(e) )
    {
      return; 
    }

  /*e->requiresConstraints = constraintList_makeNew();
    e->ensuresConstraints  = constraintList_makeNew(); */
 
  DPRINTF(( "expNode_stmt: STMT:") );
  s =  exprNode_unparse(e);
  DPRINTF ( ( message("exprNode_stmt: STMT: %s ", s) ) );
  
  if (e->kind == XPR_INIT)
    {
      constraintList tempList;
      DPRINTF (("Init") );
      DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
      loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
      exprNode_exprTraverse (e, FALSE, FALSE, loc);
      fileloc_free(loc);

      tempList = e->requiresConstraints;
      e->requiresConstraints = exprNode_traversRequiresConstraints(e);
      constraintList_free(tempList);

      tempList = e->ensuresConstraints;
      e->ensuresConstraints  = exprNode_traversEnsuresConstraints(e);
      constraintList_free(tempList);
      return; 
    }
  
  if (e->kind != XPR_STMT)
    {
      
      DPRINTF (("Not Stmt") );
      DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );

      if (exprNode_isMultiStatement (e))
	{
	  exprNode_multiStatement (e); /* evans 2001-08-21: spurious return removed */
	}

      DPRINTF( (message ("Ignoring non-statement %s", exprNode_unparse(e) ) ) );
      return; 
    }
 
  DPRINTF (("Stmt") );
  DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
     
  snode = exprData_getUopNode (e->edata);
  
  /* could be stmt involving multiple statements:
     i.e. if, while for ect.
  */
  
  if (exprNode_isMultiStatement (snode))
    {
      exprNode_multiStatement (snode);
      (void) exprNode_copyConstraints (e, snode);
      return;
    }
  
  loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
  exprNode_exprTraverse (snode, FALSE, FALSE, loc);

  fileloc_free(loc);

  constraintList_free (e->requiresConstraints);
  e->requiresConstraints = exprNode_traversRequiresConstraints(snode);

  constraintList_free (e->ensuresConstraints);
  e->ensuresConstraints  = exprNode_traversEnsuresConstraints(snode);

  DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n",
		      constraintList_print(e->requiresConstraints),
		      constraintList_print(e->ensuresConstraints) ) ) );

  return; 
}

static void exprNode_stmtList  (/*@dependent@*/ exprNode e)
{
  exprNode stmt1, stmt2;
  if (exprNode_isError (e) )
    {
      return; 
    }

  /*
    Handle case of stmtList with only one statement:
    The parse tree stores this as stmt instead of stmtList
  */

  if (e->kind != XPR_STMTLIST)
    {
      exprNode_stmt(e);
      return;
    }
  llassert (e->kind == XPR_STMTLIST);
  DPRINTF(( "exprNode_stmtList STMTLIST:") );
  DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)) ) );
  stmt1 = exprData_getPairA (e->edata);
  stmt2 = exprData_getPairB (e->edata);


  DPRINTF(("exprNode_stmtlist       ") );
  DPRINTF ((message("XW%s    |        %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2) ) ) );
   
  exprNode_stmt (stmt1);
  DPRINTF(("\nstmt after stmtList call " ));

  exprNode_stmt (stmt2);
  exprNode_mergeResolve (e, stmt1, stmt2 );
  
  DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n",
		      constraintList_print(e->requiresConstraints),
		      constraintList_print(e->ensuresConstraints) ) ) );
  return;
}

static exprNode doIf (/*@returned@*/  exprNode e, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body)
{
  constraintList temp;

  DPRINTF ((message ("doIf: %s ", exprNode_unparse(e) ) ) );

  llassert(exprNode_isDefined(test) );
  llassert (exprNode_isDefined (e) );
  llassert (exprNode_isDefined (body) );

  
      DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) ));

      DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) ));
      
      DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->trueEnsuresConstraints) ) ));

      DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->falseEnsuresConstraints) ) ));



      DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->ensuresConstraints) ) ));

      DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->ensuresConstraints) ) ));
      
      DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->trueEnsuresConstraints) ) ));

      DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->falseEnsuresConstraints) ) ));



      temp = test->trueEnsuresConstraints;
      test->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(test);
      constraintList_free(temp);

  temp = test->ensuresConstraints;
  test->ensuresConstraints = exprNode_traversEnsuresConstraints (test);
  constraintList_free(temp);

  temp = test->requiresConstraints;
  test->requiresConstraints = exprNode_traversRequiresConstraints (test);
  constraintList_free(temp);


  test->trueEnsuresConstraints = constraintList_substituteFreeTarget(test->trueEnsuresConstraints, test->ensuresConstraints);
  
  DPRINTF ((message ("doIf: test ensures %s ", constraintList_print(test->ensuresConstraints) ) ) );
    
  DPRINTF ((message ("doIf: test true ensures %s ", constraintList_print(test->trueEnsuresConstraints) ) ) );
  
  constraintList_free(e->requiresConstraints);

  
  e->requiresConstraints = constraintList_reflectChanges(body->requiresConstraints, test->trueEnsuresConstraints);

  e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints,
					   test->ensuresConstraints);
  temp = e->requiresConstraints;
  e->requiresConstraints = constraintList_mergeRequires (e->requiresConstraints, test->requiresConstraints);
  constraintList_free(temp);


  /* drl possible problem : warning bad */
  constraintList_free(e->ensuresConstraints);
  e->ensuresConstraints = constraintList_copy (test->ensuresConstraints);
  
  if (exprNode_mayEscape (body) )
    {
      DPRINTF (( message("doIf: the if statement body %s returns or exits", exprNode_unparse(body) ) ));
      e->ensuresConstraints = constraintList_mergeEnsuresFreeFirst (e->ensuresConstraints,
							test->falseEnsuresConstraints);
    }
  
  DPRINTF ((message ("doIf: if requiers %s ", constraintList_print(e->requiresConstraints) ) ) );
  
  return e;
}

/*drl added 3/4/2001
  Also used for condition i.e. ?: operation

  Precondition
  This function assumes that p, trueBranch, falseBranch have have all been traversed
  for constraints i.e. we assume that exprNode_traversEnsuresConstraints,
  exprNode_traversRequiresConstraints,  exprNode_traversTrueEnsuresConstraints,
  exprNode_traversFalseEnsuresConstraints have all been run
*/


static exprNode doIfElse (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode p, /*@dependent@*/ exprNode trueBranch, /*@dependent@*/ exprNode falseBranch)
{
  constraintList c1, cons, t, t2, f, f2;
  
  DPRINTF ((message ("doIfElse: %s ", exprNode_unparse(e) ) ) );
  
  /* do requires clauses */
  c1 = constraintList_copy (p->ensuresConstraints);
  
  t = constraintList_reflectChanges(trueBranch->requiresConstraints, p->trueEnsuresConstraints);
  t = constraintList_reflectChangesFreePre (t, p->ensuresConstraints);
  
  cons = constraintList_reflectChanges(falseBranch->requiresConstraints, p->falseEnsuresConstraints);
  cons  = constraintList_reflectChangesFreePre (cons, c1);
  
  constraintList_free(e->requiresConstraints);
  e->requiresConstraints = constraintList_mergeRequiresFreeFirst (t, cons);
  e->requiresConstraints = constraintList_mergeRequiresFreeFirst (e->requiresConstraints, p->requiresConstraints);
  
  /* do ensures clauses
     find the  the ensures lists for each subbranch
  */

  t = constraintList_mergeEnsures (p->trueEnsuresConstraints, trueBranch->ensuresConstraints);
  t2 = t;
  t = constraintList_mergeEnsures (p->ensuresConstraints, t);
  constraintList_free(t2);
  
  f = constraintList_mergeEnsures (p->falseEnsuresConstraints, falseBranch->ensuresConstraints);
  f2 = f;
  f = constraintList_mergeEnsures (p->ensuresConstraints, f);
  constraintList_free(f2);
  
  /* find ensures for whole if/else statement */
  
  constraintList_free(e->ensuresConstraints);
  
  e->ensuresConstraints = constraintList_logicalOr (t, f);
  
  constraintList_free(t);
  constraintList_free(f);
  constraintList_free(cons);
  constraintList_free(c1);
  
  DPRINTF ((message ("doIfElse: if requires %q ", constraintList_print(e->requiresConstraints) ) ) );
  DPRINTF ((message ("doIfElse: if ensures %q ", constraintList_print(e->ensuresConstraints) ) ) );
  
  return e;
}

static exprNode doWhile (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body)
{
  DPRINTF ((message ("doWhile: %s ", exprNode_unparse(e) ) ) );
  return doIf (e, test, body);
}

/*@only@*/ constraintList constraintList_makeFixedArrayConstraints (/*@observer@*/ sRefSet s)
{
  constraintList ret;
  constraint con;
  ret = constraintList_makeNew();
 
  sRefSet_elements (s, el)
    {
      if (sRef_isFixedArray(el) )
	{
	  long int size;
	  DPRINTF( (message("%s is a fixed array",
			    sRef_unparse(el)) ) );
	  size = sRef_getArraySize(el);
	  DPRINTF( (message("%s is a fixed array with size %d",
			    sRef_unparse(el), (int)size) ) );
	  con = constraint_makeSRefSetBufferSize (el, (size - 1));
	  ret = constraintList_add(ret, con);
	}
      else
	{
	  DPRINTF( (message("%s is not a fixed array",
			    sRef_unparse(el)) ) );
	  
	  
	  if (sRef_isExternallyVisible (el) )
	    {
	      /*
		DPRINTF( (message("%s is externally visible",
		sRef_unparse(el) ) ));
		con = constraint_makeSRefWriteSafeInt(el, 0);
		ret = constraintList_add(ret, con);
		
		con = constraint_makeSRefReadSafeInt(el, 0);
		
		ret = constraintList_add(ret, con);
	      */
	    }
	}
    }
  end_sRefSet_elements ;
  
  DPRINTF(( message("constraintList_makeFixedArrayConstraints returning %s",
		    constraintList_print(ret) ) ));
  return ret;
}

# if 0
exprNode makeDataTypeConstraints (/*@returned@*/ exprNode e)
{
  constraintList c;
  DPRINTF(("makeDataTypeConstraints"));

  c = constraintList_makeFixedArrayConstraints (e->uses);
  
  e->ensuresConstraints = constraintList_addListFree (e->ensuresConstraints, c);
 
 return e;
}
# endif

static void doFor (/*@dependent@*/ exprNode e, /*@dependent@*/ exprNode forPred, /*@dependent@*/ exprNode forBody)
{
  exprNode init, test, inc;
  /* merge the constraints: modle as if statement */

      /* init
	if (test)
	   for body
	   inc        */
  init  =  exprData_getTripleInit (forPred->edata);
  test =   exprData_getTripleTest (forPred->edata);
  inc  =   exprData_getTripleInc (forPred->edata);
  
  if ( ( (exprNode_isError (test) /*|| (exprNode_isError(init) )*/ ) || (exprNode_isError (inc) ) ) )
    {
      DPRINTF ((message ("strange for statement:%s, ignoring it", exprNode_unparse(e) ) ) );
      return;
    }
  
  exprNode_forLoopHeuristics(e, forPred, forBody);
  
  constraintList_free(e->requiresConstraints);
  e->requiresConstraints = constraintList_reflectChanges(forBody->requiresConstraints, test->ensuresConstraints);
  e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, test->trueEnsuresConstraints);
  e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, forPred->ensuresConstraints);
  
  if (!forBody->canBreak)
    {
      e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints, constraintList_copy(forPred->ensuresConstraints) );
      e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints,constraintList_copy( test->falseEnsuresConstraints));
    }
  else
    {
      DPRINTF(("Can break") );
    }
}

static /*@dependent@*/ exprNode exprNode_makeDependent(/*@returned@*/  exprNode e)
{
  /*@-temptrans@*/
  return e;
  /*@=temptrans@*/  
}

static void exprNode_doGenerateConstraintSwitch (/*@dependent@*/ exprNode switchExpr,
						  /*@dependent@*/ exprNode body, /*@special@*/ constraintList * currentRequires, /*@special@*/  constraintList *
						  currentEnsures,  /*@special@*/  constraintList * savedRequires, /*@special@*/ constraintList *
						  savedEnsures)
     /*@post:only *currentRequires,  *currentEnsures,  *savedRequires, *savedEnsures @*/ /*@defines *currentRequires,  *currentEnsures,  *savedRequires, *savedEnsures @*/
{
  exprNode stmt, stmtList;

  DPRINTF(( message("exprNode_doGenerateConstraintSwitch: (switch %s) %s",
		    exprNode_unparse(switchExpr), exprNode_unparse(body)
		    ) ));

  if (exprNode_isError(body) )
    {
      *currentRequires = constraintList_makeNew();
      *currentEnsures = constraintList_makeNew();

      *savedRequires = constraintList_makeNew();
      *savedEnsures = constraintList_makeNew();
      /*@-onlytrans@*/
      return;
      /*@=onlytrans@*/      
    }

  if (body->kind != XPR_STMTLIST )
    {
      DPRINTF((message("exprNode_doGenerateConstraintSwitch: non stmtlist: %s",
		       exprNode_unparse(body) )));
      stmt = body;
      stmtList = exprNode_undefined;
      stmt = exprNode_makeDependent(stmt);
      stmtList = exprNode_makeDependent(stmtList);
    }
  else
    {
      stmt     = exprData_getPairB(body->edata);
      stmtList = exprData_getPairA(body->edata);
      stmt = exprNode_makeDependent(stmt);
      stmtList = exprNode_makeDependent(stmtList);
    }

  DPRINTF((message("exprNode_doGenerateConstraintSwitch: stmtlist: %s stmt: %s",
		   exprNode_unparse(stmtList), exprNode_unparse(stmt) )
	   ));


  exprNode_doGenerateConstraintSwitch (switchExpr, stmtList, currentRequires, currentEnsures,
				       savedRequires, savedEnsures );

  if (exprNode_isError(stmt) )
    /*@-onlytrans@*/
    return;
    /*@=onlytrans@*/

  exprNode_stmt(stmt);

  switchExpr = exprNode_makeDependent (switchExpr);
    
  if (! exprNode_isCaseMarker(stmt) )
    {

      constraintList temp;

      DPRINTF (( message("Got normal statement %s (requires %s ensures %s)", exprNode_unparse(stmt),
			 constraintList_unparse(stmt->requiresConstraints), constraintList_unparse(stmt->ensuresConstraints) ) ));

      temp = constraintList_reflectChanges (stmt->requiresConstraints,
					    *currentEnsures);

            *currentRequires = constraintList_mergeRequiresFreeFirst(
								     *currentRequires,
								     temp);

	    constraintList_free(temp);

	          *currentEnsures = constraintList_mergeEnsuresFreeFirst
		    (*currentEnsures,
		     stmt->ensuresConstraints);
		  DPRINTF(( message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
				    "%s currentEnsures:%s",
				    exprNode_unparse(switchExpr), exprNode_unparse(body),
				    constraintList_print(*currentRequires), constraintList_print(*currentEnsures)
				    ) ));
		  /*@-onlytrans@*/
		  return;
		  /*@=onlytrans@*/

    }

  if (exprNode_isCaseMarker(stmt) && exprNode_mustEscape(stmtList) )
    {
      /*
      ** merge current and saved constraint with Logical Or...
      ** make a constraint for ensures
      */

      constraintList temp;
      constraint con;

      DPRINTF (( message("Got case marker") ));

      if (constraintList_isUndefined(*savedEnsures) &&
	  constraintList_isUndefined(*savedRequires) )
	{
	  llassert(constraintList_isUndefined(*savedEnsures) );
	  llassert(constraintList_isUndefined(*savedRequires) );
	  *savedEnsures  = constraintList_copy(*currentEnsures);
	  *savedRequires = constraintList_copy(*currentRequires);
	}
      else
	{
	  DPRINTF (( message("Doing logical or") ));
	  temp = constraintList_logicalOr (*savedEnsures, *currentEnsures);
	  constraintList_free (*savedEnsures);
	  *savedEnsures = temp;
	  
	  *savedRequires = constraintList_mergeRequiresFreeFirst (*savedRequires, *currentRequires);
	}
      
      con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle
					(stmt->edata), exprNode_getfileloc(stmt) );


      constraintList_free(*currentEnsures);
      *currentEnsures = constraintList_makeNew();
      *currentEnsures = constraintList_add(*currentEnsures, con);

      constraintList_free(*currentRequires);
      *currentRequires = constraintList_makeNew();
      DPRINTF(( message("exprNode_doGenerateConstraintSwitch: (switch %s) %s savedRequires:"
			"%s savedEnsures:%s",
			exprNode_unparse(switchExpr), exprNode_unparse(body),
			constraintList_print(*savedRequires), constraintList_print(*savedEnsures)
			) ));

    }

  else if (exprNode_isCaseMarker(stmt) )
    /* prior case has no break. */
    {
      /* 
	 We don't do anything to the sved constraints because the case hasn't ended
	 The new ensures constraints for the case will be:
	 the constraint for the case statement (CASE_LABEL == SWITCH_EXPR) logicalOr currentEnsures
      */
      
      constraintList temp;
      constraint con;

      constraintList ensuresTemp;

      DPRINTF (( message("Got case marker with no prior break") ));

      con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle
					(stmt->edata), exprNode_getfileloc(stmt) );

      ensuresTemp = constraintList_makeNew();

      ensuresTemp = constraintList_add (ensuresTemp, con);

      if (exprNode_isError(stmtList) )
	{
	  constraintList_free(*currentEnsures);

	  *currentEnsures = constraintList_copy(ensuresTemp);
	  constraintList_free(ensuresTemp);

	}
      else
	{
	  
	  temp = constraintList_logicalOr (*currentEnsures, ensuresTemp);
	  
	  constraintList_free(*currentEnsures);
	  constraintList_free(ensuresTemp);

	  *currentEnsures = temp;
	}
      constraintList_free(*currentRequires);
      
      *currentRequires = constraintList_makeNew();
    }
  else
    {
      /*
	we handle the case of ! exprNode_isCaseMarker above
	the else if clause should always be true.
      */
      BADEXIT;
    }

  DPRINTF(( message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
		    "%s currentEnsures:%s",
		    exprNode_unparse(switchExpr), exprNode_unparse(body),
		    constraintList_print(*currentRequires), constraintList_print(*currentEnsures)
		    ) ));
  /*@-onlytrans@*/ 
  return;
  /*@=onlytrans@*/ 

}


static void exprNode_generateConstraintSwitch ( exprNode switchStmt)
{
  constraintList constraintsRequires;
  constraintList constraintsEnsures;
  constraintList lastRequires;
  constraintList lastEnsures;

  exprNode body;
  exprNode switchExpr;

  switchExpr = exprData_getPairA(switchStmt->edata);
  body = exprData_getPairB(switchStmt->edata);

  /*@i22*/
  DPRINTF((message("") ));
  
  if ( body->kind == XPR_BLOCK)
    body = exprData_getSingle(body->edata);

  /*
  constraintsRequires = constraintList_undefined;
  constraintsEnsures = constraintList_undefined;

  lastRequires = constraintList_makeNew();
  lastEnsures = constraintList_makeNew();
  */

  exprNode_doGenerateConstraintSwitch (switchExpr, body, &lastRequires, &lastEnsures, &constraintsRequires, &constraintsEnsures);

  /*
    merge current and saved constraint with Logical Or...
    make a constraint for ensures
  */

  constraintList_free(switchStmt->requiresConstraints);
  constraintList_free(switchStmt->ensuresConstraints);

  if (constraintList_isDefined(constraintsEnsures) && constraintList_isDefined(constraintsRequires) )
    {
      switchStmt->ensuresConstraints = constraintList_logicalOr(constraintsEnsures, lastEnsures);
      switchStmt->requiresConstraints =   constraintList_mergeRequires(constraintsRequires, lastRequires);
      constraintList_free (constraintsRequires);
      constraintList_free (constraintsEnsures);
    }
  else
    {
      switchStmt->ensuresConstraints =    constraintList_copy(lastEnsures);
      switchStmt->requiresConstraints =   constraintList_copy(lastRequires);
    }

  constraintList_free (lastRequires);
  constraintList_free (lastEnsures);

  DPRINTF(( (message(" exprNode_generateConstraintSwitch returning requires: %s and ensures %s",
		     constraintList_print( switchStmt->requiresConstraints),
		     constraintList_print( switchStmt->ensuresConstraints)
		     )
	     ) ));
}

static exprNode doSwitch (/*@returned@*/ exprNode e)
{
  exprNode body;
  exprData data;

  data = e->edata;
  DPRINTF (( message ("doSwitch for: switch (%s) %s",
		      exprNode_unparse (exprData_getPairA (data)),
		      exprNode_unparse (exprData_getPairB (data))) ));

  body = exprData_getPairB (data);
  exprNode_generateConstraintSwitch (e);
  return e;
}

void exprNode_multiStatement (/*@dependent@*/ exprNode e)
{
  
  bool ret;
  exprData data;
  exprNode e1, e2;
  exprNode p, trueBranch, falseBranch;
  exprNode forPred, forBody;
  exprNode test;

  constraintList temp;

  DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse( e),
		    fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
  
  if (exprNode_handleError (e))
    {
      return; 
    }

  data = e->edata;

  ret = TRUE;

  switch (e->kind)
    {
      
    case XPR_FOR:
      forPred = exprData_getPairA (data);
      forBody = exprData_getPairB (data);
      
      /* First generate the constraints */
      exprNode_generateConstraints (forPred);
      exprNode_generateConstraints (forBody);


      doFor (e, forPred, forBody);
     
      break;

    case XPR_FORPRED:
      exprNode_generateConstraints (exprData_getTripleInit (data) );
      test = exprData_getTripleTest (data);
      exprNode_exprTraverse (test,FALSE, FALSE, exprNode_loc(e));
      exprNode_generateConstraints (exprData_getTripleInc (data) );
    
      if (!exprNode_isError(test) )
	{
	  constraintList temp2;
	  temp2 = test->trueEnsuresConstraints;
	  test->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(test);
	  constraintList_free(temp2);
	}
      
      exprNode_generateConstraints (exprData_getTripleInc (data));
      break;

    case XPR_WHILE:
      e1 = exprData_getPairA (data);
      e2 = exprData_getPairB (data);
      
       exprNode_exprTraverse (e1,
			      FALSE, FALSE, exprNode_loc(e1));
       
       exprNode_generateConstraints (e2);

       e = doWhile (e, e1, e2);
      
      break; 

    case XPR_IF:
      DPRINTF(( "IF:") );
      DPRINTF ((exprNode_unparse(e) ) );
      e1 = exprData_getPairA (data);
      e2 = exprData_getPairB (data);

      exprNode_exprTraverse (e1, FALSE, FALSE, exprNode_loc(e1));

      exprNode_generateConstraints (e2);
      e = doIf (e, e1, e2);
      break;
     
    case XPR_IFELSE:
      DPRINTF(("Starting IFELSE"));
      p = exprData_getTriplePred (data);
      trueBranch = exprData_getTripleTrue (data);
      falseBranch = exprData_getTripleFalse (data);
      
      exprNode_exprTraverse (p,
			     FALSE, FALSE, exprNode_loc(p));
      exprNode_generateConstraints (trueBranch);
      exprNode_generateConstraints (falseBranch);

      temp = p->ensuresConstraints;
      p->ensuresConstraints = exprNode_traversEnsuresConstraints (p);
      constraintList_free(temp);

      temp = p->requiresConstraints;
      p->requiresConstraints = exprNode_traversRequiresConstraints (p);
      constraintList_free(temp);

      temp = p->trueEnsuresConstraints;
      p->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(p);
      constraintList_free(temp);

      temp = p->falseEnsuresConstraints;
      p->falseEnsuresConstraints =  exprNode_traversFalseEnsuresConstraints(p);
      constraintList_free(temp);

          e = doIfElse (e, p, trueBranch, falseBranch);
      DPRINTF( ("Done IFELSE") );
      break;
 
    case XPR_DOWHILE:

      e2 = (exprData_getPairB (data));
      e1 = (exprData_getPairA (data));

      DPRINTF((message ("do { %s } while (%s)", exprNode_unparse(e2), exprNode_unparse(e1) ) ));
      exprNode_generateConstraints (e2);
      exprNode_generateConstraints (e1);
      e = exprNode_copyConstraints (e, e2);
      DPRINTF ((message ("e = %s  ", constraintList_print(e->requiresConstraints) ) ));
      
      break;
      
    case XPR_BLOCK:
      exprNode_generateConstraints (exprData_getSingle (data));
      
      constraintList_free(e->requiresConstraints);
      e->requiresConstraints = constraintList_copy ( (exprData_getSingle (data))->requiresConstraints );
      
      constraintList_free(e->ensuresConstraints);
      e->ensuresConstraints = constraintList_copy ( (exprData_getSingle (data))->ensuresConstraints );
      break;

    case XPR_SWITCH:
      e = doSwitch (e);
      break;
    case XPR_STMT:
    case XPR_STMTLIST:
      exprNode_stmtList (e);
      return ;
      /*@notreached@*/
      break;
    default:
      ret=FALSE;
    }
  return; 
}

static bool lltok_isBoolean_Op (lltok tok)
{
  /*this should really be a switch statement but
    I don't want to violate the abstraction
    maybe this should go in lltok.c */
  
  if (lltok_isEq_Op (tok) )
	{
	  return TRUE;
	}
      if (lltok_isAnd_Op (tok) )

	{

	  return TRUE;	  	  
	}
   if (lltok_isOr_Op (tok) )
	{
	  return TRUE;	  	
	}

   if (lltok_isGt_Op (tok) )
     {
       return TRUE;
     }
   if (lltok_isLt_Op (tok) )
     {
       return TRUE;
     }

   if (lltok_isLe_Op (tok) )
     {
       return TRUE;
     }
   
   if (lltok_isGe_Op (tok) )
     {
       return TRUE;
     }
   
   return FALSE;

}


static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ bool definatelv, /*@unused@*/ bool definaterv,  fileloc sequencePoint)
{
  constraint cons;
  exprNode t1, t2;
  exprData data;
  lltok tok;
  constraintList tempList, temp;
  data = e->edata;
  
  tok = exprData_getOpTok (data);
  t1 = exprData_getOpA (data);
  t2 = exprData_getOpB (data);
  
  tempList = constraintList_undefined;
  
  /* arithmetic tests */
  
  if (lltok_isEq_Op (tok) )
    {
      cons =  constraint_makeEnsureEqual (t1, t2, sequencePoint);
      e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
    }
  
  
  if (lltok_isLt_Op (tok) )
    {
      cons =  constraint_makeEnsureLessThan (t1, t2, sequencePoint);
      e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
      cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
      e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
    }
   
  if (lltok_isGe_Op (tok) )
    {
      cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
      e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
      
      cons =  constraint_makeEnsureLessThan (t1, t2, sequencePoint);
      e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
    }
  
  if (lltok_isGt_Op (tok) )
    {
      cons =  constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
      e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
      cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
      e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
    }
  
  if (lltok_isLe_Op (tok) )
    {
      cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
      e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
      
      cons =  constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
      e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
    }
  
  /* Logical operations */
  
  if (lltok_isAnd_Op (tok) )
    {
      /* true ensures  */
      tempList = constraintList_copy (t1->trueEnsuresConstraints);
      tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
      e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList);
      
      /* false ensures: fens t1 or tens t1 and fens t2 */
      tempList = constraintList_copy (t1->trueEnsuresConstraints);
      tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
      temp = tempList;
      tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints);
      constraintList_free (temp);
      
      /* evans - was constraintList_addList - memory leak detected by lclint */
      e->falseEnsuresConstraints = constraintList_addListFree (e->falseEnsuresConstraints, tempList);
    }
  else if (lltok_isOr_Op (tok) )
    {
      /* false ensures */
      tempList = constraintList_copy (t1->falseEnsuresConstraints);
      tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
      e->falseEnsuresConstraints = constraintList_addListFree(e->falseEnsuresConstraints, tempList);
      
      /* true ensures: tens t1 or fens t1 and tens t2 */
      tempList = constraintList_copy (t1->falseEnsuresConstraints);
      tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
      
      temp = tempList;
      tempList = constraintList_logicalOr (tempList, t1->trueEnsuresConstraints);
      constraintList_free(temp);

      e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList);
      tempList = constraintList_undefined;
    }
  else
    {
      DPRINTF((message("%s is not a boolean operation", lltok_unparse(tok) ) ));
    } 
}

void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv,  /*@observer@*/ /*@temp@*/ fileloc sequencePoint)
{
  exprNode t1, t2, fcn;
  lltok tok;
  bool handledExprNode;
  exprData data;
  constraint cons;

  constraintList temp;

  if (exprNode_isError(e) )
    {
      return; 
    }
  
  DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e),
		    fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
  
  /*e->requiresConstraints = constraintList_makeNew();
  e->ensuresConstraints = constraintList_makeNew();
  e->trueEnsuresConstraints = constraintList_makeNew();;
  e->falseEnsuresConstraints = constraintList_makeNew();;
  */

  if (exprNode_isUnhandled (e) )
     {
       return;
     }
  
  handledExprNode = TRUE;
  
  data = e->edata;
  
  switch (e->kind)
    {
    case XPR_WHILEPRED:
      t1 = exprData_getSingle (data);
      exprNode_exprTraverse (t1,  definatelv, definaterv, sequencePoint);
      e = exprNode_copyConstraints (e, t1);
      break;

    case XPR_FETCH:

      if (definatelv )
	{
	  t1 =  (exprData_getPairA (data) );
	  t2 =  (exprData_getPairB (data) );
	  cons =  constraint_makeWriteSafeExprNode (t1, t2);
	}
      else 
	{
	  t1 =  (exprData_getPairA (data) );
	  t2 =  (exprData_getPairB (data) );
	  cons = constraint_makeReadSafeExprNode (t1, t2 );
	}
      
      e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
      cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint);
      e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);

      cons = constraint_makeEnsureLteMaxRead (t2, t1);
      e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
	
      exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
      exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
      
      /*@i325 Should check which is array/index. */
      break;
      
    case XPR_PARENS: 
      exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint);
      break;
    case XPR_INIT:
      {
	/*	
      	idDecl t;
	
	uentry ue;
	exprNode lhs;

	t = exprData_getInitId (data); 
	ue = usymtab_lookup (idDecl_observeId (t));
	lhs = exprNode_createId (ue);
	*/
	t2 = exprData_getInitNode (data);

	/*	DPRINTF(( (message("initialization: %s = %s",
			   exprNode_unparse(lhs),
			   exprNode_unparse(t2)
			   )
		   ) )); 	*/
	
	exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
	
	/* this test is nessecary because some expressions generate a null expression node.  function pointer do that -- drl */
        if ( (!exprNode_isError (e))  &&  (!exprNode_isError(t2)) )
	  {
	    cons =  constraint_makeEnsureEqual (e, t2, sequencePoint);
	    e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
	  }
      }
      
      break;
    case XPR_ASSIGN:
      t1 = exprData_getOpA (data);
      t2 = exprData_getOpB (data);
      exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint ); 
      exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );

      /* this test is nessecary because some expressions generate a null expression node.  function pointer do that -- drl */
      if ( (!exprNode_isError (t1))  &&  (!exprNode_isError(t2)) )
	{
	  cons =  constraint_makeEnsureEqual (t1, t2, sequencePoint);
	  e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
	}
      break;
    case XPR_OP:
      t1 = exprData_getOpA (data);
      t2 = exprData_getOpB (data);
      tok = exprData_getOpTok (data);
      

      if (tok.tok == ADD_ASSIGN)
	{
	  exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
	  exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );

	  cons = constraint_makeAddAssign (t1, t2,  sequencePoint );
	  e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
	}
      else if (tok.tok == SUB_ASSIGN)
	{
	  exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
	  exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );

	  cons = constraint_makeSubtractAssign (t1, t2,  sequencePoint );
	  e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
	}
      else
	{
	  exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
	  exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
	}
      
      if (lltok_isBoolean_Op (tok) )
	exprNode_booleanTraverse (e, definatelv, definaterv, sequencePoint);

      break;
    case XPR_SIZEOFT:
      /*@i43 drl possible problem : warning make sure the case can be ignored.. */
      
      break;
      
    case XPR_SIZEOF:
      /* drl  7-16-01
	 C standard says operand to sizeof isn't evaluated unless
	 its a variable length array.  So we don't generate constraints.
      */
	 
      break;
      
    case XPR_CALL:
      fcn = exprData_getFcn(data);
      
      exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint );
      DPRINTF ( (message ("Got call that %s ( %s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (exprData_getArgs (data) ) ) ) );

      fcn->requiresConstraints = constraintList_addListFree (fcn->requiresConstraints,
						 checkCall (fcn, exprData_getArgs (data)  ) );      

      fcn->ensuresConstraints = constraintList_addListFree (fcn->ensuresConstraints,
						 exprNode_getPostConditions(fcn, exprData_getArgs (data),e  ) );

      t1 = exprNode_createNew (exprNode_getType (e) );
      checkArgumentList (t1, exprData_getArgs(data), sequencePoint);
      exprNode_mergeResolve (e, t1, fcn);
      exprNode_free(t1);
      break;
      
    case XPR_RETURN:
      exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
      break;
  
    case XPR_NULLRETURN:
      
      break;
      
      
    case XPR_FACCESS:
      exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
      break;
   
    case XPR_ARROW:
      exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
      break;
   
    case XPR_STRINGLITERAL:

      break;
      
    case XPR_NUMLIT:

      break;
      
    case XPR_PREOP: 
      t1 = exprData_getUopNode(data);
      tok = (exprData_getUopTok (data));
      exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
      /*handle * pointer access */
      if (lltok_isInc_Op (tok) )
	{
	  DPRINTF(("doing ++(var)"));
	  t1 = exprData_getUopNode (data);
	  cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
	  e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
	}
      else if (lltok_isDec_Op (tok) )
	{
	  DPRINTF(("doing --(var)"));
	  t1 = exprData_getUopNode (data);
	  cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint );
	  e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
	}
      else if (lltok_isMult( tok  ) )
	{
	  if (definatelv)
	    {
	      cons = constraint_makeWriteSafeInt (t1, 0);
	    }
	  else
	    {
	      cons = constraint_makeReadSafeInt (t1, 0);
	    }
  	      e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
	}
      else if (lltok_isNot_Op (tok) )
	/* ! expr */
	{
	  constraintList_free(e->trueEnsuresConstraints);

	  e->trueEnsuresConstraints  = constraintList_copy (t1->falseEnsuresConstraints);
	  constraintList_free(e->falseEnsuresConstraints);
	  e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints);
	}
      
      else if (lltok_isAmpersand_Op (tok) )
	{
	  break;
	}
      else if (lltok_isMinus_Op (tok) )
	{
	  break;
	}
      else if ( lltok_isExcl_Op (tok) )
	{
	  break;
	}
      else if (lltok_isTilde_Op (tok) )
	{
	  break;
	}
      else
	{
	  llcontbug((message("Unsupported preop in %s", exprNode_unparse(e) ) ));
	  BADEXIT;
	}
      break;
      
    case XPR_POSTOP:
      
      exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint );
      
      if (lltok_isInc_Op (exprData_getUopTok (data) ) )
	{
	  DPRINTF(("doing ++"));
	  t1 = exprData_getUopNode (data);
	  cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
	  e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
	}
       if (lltok_isDec_Op (exprData_getUopTok (data) ) )
	{
	  DPRINTF(("doing --"));
	  t1 = exprData_getUopNode (data);
	  cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint );
	  e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
	}
      break;
    case XPR_CAST:
      {
	t2 =  exprData_getCastNode (data);
	DPRINTF (( message ("Examining cast (%q)%s", 
			    qtype_unparse (exprData_getCastType (data)),
			    exprNode_unparse (t2) )
		   ));
	exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
      }
      break;
      
    case XPR_COND:
      {
	exprNode pred, trueBranch, falseBranch;
	   llassert(FALSE);
      pred = exprData_getTriplePred (data);
      trueBranch = exprData_getTripleTrue (data);
      falseBranch = exprData_getTripleFalse (data);

      exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint );
      
      temp =       pred->ensuresConstraints;
      pred->ensuresConstraints = exprNode_traversEnsuresConstraints(pred);
      constraintList_free(temp);

      temp =       pred->requiresConstraints;
      pred->requiresConstraints = exprNode_traversRequiresConstraints(pred);
      constraintList_free(temp);
      
      temp =       pred->trueEnsuresConstraints;
      pred->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(pred);
      constraintList_free(temp);

      temp =       pred->falseEnsuresConstraints;
      pred->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(pred);
      constraintList_free(temp);

            
      exprNode_exprTraverse (trueBranch, FALSE, TRUE, sequencePoint );
      
      temp =       trueBranch->ensuresConstraints;
      trueBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(trueBranch);
      constraintList_free(temp);


      temp =       trueBranch->requiresConstraints;
      trueBranch->requiresConstraints = exprNode_traversRequiresConstraints(trueBranch);
      constraintList_free(temp);

      
      temp =       trueBranch->trueEnsuresConstraints;
      trueBranch->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(trueBranch);
      constraintList_free(temp);

      temp =       trueBranch->falseEnsuresConstraints;
      trueBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(trueBranch);
      constraintList_free(temp);

      exprNode_exprTraverse (falseBranch, FALSE, TRUE, sequencePoint );
      
      temp =       falseBranch->ensuresConstraints;
      falseBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(falseBranch);
      constraintList_free(temp);


      temp =       falseBranch->requiresConstraints;
      falseBranch->requiresConstraints = exprNode_traversRequiresConstraints(falseBranch);
      constraintList_free(temp);

      
      temp =       falseBranch->trueEnsuresConstraints;
      falseBranch->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(falseBranch);
      constraintList_free(temp);

      temp =       falseBranch->falseEnsuresConstraints;
      falseBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(falseBranch);
      constraintList_free(temp);

      /* if pred is true e equals true otherwise pred equals false */
      
      cons =  constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
      trueBranch->ensuresConstraints = constraintList_add(trueBranch->ensuresConstraints, cons);

      cons =  constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
      falseBranch->ensuresConstraints = constraintList_add(falseBranch->ensuresConstraints, cons);

      e = doIfElse (e, pred, trueBranch, falseBranch);
      
      }
      break;
    case XPR_COMMA:
      llassert(FALSE);
      t1 = exprData_getPairA (data);
      t2 = exprData_getPairB (data);
    /* we essiantially treat this like expr1; expr2
     of course sequencePoint isn't adjusted so this isn't completely accurate
    problems../  */
      exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint );
      exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
      exprNode_mergeResolve (e, t1, t2);
      break;

    default:
      handledExprNode = FALSE;
    }

  e->requiresConstraints =  constraintList_preserveOrig ( e->requiresConstraints);
  e->ensuresConstraints  =  constraintList_preserveOrig ( e->ensuresConstraints);
  e->requiresConstraints = constraintList_addGeneratingExpr ( e->requiresConstraints, e);

  e->ensuresConstraints  = constraintList_addGeneratingExpr ( e->ensuresConstraints, e);


  e->requiresConstraints = constraintList_removeSurpressed( e->requiresConstraints);
  
  DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) ));

  DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) ));
  
  DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->trueEnsuresConstraints) ) ));

  DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->falseEnsuresConstraints) ) ));

  return;
}


constraintList exprNode_traversTrueEnsuresConstraints (exprNode e)
{
  exprNode t1;

  bool handledExprNode;
  exprData data;
  constraintList ret;

  if (exprNode_handleError (e))
    {
      ret = constraintList_makeNew();
      return ret;
    }
  ret = constraintList_copy (e->trueEnsuresConstraints );
   
  handledExprNode = TRUE;
   
  data = e->edata;
  
  switch (e->kind)
    {
    case XPR_WHILEPRED:
      t1 = exprData_getSingle (data);
      ret = constraintList_addListFree ( ret, exprNode_traversTrueEnsuresConstraints (t1) );
      break;
      
    case XPR_FETCH:
      
      ret = constraintList_addListFree (ret,
				    exprNode_traversTrueEnsuresConstraints
				    (exprData_getPairA (data) ) );
        
      ret = constraintList_addListFree (ret,
				    exprNode_traversTrueEnsuresConstraints
				    (exprData_getPairB (data) ) );
      break;
    case XPR_PREOP:
          
      ret = constraintList_addListFree (ret,
				    exprNode_traversTrueEnsuresConstraints
				    (exprData_getUopNode (data) ) );
      break;
      
    case XPR_PARENS: 
      ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints
				    (exprData_getUopNode (data) ) );
      break;

    case XPR_INIT:
      ret = constraintList_addListFree (ret,
					exprNode_traversTrueEnsuresConstraints
					(exprData_getInitNode (data) ) );
	break;


    case XPR_ASSIGN:
        ret = constraintList_addListFree (ret,
				    exprNode_traversTrueEnsuresConstraints
				    (exprData_getOpA (data) ) );
        
       ret = constraintList_addListFree (ret,
				    exprNode_traversTrueEnsuresConstraints
				    (exprData_getOpB (data) ) );
       break;
    case XPR_OP:
       ret = constraintList_addListFree (ret,
				    exprNode_traversTrueEnsuresConstraints
				    (exprData_getOpA (data) ) );
        
       ret = constraintList_addListFree (ret,
				    exprNode_traversTrueEnsuresConstraints
				    (exprData_getOpB (data) ) );
       break;
    case XPR_SIZEOFT:
      break;
      
    case XPR_SIZEOF:
          
       ret = constraintList_addListFree (ret,
					 exprNode_traversTrueEnsuresConstraints
					 (exprData_getSingle (data) ) );
       break;
      
    case XPR_CALL:
      ret = constraintList_addListFree (ret,
				     exprNode_traversTrueEnsuresConstraints
				    (exprData_getFcn (data) ) );
      /*@i11*/  /* exprNodeList_unparse (exprData_getArgs (data) ); */
      break;
      
    case XPR_RETURN:
      ret = constraintList_addListFree (ret,
				    exprNode_traversTrueEnsuresConstraints
				    (exprData_getSingle (data) ) );
      break;
  
    case XPR_NULLRETURN:
      break;
            
    case XPR_FACCESS:
      ret = constraintList_addListFree (ret,
					exprNode_traversTrueEnsuresConstraints
					(exprData_getFieldNode (data) ) );
      break;
   
    case XPR_ARROW:
      ret = constraintList_addListFree (ret,
					exprNode_traversTrueEnsuresConstraints
					(exprData_getFieldNode (data) ) );
      break;
   
    case XPR_STRINGLITERAL:
      break;
      
    case XPR_NUMLIT:
      break;
    case XPR_POSTOP:

           ret = constraintList_addListFree (ret,
				    exprNode_traversTrueEnsuresConstraints
				    (exprData_getUopNode (data) ) );
	   break;

    case XPR_CAST:

      ret = constraintList_addListFree (ret,
				    exprNode_traversTrueEnsuresConstraints
				    (exprData_getCastNode (data) ) );
      break;

    default:
      break;
    }

  return ret;
}

constraintList exprNode_traversFalseEnsuresConstraints (exprNode e)
{
  exprNode t1;
  bool handledExprNode;
  exprData data;
  constraintList ret;

   if (exprNode_handleError (e))
     {
       ret = constraintList_makeNew();
       return ret;
     }

  ret = constraintList_copy (e->falseEnsuresConstraints );
   
   handledExprNode = TRUE;
   
  data = e->edata;
  
  switch (e->kind)
    {
   case XPR_WHILEPRED:
      t1 = exprData_getSingle (data);
      ret = constraintList_addListFree ( ret,exprNode_traversFalseEnsuresConstraints (t1) );
      break;
      
    case XPR_FETCH:
      
      ret = constraintList_addListFree (ret,
				    exprNode_traversFalseEnsuresConstraints
				    (exprData_getPairA (data) ) );
        
      ret = constraintList_addListFree (ret,
				    exprNode_traversFalseEnsuresConstraints
				    (exprData_getPairB (data) ) );
      break;
    case XPR_PREOP:
          
      ret = constraintList_addListFree (ret,
				    exprNode_traversFalseEnsuresConstraints
				    (exprData_getUopNode (data) ) );
      break;
      
    case XPR_PARENS: 
      ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints
				    (exprData_getUopNode (data) ) );
      break;
    case XPR_INIT:
        ret = constraintList_addListFree (ret,
				    exprNode_traversFalseEnsuresConstraints
				    (	exprData_getInitNode (data) ) );
	break;

    case XPR_ASSIGN:
        ret = constraintList_addListFree (ret,
				    exprNode_traversFalseEnsuresConstraints
				    (exprData_getOpA (data) ) );
        
       ret = constraintList_addListFree (ret,
				    exprNode_traversFalseEnsuresConstraints
				    (exprData_getOpB (data) ) );
       break;
    case XPR_OP:
       ret = constraintList_addListFree (ret,
				    exprNode_traversFalseEnsuresConstraints
				    (exprData_getOpA (data) ) );
        
       ret = constraintList_addListFree (ret,
				    exprNode_traversFalseEnsuresConstraints
				    (exprData_getOpB (data) ) );
       break;
    case XPR_SIZEOFT:
      break;
      
    case XPR_SIZEOF:
          
       ret = constraintList_addListFree (ret,
				    exprNode_traversFalseEnsuresConstraints
				     (exprData_getSingle (data) ) );
       break;
      
    case XPR_CALL:
      ret = constraintList_addListFree (ret,
				     exprNode_traversFalseEnsuresConstraints
				    (exprData_getFcn (data) ) );
      /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data) ); */
      break;
      
    case XPR_RETURN:
      ret = constraintList_addListFree (ret,
				    exprNode_traversFalseEnsuresConstraints
				    (exprData_getSingle (data) ) );
      break;
  
    case XPR_NULLRETURN:
      break;
            
    case XPR_FACCESS:
      ret = constraintList_addListFree (ret,
					exprNode_traversFalseEnsuresConstraints
					(exprData_getFieldNode (data) ) );
      break;
      
    case XPR_ARROW:
      ret = constraintList_addListFree (ret,
					exprNode_traversFalseEnsuresConstraints
					(exprData_getFieldNode (data) ) );
      break;
   
    case XPR_STRINGLITERAL:
      break;
      
    case XPR_NUMLIT:
      break;
    case XPR_POSTOP:

           ret = constraintList_addListFree (ret,
				    exprNode_traversFalseEnsuresConstraints
				    (exprData_getUopNode (data) ) );
	   break;
	   
    case XPR_CAST:

      ret = constraintList_addListFree (ret,
				    exprNode_traversFalseEnsuresConstraints
				    (exprData_getCastNode (data) ) );
      break;

    default:
      break;
    }

  return ret;
}


/* walk down the tree and get all requires Constraints in each subexpression*/
/*@only@*/ constraintList exprNode_traversRequiresConstraints (exprNode e)
{
  exprNode t1;

  bool handledExprNode;
  exprData data;
  constraintList ret;

   if (exprNode_handleError (e))
     {
       ret = constraintList_makeNew();
       return ret;
     }
  ret = constraintList_copy (e->requiresConstraints );
  
   handledExprNode = TRUE;
   
  data = e->edata;
  
  switch (e->kind)
    {
   case XPR_WHILEPRED:
      t1 = exprData_getSingle (data);
      ret = constraintList_addListFree ( ret, exprNode_traversRequiresConstraints (t1) );
      break;
      
    case XPR_FETCH:
      
      ret = constraintList_addListFree (ret,
				    exprNode_traversRequiresConstraints
				    (exprData_getPairA (data) ) );
        
      ret = constraintList_addListFree (ret,
				    exprNode_traversRequiresConstraints
				    (exprData_getPairB (data) ) );
      break;
    case XPR_PREOP:
          
      ret = constraintList_addListFree (ret,
				    exprNode_traversRequiresConstraints
				    (exprData_getUopNode (data) ) );
      break;
      
    case XPR_PARENS: 
      ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints
				    (exprData_getUopNode (data) ) );
      break;
    case XPR_INIT:
      ret = constraintList_addListFree (ret,
					exprNode_traversRequiresConstraints
					(exprData_getInitNode (data) ) );
	break;

    case XPR_ASSIGN:
        ret = constraintList_addListFree (ret,
				    exprNode_traversRequiresConstraints
				    (exprData_getOpA (data) ) );
        
       ret = constraintList_addListFree (ret,
				    exprNode_traversRequiresConstraints
				    (exprData_getOpB (data) ) );
       break;
    case XPR_OP:
       ret = constraintList_addListFree (ret,
				    exprNode_traversRequiresConstraints
				    (exprData_getOpA (data) ) );
        
       ret = constraintList_addListFree (ret,
				    exprNode_traversRequiresConstraints
				    (exprData_getOpB (data) ) );
       break;
    case XPR_SIZEOFT:
      break;
      
    case XPR_SIZEOF:
          
       ret = constraintList_addListFree (ret,
				    exprNode_traversRequiresConstraints
				     (exprData_getSingle (data) ) );
       break;
      
    case XPR_CALL:
      ret = constraintList_addListFree (ret,
				     exprNode_traversRequiresConstraints
				    (exprData_getFcn (data) ) );
      /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data) ); */
      break;
      
    case XPR_RETURN:
      ret = constraintList_addListFree (ret,
				    exprNode_traversRequiresConstraints
				    (exprData_getSingle (data) ) );
      break;
  
    case XPR_NULLRETURN:
      break;
            
    case XPR_FACCESS:
      ret = constraintList_addListFree (ret,
					exprNode_traversRequiresConstraints
					(exprData_getFieldNode (data) ) );
      break;
      
    case XPR_ARROW:
      ret = constraintList_addListFree (ret,
					exprNode_traversRequiresConstraints
					(exprData_getFieldNode (data) ) );
      break;
   
    case XPR_STRINGLITERAL:
      break;
      
    case XPR_NUMLIT:
      break;
    case XPR_POSTOP:

           ret = constraintList_addListFree (ret,
				    exprNode_traversRequiresConstraints
				    (exprData_getUopNode (data) ) );
	   break;
	   
    case XPR_CAST:

      ret = constraintList_addListFree (ret,
				    exprNode_traversRequiresConstraints
				    (exprData_getCastNode (data) ) );
      break;

    default:
      break;
    }

  return ret;
}


/* walk down the tree and get all Ensures Constraints in each subexpression*/
/*@only@*/ constraintList exprNode_traversEnsuresConstraints (exprNode e)
{
  exprNode t1;

  bool handledExprNode;
  exprData data;
  constraintList ret;


   if (exprNode_handleError (e))
     {
       ret = constraintList_makeNew();
       return ret;
     }
   
  ret = constraintList_copy (e->ensuresConstraints );   
   handledExprNode = TRUE;
   
  data = e->edata;

  DPRINTF( (message (
		     "exprnode_traversEnsuresConstraints call for %s with constraintList of %s",
		     exprNode_unparse (e),
		     constraintList_print(e->ensuresConstraints)
		     )
	    ));
  
  
  switch (e->kind)
    {
   case XPR_WHILEPRED:
      t1 = exprData_getSingle (data);
      ret = constraintList_addListFree ( ret,exprNode_traversEnsuresConstraints (t1) );
      break;
      
    case XPR_FETCH:
      
      ret = constraintList_addListFree (ret,
				    exprNode_traversEnsuresConstraints
				    (exprData_getPairA (data) ) );
        
      ret = constraintList_addListFree (ret,
				    exprNode_traversEnsuresConstraints
				    (exprData_getPairB (data) ) );
      break;
    case XPR_PREOP:
          
      ret = constraintList_addListFree (ret,
				    exprNode_traversEnsuresConstraints
				    (exprData_getUopNode (data) ) );
      break;
      
    case XPR_PARENS: 
      ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints
				    (exprData_getUopNode (data) ) );
      break;
      
    case XPR_INIT:
      ret = constraintList_addListFree (ret,
					exprNode_traversEnsuresConstraints
					(exprData_getInitNode (data) ) );
	break;


    case XPR_ASSIGN:
        ret = constraintList_addListFree (ret,
				    exprNode_traversEnsuresConstraints
				    (exprData_getOpA (data) ) );
        
       ret = constraintList_addListFree (ret,
				    exprNode_traversEnsuresConstraints
				    (exprData_getOpB (data) ) );
       break;
    case XPR_OP:
       ret = constraintList_addListFree (ret,
				    exprNode_traversEnsuresConstraints
				    (exprData_getOpA (data) ) );
        
       ret = constraintList_addListFree (ret,
				    exprNode_traversEnsuresConstraints
				    (exprData_getOpB (data) ) );
       break;
    case XPR_SIZEOFT:
      break;
      
    case XPR_SIZEOF:
          
       ret = constraintList_addListFree (ret,
				    exprNode_traversEnsuresConstraints
				     (exprData_getSingle (data) ) );
       break;
      
    case XPR_CALL:
      ret = constraintList_addListFree (ret,
				     exprNode_traversEnsuresConstraints
				    (exprData_getFcn (data) ) );
      /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data) ); */
      break;
      
    case XPR_RETURN:
      ret = constraintList_addListFree (ret,
				    exprNode_traversEnsuresConstraints
				    (exprData_getSingle (data) ) );
      break;
  
    case XPR_NULLRETURN:
      break;
            
    case XPR_FACCESS:
      ret = constraintList_addListFree (ret,
					exprNode_traversEnsuresConstraints
					(exprData_getFieldNode (data) ) );
      break;
   
    case XPR_ARROW:
      ret = constraintList_addListFree (ret,
					exprNode_traversEnsuresConstraints
					(exprData_getFieldNode (data) ) );
      break;
      
    case XPR_STRINGLITERAL:
      break;
      
    case XPR_NUMLIT:
      break;
    case XPR_POSTOP:

           ret = constraintList_addListFree (ret,
				    exprNode_traversEnsuresConstraints
				    (exprData_getUopNode (data) ) );
	   break;
    case XPR_CAST:

      ret = constraintList_addListFree (ret,
				    exprNode_traversEnsuresConstraints
				    (exprData_getCastNode (data) ) );
      break;
      
    default:
      break;
    }

  DPRINTF( (message (
		     "exprnode_traversEnsuresConstraints call for %s with constraintList of  is returning %s",
		     exprNode_unparse (e),
		     constraintList_print(ret))));
  
  return ret;
}

/*drl moved out of constraintResolve.c 07-02-001 */
void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist, fileloc sequencePoint)
{
  temp->requiresConstraints = constraintList_makeNew();
  temp->ensuresConstraints = constraintList_makeNew();
  temp->trueEnsuresConstraints = constraintList_makeNew();
  temp->falseEnsuresConstraints = constraintList_makeNew();
  
  exprNodeList_elements (arglist, el)
    {
      constraintList temp2;
      exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint);
      temp2 = el->requiresConstraints;
      el->requiresConstraints = exprNode_traversRequiresConstraints(el);
      constraintList_free(temp2);

      temp2 = el->ensuresConstraints;
      el->ensuresConstraints  = exprNode_traversEnsuresConstraints(el);
      constraintList_free(temp2);

      temp->requiresConstraints = constraintList_addList(temp->requiresConstraints,
							    el->requiresConstraints);
      
      temp->ensuresConstraints = constraintList_addList(temp->ensuresConstraints,
							   el->ensuresConstraints);
    }
  end_exprNodeList_elements;
  
}

/*drl moved out of constraintResolve.c 07-03-001 */
constraintList exprNode_getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall)
{
  constraintList postconditions;
  uentry temp;
  DPRINTF( (message ("Got call that %s ( %s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (arglist ) ) ) );

  temp = exprNode_getUentry (fcn);

  postconditions = uentry_getFcnPostconditions (temp);

  if (constraintList_isDefined (postconditions))
    {
      postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist);
      postconditions = constraintList_doFixResult (postconditions, fcnCall);
    }
  else
    {
      postconditions = constraintList_makeNew();
    }
  
  return postconditions;
}


/*drl moved out of constraintResolve.c 07-02-001 */
constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist)
{
  constraintList preconditions;
  uentry temp;
  DPRINTF( (message ("Got call that %s ( %s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (arglist ) ) ) );

  temp = exprNode_getUentry (fcn);

  preconditions = uentry_getFcnPreconditions (temp);

  if (constraintList_isDefined(preconditions) )
    {
      preconditions = constraintList_togglePost (preconditions);
      preconditions = constraintList_preserveCallInfo(preconditions, fcn);
      preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist);
    }
  else
    {
      if (constraintList_isUndefined(preconditions) )
	preconditions = constraintList_makeNew();
    }
  DPRINTF (( message("Done checkCall\n") ));
  DPRINTF (( message("Returning list %q ", constraintList_printDetailed(preconditions) ) ));
  return preconditions;
}