machine-check-machine 0.7.1

Utility crate for the formal verification tool machine-check
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46

use syn::{
    visit_mut::{self, VisitMut},
    Attribute, Meta,
};

use crate::{Description, Error};

pub fn strip_machine(machine: &mut Description) -> Result<(), Error> {
    let mut visitor = BlockVisitor {};
    for item in machine.items.iter_mut() {
        visitor.visit_item_mut(item);
    }
    Ok(())
}

struct BlockVisitor {}
impl VisitMut for BlockVisitor {
    fn visit_local_mut(&mut self, node: &mut syn::Local) {
        strip_attributes(&mut node.attrs);
        visit_mut::visit_local_mut(self, node);
    }
    fn visit_expr_call_mut(&mut self, node: &mut syn::ExprCall) {
        strip_attributes(&mut node.attrs);
        visit_mut::visit_expr_call_mut(self, node);
    }
}

fn strip_attributes(attrs: &mut Vec<Attribute>) {
    let mut i = 0;
    while i < attrs.len() {
        let attr = &attrs[i];
        if let Meta::NameValue(meta) = &attr.meta {
            if meta.path.leading_colon.is_some()
                && meta.path.segments.len() > 2
                && &meta.path.segments[0].ident.to_string() == "mck"
                && &meta.path.segments[1].ident.to_string() == "attr"
            {
                // remove attribute
                attrs.remove(i);
            } else {
                // leave as-is, increment i
                i += 1;
            }
        }
    }
}