Rewrite all methods in an impl block to calls to the specified methods. The result of this rewriting is then parsed in `ExternSpecResolver`.
(
impl_item: &mut syn::ItemImpl,
new_ty: Box<syn::Type>,
)
| 88 | /// Rewrite all methods in an impl block to calls to the specified methods. |
| 89 | /// The result of this rewriting is then parsed in `ExternSpecResolver`. |
| 90 | pub fn rewrite_impl( |
| 91 | impl_item: &mut syn::ItemImpl, |
| 92 | new_ty: Box<syn::Type>, |
| 93 | ) -> syn::Result<TokenStream> { |
| 94 | let item_ty = &mut impl_item.self_ty; |
| 95 | if let syn::Type::Path(type_path) = item_ty.as_mut() { |
| 96 | for seg in type_path.path.segments.iter_mut() { |
| 97 | if let syn::PathArguments::AngleBracketed(genargs) = &mut seg.arguments { |
| 98 | genargs.colon2_token = Some(syn::token::Colon2::default()); |
| 99 | } |
| 100 | } |
| 101 | } |
| 102 | |
| 103 | for item in impl_item.items.iter_mut() { |
| 104 | let item_span = item.span(); |
| 105 | match item { |
| 106 | syn::ImplItem::Method(method) => { |
| 107 | for attr in method.attrs.iter_mut() { |
| 108 | attr.tokens = rewrite_self(attr.tokens.clone()); |
| 109 | } |
| 110 | |
| 111 | let args = rewrite_method_inputs(item_ty, method); |
| 112 | let ident = &method.sig.ident; |
| 113 | |
| 114 | method.attrs.push(parse_quote_spanned!(item_span=> #[prusti::extern_spec])); |
| 115 | method.attrs.push(parse_quote_spanned!(item_span=> #[trusted])); |
| 116 | |
| 117 | let mut method_path: syn::ExprPath = parse_quote_spanned! {ident.span()=> |
| 118 | #item_ty :: #ident |
| 119 | }; |
| 120 | |
| 121 | // Fix the span |
| 122 | syn::visit_mut::visit_expr_path_mut( |
| 123 | &mut SpanOverrider::new(ident.span()), |
| 124 | &mut method_path |
| 125 | ); |
| 126 | |
| 127 | method.block = parse_quote_spanned! {item_span=> |
| 128 | { |
| 129 | #method_path (#args); |
| 130 | unimplemented!() |
| 131 | } |
| 132 | }; |
| 133 | } |
| 134 | _ => { |
| 135 | return Err(syn::Error::new( |
| 136 | item.span(), |
| 137 | "expected a method".to_string(), |
| 138 | )); |
| 139 | } |
| 140 | } |
| 141 | } |
| 142 | impl_item.self_ty = new_ty; |
| 143 | |
| 144 | Ok(quote! { |
| 145 | #impl_item |
| 146 | }) |
| 147 | } |
nothing calls this directly
no test coverage detected