private Context translateSwitch ( WyilFile . Stmt . Switch stmt , Context context ) { Tuple < WyilFile . Stmt . Case > cases = stmt . getCases ( ) ; // Pair < Expr , Context > p = translateExpressionWithChecks ( stmt . getCondition ( ) , null , context ) ; Expr value = p . first ( ) ; context = p . second ( ) ; // WyalFile . Stmt defaultValue = null ; Context [ ] descendants = new Context [ cases . size ( ) + 1 ] ; Context defaultContext = null ; boolean hasDefault = false ; // for ( int i = 0 ; i != cases . size ( ) ; ++ i ) { WyilFile . Stmt . Case caSe = cases . get ( i ) ; Context caseContext ; // Setup knowledge from case values if ( ! caSe . isDefault ( ) ) { WyalFile . Stmt e = null ; for ( WyilFile . Expr constant : caSe . getConditions ( ) ) { // Expr v = convert(constant, stmt, context.getEnvironment()); Expr v = translateExpression ( constant , null , context . getEnvironment ( ) ) ; e = or ( e , new Expr . Equal ( value , v ) ) ; defaultValue = and ( defaultValue , new Expr . NotEqual ( value , v ) ) ; } caseContext = context . assume ( e ) ; descendants [ i ] = translateStatementBlock ( caSe . getBlock ( ) , caseContext ) ; } else { defaultContext = context . assume ( defaultValue ) ; defaultContext = translateStatementBlock ( caSe . getBlock ( ) , defaultContext ) ; hasDefault = true ; } } // Sort out default context if ( ! hasDefault ) { // indicates no default block was present, so we just assume what we // know and treat it as a fall through. defaultContext = context . assume ( defaultValue ) ; } descendants [ descendants . length - 1 ] = defaultContext ; // return joinDescendants ( context , descendants ) ; }
Translate a switch statement .