Rewrite a specification function to a call to the specified function. The result of this rewriting is then parsed in `ExternSpecResolver`.
(item_fn: &mut syn::ItemFn, path: &mut syn::Path)
| 71 | /// Rewrite a specification function to a call to the specified function. |
| 72 | /// The result of this rewriting is then parsed in `ExternSpecResolver`. |
| 73 | fn rewrite_fn(item_fn: &mut syn::ItemFn, path: &mut syn::Path) { |
| 74 | let ident = &item_fn.sig.ident; |
| 75 | let args = &item_fn.sig.inputs; |
| 76 | let item_fn_span = item_fn.span(); |
| 77 | item_fn.block = parse_quote_spanned! {item_fn_span=> |
| 78 | { |
| 79 | #path :: #ident (#args); |
| 80 | unimplemented!() |
| 81 | } |
| 82 | }; |
| 83 | |
| 84 | item_fn.attrs.push(parse_quote_spanned!(item_fn_span=> #[prusti::extern_spec])); |
| 85 | item_fn.attrs.push(parse_quote_spanned!(item_fn_span=> #[trusted])); |
| 86 | } |
| 87 | |
| 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`. |