private Context translateAssert ( WyilFile . Stmt . Assert stmt , Context context ) { Pair < Expr , Context > p = translateExpressionWithChecks ( stmt . getCondition ( ) , null , context ) ; Expr condition = p . first ( ) ; context = p . second ( ) ; // VerificationCondition verificationCondition = new VerificationCondition ( "assertion failed" , context . assumptions , condition , stmt . getCondition ( ) . getParent ( WyilFile . Attribute . Span . class ) ) ; context . emit ( verificationCondition ) ; // return context . assume ( condition ) ; }
Translate an assert statement . This emits a verification condition which ensures the assert condition holds given the current context .