Add section on "fixme" tests (rust-lang#731)

Author: adpaco-aws

rmc-docs/src/rmc-testing.md

@@ -61,6 +61,10 @@ In particular, the RMC testing suites are composed of:
    [Prusti](https://github.com/viperproject/prusti-dev) tool.
  * `smack`: Works like `rmc` but contains tests from the
    [SMACK](https://github.com/smackers/smack) tool.
+ * `rmc-fixme`: Similar to `rmc`, but runs ignored tests from the `rmc` testing
+                suite (i.e., tests with `fixme` or `ignore` in their name).
+                Allows us to detect when a previously not supported test becomes
+                supported. More details in ["Fixme" tests](#"fixme"-tests).
  * `expected`: Similar to `rmc` but with an additional check which ensures that
                lines appearing in `*.expected` files appear in the output
                generated by `rmc`.
@@ -135,6 +139,31 @@ Alternatively, CBMC flags can also be passed using `cbmc-flags`:
 For `cargo-rmc` tests, the preferred way to pass command-line options is adding
 them to `Cargo.toml` below the `[rmc.flags]` marker.
 
+### "Fixme" tests
+
+Any test containing `fixme` or `ignore` in its name is considered a test not
+supported for some reason. Generally, these tests are not run because they will
+either return a wrong result (since they are not supported) or take a long time
+to finish.
+
+However, "fixme" tests included in the `rmc` folder are run via the `rmc-fixme`
+testing suite. `rmc-fixme` works on test files from `rmc` but:
+ 1. Only runs tests whose name contains `fixme` or `ignore` (ignoring the rest).
+ 2. The expected outcome is failure. In other words, a test is successful if it
+    fails.
+
+We welcome contributions with "fixme" tests which demonstrate a bug or
+unsupported feature in RMC. Ideally, the test should include some comments
+regarding:
+ * The expected result of the test.
+ * The actual result of the test (e.g., interesting parts of the output).
+ * Links to related issues.
+
+To include a new "fixme" test in `rmc` you only need to ensure its name contains
+`fixme` or `ignore`. If your changes to RMC cause a "fixme" test to become
+supported, you only need to rename it so the name does not contain `fixme` nor
+`ignore`.
+
 ## Rust unit tests
 
 These tests follow the