crux-mir: Use simpler #[crux::test] attribute for symbolic tests

There's not much of a point in checking for the `crux` configuration attribute,
since one wouldn't be able to compile these tests with bare `rustc` anyway due
to their use of the `crucible` crate.

crux-mir/test/concurrency/atomic/atomic.rs

@@ -4,7 +4,7 @@ use std::thread;
 use std::sync::{Arc,atomic};
 
 #[cfg(not(with_main))]
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test_nofail() {
     let N       = 3;
 

crux-mir/test/concurrency/atomic/atomic_fetch.rs

@@ -4,7 +4,7 @@ use std::thread;
 use std::sync::{Arc,atomic};
 
 #[cfg(not(with_main))]
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test_nofail() {
     let N       = 3;
 

crux-mir/test/concurrency/mutex/mutex.rs

@@ -4,7 +4,7 @@ use std::thread;
 use std::sync::{Arc,Mutex};
 
 #[cfg(not(with_main))]
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test_nofail() {
     let data    = Arc::new(Mutex::new(0 as u32));
     let N       = 3;
@@ -37,7 +37,7 @@ fn crux_test_nofail() {
     data.crucible_TEMP_unlock();
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test_fail() {
     let data    = Arc::new(Mutex::new(0 as u32));
     let N       = 2;

crux-mir/test/concurrency/mutex/mutex_atomic.rs

@@ -6,7 +6,7 @@ use std::sync::atomic::AtomicU16;
 use std::sync::atomic::Ordering::SeqCst;
 
 #[cfg(not(with_main))]
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test_nofail() {
     let data    = Arc::new(Mutex::new(()));
     let ctr     = Arc::new(AtomicU16::new(0));

crux-mir/test/concurrency/mutex/thread_retval.rs

@@ -4,7 +4,7 @@ use std::thread;
 use std::sync::{Arc,Mutex};
 
 #[cfg(not(with_main))]
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test() {
     let N       = 2;
     let V       = 3;

crux-mir/test/concurrency/mutex/thread_retval_mutex.rs

@@ -4,7 +4,7 @@ use std::thread;
 use std::sync::{Arc,Mutex};
 
 #[cfg(not(with_main))]
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test() {
     let data    = Arc::new(Mutex::new(0 as u32));
     let N       = 3;

crux-mir/test/concurrency/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.rs

@@ -37,7 +37,7 @@ fn find_entries(tid:usize,
     count.crucible_TEMP_unlock();
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn pthread_finding_k_matches()
 {
     let mut vals = vec![];

crux-mir/test/concurrency/sv-benchmarks/c/pthread/bigshot.rs

@@ -5,7 +5,7 @@ use std::thread;
 use std::sync::{Arc,Mutex};
 
 #[cfg(not(with_main))]
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn bigshot_p() {
     let v = Arc::new(Mutex::new(None));
 
@@ -35,7 +35,7 @@ fn bigshot_p() {
 }
 
 #[cfg(not(with_main))]
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn bigshot_s() {
     let v = Arc::new(Mutex::new(None));
 
@@ -65,7 +65,7 @@ fn bigshot_s() {
 }
 
 #[cfg(not(with_main))]
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn bigshot_s2() {
     let v = Arc::new(Mutex::new(None));
 

crux-mir/test/concurrency/sv-benchmarks/c/pthread/fib_bench.rs

@@ -35,7 +35,7 @@ fn calc_fib() -> i32 {
     j
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test_fail() {
     let data    = Arc::new(Mutex::new((1 as i32, 1 as i32)));
 
@@ -59,7 +59,7 @@ fn crux_test_fail() {
     data.crucible_TEMP_unlock();
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test() {
     let data = Arc::new(Mutex::new((1 as i32, 1 as i32)));
 

crux-mir/test/concurrency/sv-benchmarks/c/pthread/indexer.rs

@@ -24,7 +24,7 @@ fn cas(tab:&Arc<Vec<Mutex<i32>>>, h:usize, val:i32, new_val:i32) -> i32
 }
 
 #[cfg(not(with_main))]
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn indexer() {
     let mut tab = vec![];
     let mut ts  = vec![];

crux-mir/test/concurrency/sv-benchmarks/c/pthread/queue.rs

@@ -125,7 +125,7 @@ fn t2_bad(m : Arc<Mutex<Queue>>) {
     }
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test_fails() {
     let mut q = Queue::new();
     q.enqueue_flag = true;
@@ -149,7 +149,7 @@ fn crux_test_fails() {
     h2.join();
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test_succeeds() {
     let mut q = Queue::new();
     q.enqueue_flag = true;

crux-mir/test/concurrency/sv-benchmarks/c/pthread/reorder.rs

@@ -39,12 +39,12 @@ fn run_test(numSet: usize, numCheck: usize) {
     }
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn reorder2() {
     run_test(2,2);
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn reorder5() {
     run_test(4,1);
 }

crux-mir/test/concurrency/sv-benchmarks/c/pthread/singleton.rs

@@ -46,7 +46,7 @@ fn thread0(v: Arc<Mutex<Option<i32>>>) {
     }
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn singleton() {
     let v = Arc::new(Mutex::new(None));
     let vv = v.clone();

crux-mir/test/concurrency/sv-benchmarks/c/pthread/stack.rs

@@ -85,7 +85,7 @@ fn t2(stack: Arc<Mutex<Stack>>, with_flag: bool)
     }
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn stack_1()
 {
     let stk = Arc::new(Mutex::new(Stack::new()));
@@ -100,7 +100,7 @@ fn stack_1()
     h2.join();
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn stack_2()
 {
     let stk = Arc::new(Mutex::new(Stack::new()));

crux-mir/test/concurrency/sv-benchmarks/c/pthread/stateful.rs

@@ -45,14 +45,14 @@ fn run_threads() -> (i32, i32)
     return r
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn stateful01_1()
 {
     let (d1, d2) = run_threads();
     crucible_assert!( !(d1 == 16 && d2 == 5) );
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn stateful01_2()
 {
     let (d1, d2) = run_threads();

crux-mir/test/concurrency/sv-benchmarks/c/pthread/triangular.rs

@@ -31,7 +31,7 @@ fn t2(i:Arc<AtomicI32>, j:Arc<AtomicI32>, m:Arc<Mutex<()>>)
     }
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn triangular_1()
 {
     let i = Arc::new(AtomicI32::new(3));
@@ -58,7 +58,7 @@ fn triangular_1()
     crucible_assert!(! (condI || condJ) );
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn triangular_2()
 {
     let i = Arc::new(AtomicI32::new(3));

crux-mir/test/concurrency/sv-benchmarks/c/pthread/triangular_static.rs

@@ -34,7 +34,7 @@ fn t2(m:Arc<Mutex<()>>)
     }
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn triangular_1()
 {
     let m = Arc::new(Mutex::new(()));
@@ -54,7 +54,7 @@ fn triangular_1()
     crucible_assert!(! (condI || condJ) );
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn triangular_2()
 {
     let m = Arc::new(Mutex::new(()));

crux-mir/test/concurrency/sv-benchmarks/c/pthread/twostage.rs

@@ -59,7 +59,7 @@ fn twostage_test(t_threads: usize, r_threads: usize) {
     }
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn twostage_3() {
     twostage_test(2,1);
 }

crux-mir/test/coverage/coverage.rs

@@ -1,7 +1,7 @@
 extern crate crucible;
 use crucible::*;
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test() -> i32 {
     let x = u8::symbolic("x");
     crucible_assume!(x < 2);

crux-mir/test/coverage/coverage_cond.rs

@@ -10,7 +10,7 @@ fn g(cond: bool) -> u8 {
     if !cond { 10 } else { 20 }
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test() -> u8 {
     f(true) + g(true)
 }

crux-mir/test/coverage/coverage_dual.rs

@@ -6,12 +6,12 @@ fn f(c: bool, t: i32, e: i32) -> i32 {
     if c { t } else { e }
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test1() -> i32 {
     f(false, 1, 2)
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test2() -> i32 {
     f(true, 10, 20)
 }

crux-mir/test/coverage/coverage_loop.rs

@@ -1,7 +1,7 @@
 extern crate crucible;
 use crucible::*;
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test() -> i32 {
     let mut y = 1;
     for i in 0..10 {

crux-mir/test/coverage/coverage_macro.rs

@@ -19,7 +19,7 @@ fn f() -> Option<u8> {
     Some(1)
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test() -> u8 {
     f().unwrap_or(0)
 }

crux-mir/test/coverage/coverage_match.rs

@@ -7,7 +7,7 @@ enum E {
     C = 30,
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test() -> i32 {
     let x = u8::symbolic("x");
     crucible_assume!(x != 1);

crux-mir/test/coverage/coverage_mono.rs

@@ -6,7 +6,7 @@ fn f<T>(c: bool, t: T, e: T) -> T {
     if c { t } else { e }
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test() -> i32 {
     f::<u8>(false, 1_u8, 2_u8) as i32 + f::<i32>(true, 10, 20)
 }

crux-mir/test/coverage/coverage_shortcircuit.rs

@@ -1,7 +1,7 @@
 extern crate crucible;
 use crucible::*;
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test() -> i32 {
     let x = u8::symbolic("x");
     crucible_assume!(x < 1);

crux-mir/test/coverage/coverage_try.rs

@@ -11,7 +11,7 @@ fn f() -> Option<u8> {
     x.checked_add(y)
 }
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test() -> u8 {
     f().unwrap_or(0)
 }

crux-mir/test/symb_eval/alloc/out_of_bounds.rs

@@ -2,7 +2,7 @@ extern crate crucible;
 use crucible::*;
 use crucible::alloc::allocate;
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test() -> i32 {
     unsafe {
         let ptr = allocate::<i32>(10);

crux-mir/test/symb_eval/alloc/uninit_read.rs

@@ -2,7 +2,7 @@ extern crate crucible;
 use crucible::*;
 use crucible::alloc::allocate;
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test() -> i32 {
     unsafe {
         let ptr = allocate::<i32>(10);

crux-mir/test/symb_eval/alloc/valid_read.rs

@@ -2,7 +2,7 @@ extern crate crucible;
 use crucible::*;
 use crucible::alloc::allocate;
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test() -> i32 {
     unsafe {
         let ptr = allocate::<i32>(10);

crux-mir/test/symb_eval/alloc/zero_length.rs

@@ -2,7 +2,7 @@ extern crate crucible;
 use crucible::*;
 use crucible::alloc::allocate;
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test() {
     unsafe {
         // Make sure the CustomOp succeeds in creating a pointer to the first element of an empty

crux-mir/test/symb_eval/any/conditional.rs

@@ -7,7 +7,7 @@ extern crate crucible;
 use crucible::*;
 use crucible::any::Any;
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test() {
     let mut x = bool::symbolic("x");
     if x {

crux-mir/test/symb_eval/any/downcast.rs

@@ -3,7 +3,7 @@
 extern crate crucible;
 use crucible::any::Any;
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test() -> i32 {
     let x: i32 = 1;
     let a = Any::new(x);

crux-mir/test/symb_eval/any/downcast_fail.rs

@@ -3,7 +3,7 @@
 extern crate crucible;
 use crucible::any::Any;
 
-#[cfg_attr(crux, crux::test)]
+#[crux::test]
 fn crux_test() -> i32 {
     let x: () = ();
     let a = Any::new(x);