Cleanup RMC Flags

[vecchiot-aws]

Description of changes:

This PR cleans up the flags in rmc and cargo-rmc by unifying them into a shared file, adding group organization, and descriptions for each flag.

Resolved issues:

Call-outs:

Testing:

• How is this change tested? Existing regression suite.

• Is this a refactor change? Yes.

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.

[nchong-at-aws]

Good clean-up. Some suggested/requested changes on naming.

[nchong-at-aws]

Maybe proof_harness_flags?

[nchong-at-aws]

Consider pointing to the cbmc-viewer docs for more info

[nchong-at-aws]

retcode -> return code

[nchong-at-aws]

Remove necessarily

[bdalrhm]

Appreciate the help messages 🙂

[bdalrhm]

Suggested change

	def add_flags(
	parser,
	exclude_flags=[],
	exclude_groups=[]):
	def add_flags(parser, exclude_flags=[], exclude_groups=[]):

Consider using a formatter (like autopep)

[bdalrhm]

Suggested change

	parser = argparse.ArgumentParser(description="Verify a Rust crate")
	parser = argparse.ArgumentParser(prog="cargo rmc", description="Verify a Rust crate")

cargo-rmc script is usually called as cargo rmc.

[avanhatt]

nit: can we fail here instead of warn? Warnings are easy to overlook

[avanhatt]

I know this isn't your change, but should this give a more helpful message?

[vecchiot-aws]

The error is printed by dependencies_in_path, so we don't need to print anything here.

[avanhatt]

Should this specify in the last position?

[vecchiot-aws]

It doesn't have to be in the last position; actually putting it first can avoid issues with flags that take multiple arguments. The only thing that really matters is --cbmc-args last, or else some RMC flags might be interpretted as CBMC flags.

[vecchiot-aws]

Raise an error instead; "Error setting up command line parser..." + link to issue page for users to report bug.

[danielsn]

Why do we exclude these flags? Add a comment explaining why.

[danielsn]

alphabatize

[danielsn]

sort