verify-rust-std/stdarch.patch at 3cae612d267d360ccc1abc1b3a3d5cbec1f2abe1 · tautschnig/verify-rust-std · GitHub

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
--- a/crates/core_arch/src/aarch64/neon/mod.rs
+++ b/crates/core_arch/src/aarch64/neon/mod.rs
@@ -2,6 +2,9 @@

 #![allow(non_camel_case_types)]

+#[cfg(kani)]
+use crate::kani;
+
 #[rustfmt::skip]
 mod generated;
 #[rustfmt::skip]
--- a/crates/core_arch/src/arm_shared/neon/mod.rs
+++ b/crates/core_arch/src/arm_shared/neon/mod.rs
@@ -1,5 +1,8 @@
 //! ARMv7 NEON intrinsics

+#[cfg(kani)]
+use crate::kani;
+
 #[rustfmt::skip]
 mod generated;
 #[rustfmt::skip]
--- a/crates/core_arch/src/macros.rs
+++ b/crates/core_arch/src/macros.rs
@@ -128,6 +128,15 @@ macro_rules! types {
             }
         }

+        #[cfg(kani)]
+        $(#[$stability])+
+        impl kani::Arbitrary for $name {
+            fn any() -> Self {
+                let data: [$elem_type; $len] = kani::any();
+                Self { 0: data }
+            }
+        }
+
         $(#[$stability])+
         impl crate::fmt::Debug for $name {
             #[inline]
--- a/crates/core_arch/src/x86/mod.rs
+++ b/crates/core_arch/src/x86/mod.rs
@@ -1,5 +1,7 @@
 //! `x86` and `x86_64` intrinsics.

+#[cfg(kani)]
+use crate::kani;
 use crate::mem::transmute;

 #[macro_use]