private Context translateIf ( WyilFile . Stmt . IfElse stmt , Context context ) { // Pair < Expr , Context > p = translateExpressionWithChecks ( stmt . getCondition ( ) , null , context ) ; Expr trueCondition = p . first ( ) ; // FIXME: this is broken as includes assumptions propagated through // logical &&'s context = p . second ( ) ; Expr falseCondition = invertCondition ( trueCondition , stmt . getCondition ( ) ) ; // Context trueContext = context . assume ( trueCondition ) ; Context falseContext = context . assume ( falseCondition ) ; // trueContext = translateStatementBlock ( stmt . getTrueBranch ( ) , trueContext ) ; if ( stmt . hasFalseBranch ( ) ) { falseContext = translateStatementBlock ( stmt . getFalseBranch ( ) , falseContext ) ; } // Finally, we must join the two context's back together. This ensures // that information from either side is properly preserved return joinDescendants ( context , new Context [ ] { trueContext , falseContext } ) ; }
Translate an if statement . This translates the true and false branches and then recombines them together to form an updated environment . This is challenging when the environments are updated independently in both branches .