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

use proc_macro2::Span;

use crate::wir::WIdent;

pub struct IdentCreator {
    prefix: String,
    next_temp_counter: u64,
    created_temporaries: Vec<WIdent>,
}

impl IdentCreator {
    pub fn new(prefix: String) -> Self {
        IdentCreator {
            prefix,
            next_temp_counter: 0,
            created_temporaries: Vec::new(),
        }
    }

    pub fn create_temporary_ident(&mut self, span: Span) -> WIdent {
        let tmp_ident = WIdent::new(
            format!("__mck_{}tmp_{}", self.prefix, self.next_temp_counter),
            span,
        );
        self.created_temporaries.push(tmp_ident.clone());

        self.next_temp_counter = self
            .next_temp_counter
            .checked_add(1)
            .expect("Temp counter should not overflow");
        tmp_ident
    }

    pub fn drain_created_temporaries(&mut self) -> impl Iterator<Item = WIdent> + use<'_> {
        self.created_temporaries.drain(..)
    }
}