private void translateFunctionOrMethodDeclaration ( WyilFile . Decl . FunctionOrMethod declaration ) { // Create the prototype for this function or method. This is the // function or method declaration which can be used within verification // conditions to refer to this function or method. This does not include // a body, since function or methods are treated as being // "uninterpreted" for the purposes of verification. createFunctionOrMethodPrototype ( declaration ) ; // Create macros representing the individual clauses of the function or // method's precondition and postcondition. These macros can then be // called either to assume the precondition/postcondition or to check // them. Using individual clauses helps to provide better error // messages. translatePreconditionMacros ( declaration ) ; translatePostconditionMacros ( declaration ) ; // The environments are needed to prevent clashes between variable // versions across verification conditions, and also to type variables // used in verification conditions. GlobalEnvironment globalEnvironment = new GlobalEnvironment ( declaration ) ; LocalEnvironment localEnvironment = new LocalEnvironment ( globalEnvironment ) ; // Generate the initial assumption set for a given function or method, // which roughly corresponds to its precondition. AssumptionSet assumptions = generateFunctionOrMethodAssumptionSet ( declaration , localEnvironment ) ; // Generate verification conditions by propagating forwards through the // control-flow graph of the function or method in question. For each // statement encountered, generate the preconditions which must hold // true at that point. Furthermore, generate the effect of this // statement on the current state. List < VerificationCondition > vcs = new ArrayList <> ( ) ; Context context = new Context ( wyalFile , assumptions , localEnvironment , localEnvironment , null , vcs ) ; translateStatementBlock ( declaration . getBody ( ) , context ) ; // // Translate each generated verification condition into an assertion in // the underlying WyalFile. createAssertions ( declaration , vcs , globalEnvironment ) ; }
Transform a function or method declaration into verification conditions as necessary . This is done by traversing the control - flow graph of the function or method in question . Verifications are emitted when conditions are encountered which must be checked . For example that the preconditions are met at a function invocation .