+
+ 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;
+ // char * mes;
+ 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_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:
+
+ // ctype_unparse (qtype_getType (exprData_getType (data) ) );
+
+ 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:
+ // cstring_makeLiteral ("return");;
+ break;
+
+ case XPR_FACCESS:
+ ret = constraintList_addListFree (ret,
+ exprNode_traversFalseEnsuresConstraints
+ (exprData_getFieldNode (data) ) );
+ //exprData_getFieldName (data) ;
+ break;
+
+ case XPR_ARROW:
+ ret = constraintList_addListFree (ret,
+ exprNode_traversFalseEnsuresConstraints
+ (exprData_getFieldNode (data) ) );
+ // exprData_getFieldName (data);
+ break;
+
+ case XPR_STRINGLITERAL:
+ // cstring_copy (exprData_getLiteral (data));
+ break;
+
+ case XPR_NUMLIT:
+ // cstring_copy (exprData_getLiteral (data));
+ 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;
+