machine-check-common 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

use indexmap::IndexMap;

use crate::iir::{
    description::{IFnId, IStruct, IStructId},
    func::IFn,
    path::IIdent,
};

#[derive(Clone, Debug)]
pub struct IFnContext<'a> {
    pub func: &'a IFn,
    pub context: &'a IContext<'a>,
}

#[derive(Clone, Debug)]
pub struct IContext<'a> {
    pub structs: Option<&'a IndexMap<IIdent, IStruct>>,
}

impl IContext<'_> {
    pub fn empty() -> IContext<'static> {
        IContext { structs: None }
    }

    pub fn struct_with_id(&self, id: IStructId) -> &IStruct {
        let Some(structs) = self.structs else {
            panic!("Should have structs when looking up one");
        };
        structs
            .get_index(id.0)
            .expect("Struct with given id should exist")
            .1
    }

    pub fn fn_with_id(&self, id: IFnId) -> &IFn {
        self.struct_with_id(id.struct_id)
            .fns
            .get_index(id.fn_index)
            .expect("Call with given id should exist")
            .1
    }
}