machine_check

Function run

Source 
pub fn run<M: FullMachine>(system: M) -> ExecResult
Expand description

Executes machine-check with system environment arguments.

Is supposed to be used for simple systems that do not take arguments.

The system must implement Machine. The system structures and Input, State, and Machine implementations must be enclosed within the machine_description macro, which processes them to enable fast and efficient formal verification.

Examples found in repository?
examples/conditional_panic.rs (line 88)
86fn main() {
87    let system = machine_module::System {};
88    machine_check::run(system);
89}
More examples
Hide additional examples
examples/counter.rs (line 111)
107fn main() {
108    // Construct the system. This one has no unchanging data.
109    let system = machine_module::System {};
110    // Run machine-check with the constructed system.
111    machine_check::run(system);
112}
examples/timed_panic.rs (line 71)
67fn main() {
68    // Construct the system. This one has no unchanging data.
69    let system = machine_module::System {};
70    // Run machine-check with the constructed system.
71    machine_check::run(system);
72}
examples/simple_risc.rs (line 147)
116fn main() {
117    let toy_program = [
118        // (0) set r0 to zero
119        Bitvector::new(0b0100_0000_0000),
120        // (1) set r1 to one
121        Bitvector::new(0b0101_0000_0001),
122        // (2) set r2 to zero
123        Bitvector::new(0b0110_0000_0000),
124        // --- main loop ---
125        // (3) store r1 content to data location 0
126        Bitvector::new(0b1100_0000_0000),
127        // (4) store r2 content to data location 1
128        Bitvector::new(0b1100_0000_0001),
129        // (5) read input location 0 to r3
130        Bitvector::new(0b0011_0100_0000),
131        // (6) jump to (3) if r3 bit 0 is set
132        Bitvector::new(0b0011_1000_0011),
133        // (7) increment r2
134        Bitvector::new(0b0010_0000_1001),
135        // (8) store r2 content to data location 1
136        Bitvector::new(0b1110_0000_0001),
137        // (9) jump to (3)
138        Bitvector::new(0b0001_1000_0011),
139    ];
140
141    // load toy program to program memory, filling unused locations with 0
142    let mut progmem = BitvectorArray::new_filled(Bitvector::new(0));
143    for (index, instruction) in toy_program.into_iter().enumerate() {
144        progmem[Bitvector::new(index as u64)] = instruction;
145    }
146    let system = machine_module::System { progmem };
147    machine_check::run(system);
148}