Replace annotations in some test cases with thrust_macros

Author: coord-e

tests/ui/fail/annot_enum_simple.rs

@@ -5,8 +5,12 @@ pub enum X {
     B(bool),
 }
 
-#[thrust::requires(x == X::A(1))]
-#[thrust::ensures(true)]
+impl thrust_models::Model for X {
+    type Ty = X;
+}
+
+#[thrust_macros::requires(x == X::A(1))]
+#[thrust_macros::ensures(true)]
 fn test(x: X) {
     if let X::A(i) = x {
         assert!(i == 2);

tests/ui/fail/annot_exists.rs

@@ -2,12 +2,14 @@
 //@compile-flags: -C debug-assertions=off
 //@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
 
+use thrust_models::exists;
+
 #[thrust::trusted]
 #[thrust::callable]
 fn rand() -> i32 { unimplemented!() }
 
-#[thrust::requires(true)]
-#[thrust::ensures(exists x:int. result == 2 * x)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(exists(|x: i32| result == 2 * x))]
 fn f() -> i32 {
     let x = rand();
     x + x + x

tests/ui/fail/annot_mut_term.rs

@@ -1,7 +1,9 @@
 //@error-in-other-file: Unsat
 
-#[thrust::requires(true)]
-#[thrust::ensures(x == <*x, y>)]
+use thrust_models::model::Mut;
+
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(x == Mut::new(*x, y))]
 fn f(x: &mut i64, y: i64) {
     *x = y;
 }

tests/ui/fail/tuple_annot.rs

@@ -1,8 +1,8 @@
 //@error-in-other-file: Unsat
 //@compile-flags: -C debug-assertions=off
 
-#[thrust::requires(true)]
-#[thrust::ensures(^x == ((*x).1, (*x).1))]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(!x == ((*x).1, (*x).1))]
 fn swap_tuple(x: &mut (i32, i32)) {
     let v = *x;
     *x = (v.1, v.0);

tests/ui/pass/annot_enum_simple.rs

@@ -5,8 +5,12 @@ pub enum X {
     B(bool),
 }
 
-#[thrust::requires(x == X::A(1))]
-#[thrust::ensures(true)]
+impl thrust_models::Model for X {
+    type Ty = X;
+}
+
+#[thrust_macros::requires(x == X::A(1))]
+#[thrust_macros::ensures(true)]
 fn test(x: X) {
     if let X::A(i) = x {
         assert!(i == 1);

tests/ui/pass/annot_exists.rs

@@ -2,12 +2,14 @@
 //@compile-flags: -C debug-assertions=off
 //@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
 
+use thrust_models::exists;
+
 #[thrust::trusted]
 #[thrust::callable]
 fn rand() -> i32 { unimplemented!() }
 
-#[thrust::requires(true)]
-#[thrust::ensures(exists x:int. result == 2 * x)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(exists(|x: i32| result == 2 * x))]
 fn f() -> i32 {
     let x = rand();
     x + x

tests/ui/pass/annot_mut_term.rs

@@ -1,7 +1,9 @@
 //@check-pass
 
-#[thrust::requires(true)]
-#[thrust::ensures(x == <*x, y>)]
+use thrust_models::model::Mut;
+
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(x == Mut::new(*x, y))]
 fn f(x: &mut i64, y: i64) {
     *x = y;
 }

tests/ui/pass/take_max_annot.rs

@@ -1,9 +1,8 @@
 //@check-pass
 //@compile-flags: -C debug-assertions=off
 
-#[thrust::requires(true)]
-#[thrust::ensures(true)]
 #[thrust::trusted]
+#[thrust::callable]
 fn rand() -> i64 { unimplemented!() }
 
 #[thrust::requires(true)]

tests/ui/pass/tuple_annot.rs

@@ -1,8 +1,8 @@
 //@check-pass
 //@compile-flags: -C debug-assertions=off
 
-#[thrust::requires(true)]
-#[thrust::ensures(^x == ((*x).1, (*x).0))]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(^x == ((*x).1, (*x).0))]
 fn swap_tuple(x: &mut (i32, i32)) {
     let v = *x;
     *x = (v.1, v.0);