private void generatePostconditionChecks ( WyilFile . Stmt . Return stmt , Expr [ ] exprs , Context context ) { WyilFile . Decl . FunctionOrMethod declaration = ( WyilFile . Decl . FunctionOrMethod ) context . getEnvironment ( ) . getParent ( ) . enclosingDeclaration ; WyilFile . Tuple < WyilFile . Expr > postcondition = declaration . getEnsures ( ) ; Tuple < WyilFile . Decl . Variable > parameters = declaration . getParameters ( ) ; Tuple < WyilFile . Decl . Variable > returns = declaration . getReturns ( ) ; // First, check whether or not there are any postconditions! if ( postcondition . size ( ) > 0 ) { // There is at least one return value and at least one // postcondition clause. Therefore, we need to check the return // values against the post condition(s). One of the difficulties // here is that the postcondition will refer to parameters as // they were on entry to the function/method, not as they are // now. Expr [ ] arguments = new Expr [ parameters . size ( ) + returns . size ( ) ] ; // Translate parameters as arguments to post-condition // invocation for ( int i = 0 ; i != parameters . size ( ) ; ++ i ) { WyilFile . Decl . Variable var = parameters . get ( i ) ; WyalFile . VariableDeclaration vd = context . readFirst ( var ) ; arguments [ i ] = new Expr . VariableAccess ( vd ) ; } // Copy over return expressions as arguments for invocation(s) System . arraycopy ( exprs , 0 , arguments , parameters . size ( ) , exprs . length ) ; // // Finally, generate an appropriate verification condition to // check each postcondition clause for ( int i = 0 ; i != postcondition . size ( ) ; ++ i ) { Name ident = convert ( declaration . getQualifiedName ( ) , "_ensures_" + i , declaration . getName ( ) ) ; Expr clause = new Expr . Invoke ( null , ident , null , arguments ) ; context . emit ( new VerificationCondition ( "postcondition may not be satisfied" , context . assumptions , clause , stmt . getParent ( WyilFile . Attribute . Span . class ) ) ) ; } } }
Generate the post - condition checks necessary at a return statement in a function or method .