Add ignored test and TODO for (smt) equality of floating point

Author: utaal

verify/rust_verify/tests/common/mod.rs

@@ -97,8 +97,8 @@ pub fn verify_with_pervasive(
 
 #[macro_export]
 macro_rules! test_verify_with_pervasive {
-    (#[test] $name:ident $body:expr => $result:pat => $assertions:expr ) => {
-        #[test]
+    ($(#[$attrs:meta])* $name:ident $body:expr => $result:pat => $assertions:expr ) => {
+        $(#[$attrs])*
         fn $name() {
             let result = verify_with_pervasive($body);
             if let $result = result {
@@ -108,8 +108,8 @@ macro_rules! test_verify_with_pervasive {
             }
         }
     };
-    (#[test] $name:ident $body:expr => $result:pat) => {
-        #[test]
+    ($(#[$attrs:meta])* $name:ident $body:expr => $result:pat) => {
+        $(#[$attrs])*
         fn $name() {
             let result = verify_with_pervasive($body);
             if let $result = result {

verify/rust_verify/tests/partial_eq.rs

@@ -0,0 +1,13 @@
+#![feature(rustc_private)]
+#[macro_use]
+mod common;
+use common::*;
+
+test_verify_with_pervasive! {
+    // TODO: SOUNDNESS; when the `f64::NAN` expression is supported, this may be unsound
+    #[test] #[ignore] test_float_nan code! {
+        fn float_nan() {
+            assert(f64::NAN != f64::NAN);
+        }
+    } => Ok(())
+}