core-models 0.0.5-pre.1

Models of the Rust core library
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

//! This module provides abstractions that are useful for writting
//! specifications in minicore. Currently it provides two abstractions: bits and
//! bit vectors.
//!
//! # Examples
//!
//! Converting an integer to a bit vector and back:
//!
//! ```rust
//! use core_models::abstractions::{bit::{Bit, MachineInteger}, bitvec::BitVec};
//!
//! // Create a BitVec from a machine integer (using the integer's bit-width)
//! let bv = BitVec::<16>::from_int(42u16);
//! println!("BitVec: {:?}", bv);
//!
//! // Convert the BitVec back into a machine integer
//! let n: u16 = bv.to_int();
//! println!("Integer: {}", n);
//!
//! assert!(n == 42);
//! ```

pub mod bit;
pub mod bitvec;
pub mod funarr;