conditional_panic/
conditional_panic.rs

1//! Example of inherently panicking system.
2//!
3//! Any machine-check formal verification of this system
4//! should return an inherent panic error with "Example panic 2"
5//! reached, as it is possible to reach it with a certain input.
6//!
7//! Only the things specific to the inherent panics will be commented
8//! here. See the example "counter" for a basic description
9//! of a machine-check system.
10
11#[machine_check::machine_description]
12mod machine_module {
13    use ::machine_check::Bitvector;
14    use ::std::{
15        clone::Clone,
16        cmp::{Eq, PartialEq},
17        fmt::Debug,
18        hash::Hash,
19    };
20
21    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
22    pub struct Input {
23        panic_input: Bitvector<8>,
24    }
25
26    impl ::machine_check::Input for Input {}
27
28    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
29    pub struct State {}
30
31    impl ::machine_check::State for State {}
32
33    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
34    pub struct System {}
35
36    // We can define support functions in inherent
37    // system implementations.
38    #[allow(dead_code, unreachable_code)]
39    impl System {
40        // This function simply panics.
41        // Currently, the treatment of panic as diverging
42        // is not supported, so the result must be still
43        // produced.
44        fn example_fn() -> ::machine_check::Bitvector<8> {
45            ::std::panic!("Example panic 1");
46            ::machine_check::Bitvector::<8>::new(0)
47        }
48    }
49
50    #[allow(unused_variables)]
51    impl ::machine_check::Machine for System {
52        type Input = Input;
53        type State = State;
54
55        fn init(&self, input: &Input) -> State {
56            State {}
57        }
58
59        #[allow(unreachable_code)]
60        fn next(&self, state: &State, input: &Input) -> State {
61            // Do not execute the following block.
62            if false {
63                // The example function can be called as an associated
64                // method, and would always panic (you can try it
65                // by changing the condition).
66                //
67                // Currently, it is necessary to assign the result
68                // to a variable. Since discovering the return type of other
69                // methods is not supported yet, its type must be explicitly
70                // specified.
71                let a: ::machine_check::Bitvector<8> = Self::example_fn();
72            }
73            // Panic if the input field panic_input is equal to 1.
74            if input.panic_input == Bitvector::<8>::new(1) {
75                // The first panic should win, i.e. "Example panic 2"
76                // inherent panic error should be returned when formally
77                // verifying with machine-check.
78                ::std::panic!("Example panic 2");
79                ::std::panic!("Example panic 3");
80            }
81            State {}
82        }
83    }
84}
85
86fn main() {
87    let system = machine_module::System {};
88    machine_check::run(system);
89}
conditional_panic/conditional_panic.rs

conditional_panic/
conditional_panic.rs
