forked from project-oak/rust-verification-tools
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathenumeration.rs
60 lines (52 loc) · 1.74 KB
/
enumeration.rs
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
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
// Copyright 2020 The Propverify authors
// Based on parts of Proptest which is Copyright 2017, 2018 Jason Lingle
//
// Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
// option. This file may not be copied, modified, or distributed
// except according to those terms.
////////////////////////////////////////////////////////////////
// Proptest-based tests exploring how to use proptest with
// enumerations
////////////////////////////////////////////////////////////////
#[cfg(not(verify))]
use proptest::prelude::*;
#[cfg(verify)]
use propverify::prelude::*;
////////////////////////////////////////////////////////////////
// An enumeration type
//
// Example taken from proptest
////////////////////////////////////////////////////////////////
#[cfg(test)]
mod test {
use super::*;
use core::fmt::Debug;
#[derive(Clone, Debug)]
enum MyEnum {
Big(u64),
Medium(u32),
Little(i16),
}
fn my_enum_strategy(s: u8) -> impl Strategy<Value = MyEnum> {
prop_oneof![
(0..i16::from(s)).prop_map(MyEnum::Little),
(0..u32::from(s)).prop_map(MyEnum::Medium),
(0..u64::from(s)).prop_map(MyEnum::Big),
]
}
proptest! {
#[test]
fn enum_test1(x in my_enum_strategy(10)) {
match x {
MyEnum::Big(b) => assert!(b < 10),
MyEnum::Medium(m) => assert!(m < 10),
MyEnum::Little(l) => assert!(l < 10)
}
}
}
}
////////////////////////////////////////////////////////////////
// End
////////////////////////////////////////////////////////////////