Module shadow

This module contains an API for shadow memory. Shadow memory is a mechanism by which we can store metadata on memory locations, e.g. whether a memory location is initialized.

The main data structure provided by this module is the ShadowMem struct, which allows us to store metadata on a given memory location.

Example

use kani::shadow::ShadowMem;
use std::alloc::{alloc, Layout};

let mut sm = ShadowMem::new(false);

unsafe {
    let ptr = alloc(Layout::new::<u8>());
    // assert the memory location is not initialized
    assert!(!sm.get(ptr));
    // write to the memory location
    *ptr = 42;
    // update the shadow memory to indicate that this location is now initialized
    sm.set(ptr, true);
}

Structs

ShadowMem

A shadow memory data structure that contains a two-dimensional array of a generic type T. Each element of the outer array represents an object, and each element of the inner array represents a byte in the object.