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
47
48
49
50
51
52

use syn::{FnArg, Ident, Pat, PatType, Receiver, Type};
use syn_path::path;

use super::{create_converted_type, create_pat_ident, create_type_path, create_type_reference};

#[derive(Clone)]
pub enum ArgType {
    Normal,
    Reference,
    #[allow(dead_code)]
    MutableReference,
}

pub fn create_self_arg(arg_ty: ArgType) -> FnArg {
    let ty = create_type_path(path!(Self));
    let (reference, mutability, ty) = match arg_ty {
        ArgType::Normal => (None, None, ty),
        ArgType::Reference => (
            Some((Default::default(), None)),
            None,
            create_type_reference(false, ty),
        ),
        ArgType::MutableReference => (
            Some(Default::default()),
            Some(Default::default()),
            create_type_reference(true, ty),
        ),
    };
    FnArg::Receiver(Receiver {
        attrs: vec![],
        reference,
        mutability,
        self_token: Default::default(),
        colon_token: None,
        ty: Box::new(ty),
    })
}

pub fn create_arg(arg_ty: ArgType, ident: Ident, ty: Option<Type>) -> FnArg {
    let ty = match ty {
        Some(ty) => ty,
        None => create_type_path(path!(Self)),
    };

    let ty = create_converted_type(arg_ty, ty);
    FnArg::Typed(PatType {
        attrs: vec![],
        pat: Box::new(Pat::Ident(create_pat_ident(ident))),
        colon_token: Default::default(),
        ty: Box::new(ty),
    })
}