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

use machine_check_common::iir::stmt::{IAssignStmt, IIfStmt, IStmt};

use crate::{
    into_iir::func::WFnData,
    wir::{WStmt, ZConverted},
    Error,
};

impl WStmt<ZConverted> {
    pub(super) fn into_iir(self, fn_data: &WFnData) -> Result<Option<IStmt>, Error> {
        Ok(match self {
            WStmt::Assign(stmt_assign) => {
                let left_ident = stmt_assign.left.into_iir();
                let left = fn_data
                    .ident_var(&left_ident)
                    .expect("Left-side variable should be in variable map");

                let right = stmt_assign.right.into_iir(fn_data)?;

                right.map(|right| IStmt::Assign(IAssignStmt { left, right }))
            }
            WStmt::If(stmt_if) => {
                let condition = stmt_if.condition.ident.into_iir();

                let condition = fn_data
                    .ident_var(&condition)
                    .expect("Condition variable should be in variable map");

                let then_block = stmt_if.then_block.into_iir(fn_data)?;
                let else_block = stmt_if.else_block.into_iir(fn_data)?;

                Some(IStmt::If(IIfStmt {
                    condition,
                    then_block,
                    else_block,
                }))
            }
        })
    }
}