exprNode_doGenerateConstraintSwitch (switchExpr, body, &lastRequires,
&lastEnsures, &constraintsRequires, &constraintsEnsures);
/*@=mustfree@*/
exprNode_doGenerateConstraintSwitch (switchExpr, body, &lastRequires,
&lastEnsures, &constraintsRequires, &constraintsEnsures);
/*@=mustfree@*/