rapx 0.7.31

A static analysis platform for Rust program analysis and verification
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

/// Identifies a memory slot: a local variable with optional field projections.
#[derive(Debug, Clone, Hash, PartialEq, Eq)]
pub struct Slot {
    pub local: usize,
    pub fields: Vec<usize>,
}

impl Slot {
    pub fn new(local: usize) -> Self {
        Slot {
            local,
            fields: Vec::new(),
        }
    }

    pub fn project(&self, field_idx: usize) -> Self {
        let mut fields = self.fields.clone();
        fields.push(field_idx);
        Slot {
            local: self.local,
            fields,
        }
    }
}

/// An abstract memory location a pointer can point to.
#[derive(Debug, Clone, Hash, PartialEq, Eq)]
pub enum AbstractLoc {
    Slot(Slot),
    Null,
}