Move cargo tests to compiletest.

[bdalrhm]

Description of changes:

This PR moves cargo tests to compiletest. expected.* files are renamed to *.expected to make use of available convenience functions. Note that a --target-dir option is added to change the default target directories for cargo builds to build/<arch>/test/cargo/<proj-name>/<function-name>/target and avoid race problems while running cargo tests concurrently. For consistency, other generated files are also moved into the specified target directory.

Resolved issues:

Resolves #177

Call-outs:

Testing:

• How is this change tested?
  • Cargo tests still pass after the changes
• Is this a refactor change?
  • To some degree, cargo-rmc-tests is moved and renamed to src/test/cargo

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[adpaco-aws]

This looks great! Could we use CargoRMC and cargo-rmc for the enum variant and its associated string?

[vecchiot-aws]

I don't know how to comment on a non-changed file, but should we be adding this argument to scripts/rmc as well?

[bdalrhm]

I thought about that, but I could not come to a conclusion. Normally, when someone runs cargo, they expect all artifacts (besides Cargo.lock) to be in the target directory. rustc has a somewhat similar option --out-dir for specifying the directory of the compiled file. However, it's not really treated as a build directory and I don't know if we should treat it as such. So, I think this is a decision for the team to make.

[adpaco-aws]

In addition to @bdalrhm explanation, I would like to point out that RMC's workflow is more similar to CBMC's: It does generate a verification output, not a compiled program. So it makes sense for us to have this --target-dir flag for cargo-rmc but not for rmc itself.