trame-runtime 0.1.0

Runtime traits and implementations for trame
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

use creusot_std::prelude::*;

use crate::IHeap;

use super::{CHeap, CPtr, CShapeHandle, CShapeStore, init_fact, shape_is_scalar, shape_size};

/// Sanity check: `can_drop` matches init membership.
#[check(ghost)]
pub fn can_drop_matches_init(store: &CShapeStore, handle: CShapeHandle, heap: CHeap, ptr: CPtr) {
    let shape = super::CShapeView { store, handle };
    proof_assert!(
        if shape_is_scalar(shape) {
            heap.can_drop(ptr, shape) == heap.range_init(ptr, shape_size(shape))
        } else {
            heap.can_drop(ptr, shape)
                == heap@.init.contains(init_fact(
                    ptr.alloc_id,
                    ptr.offset as usize,
                    shape.handle
                ))
        }
    );
}