prusti_specs/extern_spec_rewriter/
mods.rs

1//! Process external specifications in Rust modules marked with the
2//! #[extern_spec] attribute. Nested modules are processed recursively.
3//! Specifications are collected from functions and function stubs.
4//!
5//! Modules are rewritten so that their name does not clash with the module
6//! they are specifying.
7
8use super::{
9    common::check_is_stub,
10    functions::{rewrite_fn, rewrite_stub},
11};
12use proc_macro2::TokenStream;
13use syn::spanned::Spanned;
14
15pub fn rewrite_mod(item_mod: &syn::ItemMod, mut path: syn::Path) -> syn::Result<TokenStream> {
16    path.segments.push(syn::PathSegment {
17        ident: item_mod.ident.clone(),
18        arguments: syn::PathArguments::None,
19    });
20
21    let mut rewritten_fns = TokenStream::new();
22    for item in item_mod.content.as_ref().iter().flat_map(|c| &c.1) {
23        match item {
24            syn::Item::Fn(ref item_fn) => {
25                check_is_stub(&item_fn.block)?;
26                rewritten_fns.extend(rewrite_fn(item_fn, &path, false));
27            }
28            syn::Item::Mod(ref inner_mod) => rewritten_fns.extend(rewrite_mod(inner_mod, path.clone())?),
29            syn::Item::Verbatim(ref tokens) => rewritten_fns.extend(rewrite_stub(tokens, &path, false)?),
30            syn::Item::Use(_) => rewritten_fns.extend(syn::Error::new(
31                item.span(),
32                "`use` statements have no effect in #[extern_spec] modules; module contents share the outer scope.",
33            ).to_compile_error()),
34            _ => return Err(syn::Error::new(item.span(), "unexpected item")),
35        }
36    }
37
38    Ok(rewritten_fns)
39}
prusti_specs/extern_spec_rewriter/mods.rs

prusti_specs/extern_spec_rewriter/
mods.rs
