tests(s2n-quic-core): kani test for packet number map (#1508)

aws · Mar 29, 2023 · 1554b98 · 1554b98
1 parent 1ab3385
commit 1554b98
Showing 1 changed file with 17 additions and 0 deletions.
diff --git a/quic/s2n-quic-core/src/packet/number/map.rs b/quic/s2n-quic-core/src/packet/number/map.rs
@@ -769,4 +769,21 @@ mod tests {
             .with_type::<Vec<Operation>>()
             .for_each(|ops| model(ops))
     }
+
+    #[test]
+    #[cfg_attr(kani, kani::proof, kani::unwind(9), kani::solver(kissat))]
+    fn insert_value() {
+        // Confirm that a value is inserted
+        check!().with_type().cloned().for_each(|pn| {
+            let space = PacketNumberSpace::ApplicationData;
+            let mut map = Map::default();
+            assert!(map.is_empty());
+            let pn = space.new_packet_number(pn);
+
+            map.insert(pn, ());
+
+            assert!(map.get(pn).is_some());
+            assert!(!map.is_empty());
+        });
+    }
 }