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
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78

use syn::{Expr, ExprAssign, Ident, Local, LocalInit, Pat, PatIdent, PatType, Stmt, Type};

use super::{create_expr_path, create_path_from_ident};

fn create_let_mut_choice(
    mutable: bool,
    left_ident: Ident,
    right_expr: Option<Expr>,
    ty: Option<Type>,
) -> Local {
    let mutability = if mutable {
        Some(Default::default())
    } else {
        None
    };
    let mut left_pat = Pat::Ident(PatIdent {
        attrs: vec![],
        by_ref: None,
        mutability,
        ident: left_ident,
        subpat: None,
    });
    if let Some(ty) = ty {
        left_pat = Pat::Type(PatType {
            attrs: vec![],
            pat: Box::new(left_pat),
            colon_token: Default::default(),
            ty: Box::new(ty),
        });
    }
    let init = right_expr.map(|right_expr| LocalInit {
        eq_token: Default::default(),
        expr: Box::new(right_expr),
        diverge: None,
    });

    Local {
        attrs: vec![],
        let_token: Default::default(),
        pat: left_pat,
        init,
        semi_token: Default::default(),
    }
}

pub fn create_let(left_ident: Ident, right_expr: Expr, ty: Option<Type>) -> Stmt {
    Stmt::Local(create_let_mut_choice(
        false,
        left_ident,
        Some(right_expr),
        ty,
    ))
}

pub fn create_let_bare(ident: Ident, ty: Option<Type>) -> Stmt {
    Stmt::Local(create_let_mut_choice(false, ident, None, ty))
}

pub fn create_assign(left_ident: Ident, right_expr: Expr, semicolon: bool) -> Stmt {
    Stmt::Expr(
        create_assign_expr(left_ident, right_expr),
        if semicolon {
            Some(Default::default())
        } else {
            None
        },
    )
}

fn create_assign_expr(left_ident: Ident, right_expr: Expr) -> Expr {
    let left_expr = create_expr_path(create_path_from_ident(left_ident));
    Expr::Assign(ExprAssign {
        attrs: vec![],
        left: Box::new(left_expr),
        eq_token: Default::default(),
        right: Box::new(right_expr),
    })
}