private void createAssertions ( WyilFile . Decl declaration , List < VerificationCondition > vcs , GlobalEnvironment environment ) { // FIXME: should be logged somehow? for ( int i = 0 ; i != vcs . size ( ) ; ++ i ) { VerificationCondition vc = vcs . get ( i ) ; // Build the actual verification condition WyalFile . Stmt . Block verificationCondition = buildVerificationCondition ( declaration , environment , vc ) ; // Determine enclosing source unit Decl . Unit unit = declaration . getAncestor ( Decl . Unit . class ) ; // FIXME: this is not ideal Path . ID id = Trie . fromString ( unit . getName ( ) . toString ( ) . replaceAll ( "::" , "/" ) ) ; // Add generated verification condition as assertion WyalFile . Declaration . Assert assrt = new WyalFile . Declaration . Assert ( verificationCondition , vc . description , id , WhileyFile . ContentType ) ; allocate ( assrt , vc . getSpan ( ) ) ; } }
Turn each verification condition into an assertion in the underlying WyalFile being generated . The main challenge here is to ensure that all variables used in the assertion are properly typed .