Add proof annotation for smack harnesses (rust-lang#1939)

A bunch of the harnesses from the smack testsuite were missing kani::proof annotation. They have the kani-verify-fail tag on them, and because of rust-lang#1910, they would fail but with a different error than expected.

Add #[kani::proof] to them.

Author: celinval

tests/smack/basic/add.rs

@@ -3,6 +3,7 @@
 // @expect error
 // kani-verify-fail
 
+#[kani::proof]
 pub fn main() {
     let a = 2;
     let b = 3;

tests/smack/basic/arith_assume3.rs

@@ -3,6 +3,7 @@
 // @expect error
 // kani-verify-fail
 
+#[kani::proof]
 pub fn main() {
     let a = kani::any();
     let b = kani::any();

tests/smack/basic/div.rs

@@ -3,6 +3,7 @@
 // @expect error
 // kani-verify-fail
 
+#[kani::proof]
 pub fn main() {
     let a = 2;
     let b = 3;

tests/smack/basic/mod.rs

@@ -3,6 +3,7 @@
 // @expect error
 // kani-verify-fail
 
+#[kani::proof]
 pub fn main() {
     let a = 2;
     let b = 3;

tests/smack/basic/mul.rs

@@ -3,6 +3,7 @@
 // @expect error
 // kani-verify-fail
 
+#[kani::proof]
 pub fn main() {
     let a = 2;
     let b = 3;

tests/smack/basic/sub.rs

@@ -3,6 +3,7 @@
 // @expect error
 // kani-verify-fail
 
+#[kani::proof]
 pub fn main() {
     let a = 2;
     let b = 3;

tests/smack/functions/closure_fail.rs

@@ -11,6 +11,7 @@ where
     some_closure(1);
 }
 
+#[kani::proof]
 pub fn main() {
     let mut num: i32 = kani::any();
     if num <= std::i32::MAX - 10 {

tests/smack/functions/double_fail.rs

@@ -7,6 +7,7 @@ fn double(a: u32) -> u32 {
     a * 2
 }
 
+#[kani::proof]
 pub fn main() {
     let a = kani::any();
     if a <= std::u32::MAX / 2 {

tests/smack/generics/generic_function1.rs

@@ -34,6 +34,7 @@ fn swapem<T, U: S<T>>(s: U) -> U {
     s.swap_items()
 }
 
+#[kani::proof]
 pub fn main() {
     let x2 = kani::any();
     let y2 = kani::any();

tests/smack/generics/generic_function2.rs

@@ -34,6 +34,7 @@ fn swapem<T, U: S<T>>(s: U) -> U {
     s.swap_items()
 }
 
+#[kani::proof]
 pub fn main() {
     let x2 = kani::any();
     let y2 = kani::any();

tests/smack/generics/generic_function3.rs

@@ -34,6 +34,7 @@ fn swapem<T, U: S<T>>(s: U) -> U {
     s.swap_items()
 }
 
+#[kani::proof]
 pub fn main() {
     let x2 = kani::any();
     let y2 = kani::any();

tests/smack/generics/generic_function4.rs

@@ -34,6 +34,7 @@ fn swapem<T, U: S<T>>(s: U) -> U {
     s.swap_items()
 }
 
+#[kani::proof]
 pub fn main() {
     let x2 = kani::any();
     let y2 = kani::any();

tests/smack/generics/generic_function5.rs

@@ -34,6 +34,7 @@ fn swapem<T, U: S<T>>(s: U) -> U {
     s.swap_items()
 }
 
+#[kani::proof]
 pub fn main() {
     let x2 = kani::any();
     let y2 = kani::any();

tests/smack/overflow/add_overflow.rs

@@ -8,6 +8,7 @@ pub fn get128() -> u8 {
     128
 }
 
+#[kani::proof]
 pub fn main() {
     let a: u8 = get128();
     let b: u8 = get128();

tests/smack/overflow/mul_overflow.rs

@@ -8,6 +8,7 @@ fn get128() -> u8 {
     128
 }
 
+#[kani::proof]
 pub fn main() {
     let a: u8 = get128();
     let b: u8 = 2;

tests/smack/overflow/sub_overflow.rs

@@ -8,6 +8,7 @@ fn get128() -> u8 {
     128
 }
 
+#[kani::proof]
 pub fn main() {
     let a: u8 = get128();
     let b: u8 = 129;

tests/smack/recursion/fac_fail.rs

@@ -11,6 +11,7 @@ fn fac(n: u64, acc: u64) -> u64 {
     }
 }
 
+#[kani::proof]
 pub fn main() {
     let x = fac(5, 1);
     assert!(x != 120);

tests/smack/recursion/fib_fail.rs

@@ -12,6 +12,7 @@ fn fib(x: u64) -> u64 {
     }
 }
 
+#[kani::proof]
 pub fn main() {
     let x = fib(6);
     assert!(x != 8);

tests/smack/structures/option_fail.rs

@@ -7,6 +7,7 @@ fn safe_div(x: u32, y: u32) -> Option<u32> {
     if y != 0 { Some(x / y) } else { None }
 }
 
+#[kani::proof]
 pub fn main() {
     let x = kani::any();
     if x > 0 && x <= 100 {

tests/smack/structures/point_fail.rs

@@ -37,6 +37,7 @@ impl AddAssign for Point {
     }
 }
 
+#[kani::proof]
 pub fn main() {
     let w = kani::any();
     let x = kani::any();

tests/smack/vector/vec11.rs

@@ -4,6 +4,7 @@
 // @expect error
 // kani-verify-fail
 
+#[kani::proof]
 pub fn main() {
     let mut v: Vec<u64> = Vec::new();
     v.push(0);

tests/smack/vector/vec12.rs

@@ -4,6 +4,7 @@
 // @expect error
 // kani-verify-fail
 
+#[kani::proof]
 pub fn main() {
     let mut v: Vec<u64> = Vec::new();
     v.push(0);

tests/smack/vector/vec13.rs

@@ -4,6 +4,7 @@
 // @expect error
 // kani-verify-fail
 
+#[kani::proof]
 pub fn main() {
     let mut v: Vec<u64> = Vec::new();
     v.push(0);

tests/smack/vector/vec_resize_fail.rs

@@ -4,6 +4,7 @@
 // @expect error
 // kani-verify-fail
 
+#[kani::proof]
 pub fn main() {
     let mut v1: Vec<u64> = vec![0];
     let mut v2: Vec<u64> = vec![3];