Add many more test cases

(thanks Claude)

Author: coord-e

tests/ui/fail/fn_poly_annot_complex.rs

@@ -0,0 +1,12 @@
+//@error-in-other-file: Unsat
+
+#[thrust::requires((x.0 > 0) && (x.1 > 0))]
+#[thrust::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)
+}
+
+fn main() {
+    let result = swap_positive((-5, 10, true, 42));
+    assert!(result.0 == 10);
+}

tests/ui/fail/fn_poly_annot_multi_inst.rs

@@ -0,0 +1,15 @@
+//@error-in-other-file: Unsat
+
+#[thrust::requires(true)]
+#[thrust::ensures(result == x)]
+fn id<T>(x: T) -> T {
+    x
+}
+
+fn main() {
+    let a = id(42);
+    assert!(a == 42);
+    
+    let b = id(true);
+    assert!(b == false);
+}

tests/ui/fail/fn_poly_annot_nested.rs

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

tests/ui/fail/fn_poly_annot_recursive.rs

@@ -0,0 +1,17 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+#[thrust::requires(n >= 0)]
+#[thrust::ensures(result == value)]
+fn repeat<T>(n: i32, value: T) -> T {
+    if n == 0 {
+        value
+    } else {
+        repeat(n - 1, value)
+    }
+}
+
+fn main() {
+    let result = repeat(-1, 42);
+    assert!(result == 42);
+}

tests/ui/fail/fn_poly_annot_ref.rs

@@ -0,0 +1,13 @@
+//@error-in-other-file: Unsat
+
+#[thrust::requires(true)]
+#[thrust::ensures(result != x)]
+fn id_ref<T>(x: &T) -> &T {
+    x
+}
+
+fn main() {
+    let val = 42;
+    let r = id_ref(&val);
+    assert!(*r == 42);
+}

tests/ui/fail/fn_poly_annot_stronger.rs

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

tests/ui/fail/fn_poly_double_nested.rs

@@ -0,0 +1,21 @@
+//@error-in-other-file: Unsat
+
+fn id<T>(x: T) -> T {
+    x
+}
+
+fn apply_twice<T>(x: T) -> T {
+    id(id(x))
+}
+
+fn apply_thrice<T>(x: T) -> T {
+    apply_twice(id(x))
+}
+
+fn apply_four<T>(x: T) -> T {
+    apply_twice(apply_twice(x))
+}
+
+fn main() {
+    assert!(apply_four(42) == 43);
+}

tests/ui/fail/fn_poly_multiple_calls.rs

@@ -0,0 +1,13 @@
+//@error-in-other-file: Unsat
+
+fn first<T, U>(pair: (T, U)) -> T {
+    pair.0
+}
+
+fn main() {
+    let x = first((42, true));
+    let y = first((true, 100));
+    
+    assert!(x == 42);
+    assert!(y == false);
+}

tests/ui/fail/fn_poly_mut_ref.rs

@@ -0,0 +1,16 @@
+//@error-in-other-file: Unsat
+
+fn update<T>(x: &mut T, new_val: T) {
+    *x = new_val;
+}
+
+fn chain_update<T>(x: &mut T, temp: T, final_val: T) {
+    update(x, temp);
+    update(x, final_val);
+}
+
+fn main() {
+    let mut val = 42;
+    chain_update(&mut val, 100, 200);
+    assert!(val == 42);
+}

tests/ui/fail/fn_poly_nested_calls.rs

@@ -0,0 +1,17 @@
+//@error-in-other-file: Unsat
+
+fn id<T>(x: T) -> T {
+    x
+}
+
+fn apply_twice<T>(x: T) -> T {
+    id(id(x))
+}
+
+fn apply_thrice<T>(x: T) -> T {
+    id(apply_twice(x))
+}
+
+fn main() {
+    assert!(apply_thrice(42) == 43);
+}