mirror of https://codeberg.org/topola/topola.git
contracts: Replace `return` with block break
Without that, postconditions were skipped.
This commit is contained in:
parent
1a271cd89c
commit
d286f5c182
|
|
@ -4,7 +4,10 @@
|
||||||
|
|
||||||
use proc_macro2::{Ident, Span, TokenStream};
|
use proc_macro2::{Ident, Span, TokenStream};
|
||||||
use quote::ToTokens;
|
use quote::ToTokens;
|
||||||
use syn::{spanned::Spanned, visit_mut as visitor, Attribute, Expr, ExprCall};
|
use syn::{
|
||||||
|
spanned::Spanned, visit_mut as visitor, Attribute, Expr, ExprCall,
|
||||||
|
ReturnType, Type,
|
||||||
|
};
|
||||||
|
|
||||||
use crate::implementation::{
|
use crate::implementation::{
|
||||||
Contract, ContractMode, ContractType, FuncWithContracts,
|
Contract, ContractMode, ContractType, FuncWithContracts,
|
||||||
|
|
@ -313,12 +316,22 @@ pub(crate) fn generate(
|
||||||
};
|
};
|
||||||
|
|
||||||
//
|
//
|
||||||
// wrap the function body in a closure if we have any postconditions
|
// wrap the function body in a block so that we can use its return value
|
||||||
//
|
//
|
||||||
|
|
||||||
let body = {
|
let body = 'blk: {
|
||||||
let block = &func.function.block;
|
let mut block = func.function.block.clone();
|
||||||
quote::quote! { let ret = #block; }
|
syn::visit_mut::visit_block_mut(&mut ReturnReplacer {}, &mut block);
|
||||||
|
|
||||||
|
if let ReturnType::Type(.., ref return_type) = func.function.sig.output
|
||||||
|
{
|
||||||
|
if let Type::ImplTrait(..) = **return_type {
|
||||||
|
} else {
|
||||||
|
break 'blk quote::quote! { let ret: #return_type = 'run: #block; };
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
quote::quote! { let ret = 'run: #block; }
|
||||||
};
|
};
|
||||||
|
|
||||||
//
|
//
|
||||||
|
|
@ -352,14 +365,13 @@ pub(crate) fn generate(
|
||||||
func.function.into_token_stream()
|
func.function.into_token_stream()
|
||||||
}
|
}
|
||||||
|
|
||||||
struct SelfReplacer<'a> {
|
struct ReturnReplacer {}
|
||||||
replace_with: &'a syn::Ident,
|
|
||||||
}
|
|
||||||
|
|
||||||
impl syn::visit_mut::VisitMut for SelfReplacer<'_> {
|
impl syn::visit_mut::VisitMut for ReturnReplacer {
|
||||||
fn visit_ident_mut(&mut self, i: &mut Ident) {
|
fn visit_expr_mut(&mut self, node: &mut Expr) {
|
||||||
if i == "self" {
|
if let Expr::Return(retexpr) = node {
|
||||||
*i = self.replace_with.clone();
|
let retexprexpr = retexpr.expr.clone();
|
||||||
|
*node = syn::parse_quote!(break 'run #retexprexpr);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue