private Context translateFail ( WyilFile . Stmt . Fail stmt , Context context ) { Expr condition = new Expr . Constant ( new Value . Bool ( false ) ) ; // VerificationCondition verificationCondition = new VerificationCondition ( "possible panic" , context . assumptions , condition , stmt . getParent ( WyilFile . Attribute . Span . class ) ) ; context . emit ( verificationCondition ) ; // return null ; }
Translate a fail statement . Execution should never reach such a statement . Hence we need to emit a verification condition to ensure this is the case .