Replace thrust:: with thrust_macros:: for requires/ensures in UI tests

std.rs

@@ -172,30 +172,62 @@ mod thrust_models {
         type Ty = model::Int;
     }
 
-    impl Model for isize {
-        type Ty = model::Int;
-    }
+    macro_rules! int_model {
+        ($T:ty) => {
+            impl Model for $T {
+                type Ty = model::Int;
+            }
 
-    impl Model for i32 {
-        type Ty = model::Int;
-    }
+            impl PartialEq<model::Int> for $T {
+                #[thrust::ignored]
+                fn eq(&self, _other: &model::Int) -> bool {
+                    unimplemented!()
+                }
+            }
 
-    impl Model for i64 {
-        type Ty = model::Int;
-    }
+            impl PartialOrd<model::Int> for $T {
+                #[thrust::ignored]
+                fn partial_cmp(&self, _other: &model::Int) -> Option<std::cmp::Ordering> {
+                    unimplemented!()
+                }
+            }
 
-    impl Model for usize {
-        type Ty = model::Int;
-    }
+            impl std::ops::Add<model::Int> for $T {
+                type Output = model::Int;
 
-    impl Model for u32 {
-        type Ty = model::Int;
-    }
+                #[thrust::ignored]
+                fn add(self, _rhs: model::Int) -> Self::Output {
+                    unimplemented!()
+                }
+            }
 
-    impl Model for u64 {
-        type Ty = model::Int;
+            impl std::ops::Sub<model::Int> for $T {
+                type Output = model::Int;
+
+                #[thrust::ignored]
+                fn sub(self, _rhs: model::Int) -> Self::Output {
+                    unimplemented!()
+                }
+            }
+
+            impl std::ops::Mul<model::Int> for $T {
+                type Output = model::Int;
+
+                #[thrust::ignored]
+                fn mul(self, _rhs: model::Int) -> Self::Output {
+                    unimplemented!()
+                }
+            }
+        };
     }
 
+    int_model!(isize);
+    int_model!(i32);
+    int_model!(i64);
+    int_model!(usize);
+    int_model!(u32);
+    int_model!(u64);
+
     impl Model for bool {
         type Ty = bool;
     }

tests/ui/fail/adt.rs

@@ -6,9 +6,13 @@ pub enum X {
     B(bool),
 }
 
+impl thrust_models::Model for X {
+    type Ty = Self;
+}
+
 #[thrust::trusted]
-#[thrust::requires(true)]
-#[thrust::ensures(true)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(true)]
 fn rand() -> X { unimplemented!() }
 
 fn inv(x: X) -> X {

tests/ui/fail/adt_mut.rs

@@ -11,8 +11,8 @@ impl thrust_models::Model for X {
 }
 
 #[thrust::trusted]
-#[thrust::requires(true)]
-#[thrust::ensures(true)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(true)]
 fn rand() -> X { unimplemented!() }
 
 fn inv(x: &mut X) {

tests/ui/fail/adt_poly_fn_mono.rs

@@ -5,9 +5,13 @@ pub enum X<T> {
     A(T),
 }
 
+impl<T> thrust_models::Model for X<T> {
+    type Ty = Self;
+}
+
 #[thrust::trusted]
-#[thrust::requires(true)]
-#[thrust::ensures(true)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(true)]
 fn rand() -> X<i32> { unimplemented!() }
 
 fn inv(x: X<i32>) -> X<i32> {

tests/ui/fail/adt_poly_fn_poly.rs

@@ -5,9 +5,13 @@ pub enum X<T> {
     B(T),
 }
 
+impl<T> thrust_models::Model for X<T> {
+    type Ty = Self;
+}
+
 #[thrust::trusted]
-#[thrust::requires(true)]
-#[thrust::ensures(true)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(true)]
 fn rand<T>() -> X<T> { unimplemented!() }
 
 fn is_a<T>(x: &X<T>) -> bool {

tests/ui/fail/annot.rs

@@ -1,7 +1,7 @@
 //@error-in-other-file: Unsat
 
-#[thrust::requires(true)]
-#[thrust::ensures(result != x)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result != x)]
 fn rand_except(x: i64) -> i64 {
     if x == 0 {
         1
@@ -10,8 +10,8 @@ fn rand_except(x: i64) -> i64 {
     }
 }
 
-#[thrust::requires(true)]
-#[thrust::ensures((result == 1) || (result == -1) && result == 0)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures((result == 1) || (result == -1) && result == 0)]
 fn f(x: i64) -> i64 {
     let y = rand_except(x);
     if y > x {

tests/ui/fail/annot_box_term.rs

@@ -6,7 +6,7 @@ fn box_create(x: i64) -> Box<i64> {
     Box::new(x)
 }
 
-#[thrust::requires(b == <v>)]
+#[thrust_macros::requires(b == thrust_models::model::Box::new(v))]
 fn box_consume(b: Box<i64>, v: i64) {
     assert!(*b == v);
 }

tests/ui/fail/enum_ref_drop.rs

@@ -7,8 +7,8 @@ pub enum X<'a, 'b> {
 }
 
 #[thrust::trusted]
-#[thrust::requires(true)]
-#[thrust::ensures(true)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(true)]
 fn rand() -> i64 { unimplemented!() }
 
 fn x(i: &mut i64) -> X {

tests/ui/fail/extern_spec_take.rs

@@ -1,8 +1,8 @@
 //@error-in-other-file: Unsat
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(result == *dest && ^dest == 0)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result == *dest && !dest == 0)]
 fn _extern_spec_take(dest: &mut i32) -> i32 {
     std::mem::take(dest)
 }

tests/ui/fail/fn_poly_annot.rs

@@ -1,7 +1,7 @@
 //@error-in-other-file: Unsat
 
-#[thrust::requires(true)]
-#[thrust::ensures(result != x.0)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result != x.0)]
 fn left<T, U>(x: (T, U)) -> T {
     x.0
 }

tests/ui/fail/fn_poly_annot_complex.rs

@@ -1,7 +1,7 @@
 //@error-in-other-file: Unsat
 
-#[thrust::requires((x.0 > 0) && (x.1 > 0))]
-#[thrust::ensures((result.0 == x.1) && (result.1 == x.0))]
+#[thrust_macros::requires((x.0 > 0) && (x.1 > 0))]
+#[thrust_macros::ensures((result.0 == x.1) && (result.1 == x.0))]
 fn swap_positive<T, U>(x: (i32, i32, T, U)) -> (i32, i32, U, T) {
     (x.1, x.0, x.3, x.2)
 }

tests/ui/fail/fn_poly_annot_multi_inst.rs

@@ -1,7 +1,7 @@
 //@error-in-other-file: Unsat
 
-#[thrust::requires(true)]
-#[thrust::ensures(result == x)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result == x)]
 fn id<T>(x: T) -> T {
     x
 }

tests/ui/fail/fn_poly_annot_nested.rs

@@ -1,13 +1,13 @@
 //@error-in-other-file: Unsat
 
-#[thrust::requires(true)]
-#[thrust::ensures(result == x)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result == x)]
 fn id<T>(x: T) -> T {
     x
 }
 
-#[thrust::requires(true)]
-#[thrust::ensures(result != x)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result != x)]
 fn apply_twice<T>(x: T) -> T {
     id(id(x))
 }

tests/ui/fail/fn_poly_annot_recursive.rs

@@ -1,8 +1,8 @@
 //@error-in-other-file: Unsat
 //@compile-flags: -C debug-assertions=off
 
-#[thrust::requires(n >= 0)]
-#[thrust::ensures(result == value)]
+#[thrust_macros::requires(n >= 0)]
+#[thrust_macros::ensures(result == value)]
 fn repeat<T>(n: i32, value: T) -> T {
     if n == 0 {
         value

tests/ui/fail/fn_poly_annot_ref.rs

@@ -1,7 +1,7 @@
 //@error-in-other-file: Unsat
 
-#[thrust::requires(true)]
-#[thrust::ensures(result != x)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result != x)]
 fn id_ref<T>(x: &T) -> &T {
     x
 }

tests/ui/fail/fn_poly_annot_stronger.rs

@@ -1,8 +1,8 @@
 //@error-in-other-file: Unsat
 //@compile-flags: -C debug-assertions=off
 
-#[thrust::requires(x > 0)]
-#[thrust::ensures((result == x) && (result > 0))]
+#[thrust_macros::requires(x > 0)]
+#[thrust_macros::ensures((result == x) && (result > 0))]
 fn pass_positive<T>(x: i32, _dummy: T) -> i32 {
     x
 }

tests/ui/fail/fn_ptr.rs

@@ -1,8 +1,8 @@
 //@error-in-other-file: Unsat
 //@compile-flags: -C debug-assertions=off
 
-#[thrust::requires(true)]
-#[thrust::ensures(true)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(true)]
 #[thrust::trusted]
 fn rand() -> i64 { unimplemented!() }
 

tests/ui/fail/just_rec.rs

@@ -2,13 +2,13 @@
 //@compile-flags: -C debug-assertions=off
 
 #[thrust::trusted]
-#[thrust::requires(true)]
-#[thrust::ensures(true)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(true)]
 fn rand() -> i32 { unimplemented!() }
 
 #[thrust::trusted]
-#[thrust::requires(true)]
-#[thrust::ensures(true)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(true)]
 fn rand_bool() -> bool { unimplemented!() }
 
 fn just_rec(ma: &mut i32) {

tests/ui/fail/loop.rs

@@ -1,8 +1,8 @@
 //@error-in-other-file: Unsat
 //@compile-flags: -C debug-assertions=off
 
-#[thrust::requires(true)]
-#[thrust::ensures(true)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(true)]
 #[thrust::trusted]
 fn rand() -> i64 { unimplemented!() }
 

tests/ui/fail/mut_recursive.rs

@@ -1,8 +1,8 @@
 //@error-in-other-file: Unsat
 //@compile-flags: -C debug-assertions=off
 
-#[thrust::requires(true)]
-#[thrust::ensures(true)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(true)]
 #[thrust::trusted]
 fn rand() -> i64 { unimplemented!() }
 

tests/ui/fail/recursive.rs

@@ -1,8 +1,8 @@
 //@error-in-other-file: Unsat
 //@compile-flags: -C debug-assertions=off
 
-#[thrust::requires(true)]
-#[thrust::ensures(true)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(true)]
 #[thrust::trusted]
 fn rand() -> i64 { unimplemented!() }
 

tests/ui/fail/split.rs

@@ -2,8 +2,8 @@
 //@compile-flags: -C debug-assertions=off
 
 #[thrust::trusted]
-#[thrust::requires(true)]
-#[thrust::ensures(true)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(true)]
 fn rand() -> i32 { unimplemented!() }
 
 fn split<'a>((a, b): &'a mut (i32, i32)) -> (&'a mut i32, &'a mut i32) {

tests/ui/fail/take_max.rs

@@ -1,8 +1,8 @@
 //@error-in-other-file: Unsat
 //@compile-flags: -C debug-assertions=off
 
-#[thrust::requires(true)]
-#[thrust::ensures(true)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(true)]
 #[thrust::trusted]
 fn rand() -> i64 { unimplemented!() }
 

tests/ui/fail/take_max_annot.rs

@@ -1,15 +1,15 @@
 //@error-in-other-file: Unsat
 //@compile-flags: -C debug-assertions=off
 
-#[thrust::requires(true)]
-#[thrust::ensures(true)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(true)]
 #[thrust::trusted]
 fn rand() -> i64 { unimplemented!() }
 
-#[thrust::requires(true)]
-#[thrust::ensures(
-    *ma >= *mb && *ma == ^ma && ma == result ||
-    *ma < *mb && *mb == ^mb && mb == result
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    *ma >= *mb && *ma == !ma && ma == result ||
+    *ma < *mb && *mb == !mb && mb == result
 )]
 fn take_max<'a>(ma: &'a mut i64, mb: &'a mut i64) -> &'a mut i64 {
   if *ma >= *mb {

tests/ui/pass/adt.rs

@@ -6,9 +6,13 @@ pub enum X {
     B(bool),
 }
 
+impl thrust_models::Model for X {
+    type Ty = Self;
+}
+
 #[thrust::trusted]
-#[thrust::requires(true)]
-#[thrust::ensures(true)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(true)]
 fn rand() -> X { unimplemented!() }
 
 fn inv(x: X) -> X {