From f282d80bfea94cfb3a0c918166360a4c02627600 Mon Sep 17 00:00:00 2001
From: Thomas Del Vecchio <vecchiot@amazon.com>
Date: Thu, 15 Jul 2021 17:00:32 -0400
Subject: [PATCH 01/14] Initial draft.

---
 scripts/cargo-rmc    | 35 +++++++-----------
 scripts/rmc          | 30 ++++-----------
 scripts/rmc_flags.py | 88 ++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 108 insertions(+), 45 deletions(-)
 create mode 100644 scripts/rmc_flags.py

diff --git a/scripts/cargo-rmc b/scripts/cargo-rmc
index 5ac6d9de75d9..cb43e58706ad 100755
--- a/scripts/cargo-rmc
+++ b/scripts/cargo-rmc
@@ -6,6 +6,7 @@ import argparse
 import glob
 import sys
 import rmc
+import rmc_flags
 import os
 import pathlib
 
@@ -20,28 +21,12 @@ def main():
         del sys.argv[1]
 
     parser = argparse.ArgumentParser(description="Verify a Rust crate")
-    parser.add_argument("crate", help="crate to verify", nargs="?")
-    parser.add_argument("--crate", help="crate to verify", dest="crate_flag")
-    parser.add_argument("--verbose", "-v", action="store_true")
-    parser.add_argument("--quiet", "-q", action="store_true")
-    parser.add_argument("--debug", action="store_true")
-    parser.add_argument("--keep-temps", action="store_true")
-    parser.add_argument("--gen-c", action="store_true")
-    parser.add_argument("--mangler", default="v0")
-    parser.add_argument("--visualize", action="store_true")
-    parser.add_argument("--c-lib", nargs="*", default=[], action="extend")
-    parser.add_argument("--srcdir", default=".")
-    parser.add_argument("--target-dir", default="target",
-                        help="Directory for all generated artifacts")
-    parser.add_argument("--wkdir", default=".")
-    parser.add_argument("--function", default="main")
-    parser.add_argument("--no-default-checks", action="store_true", help="Disable all default checks")
-    parser.add_argument("--no-memory-safety-checks", action="store_true", help="Disable default memory safety checks")
-    parser.add_argument("--no-overflow-checks", action="store_true", help="Disable default overflow checks")
-    parser.add_argument("--no-unwinding-checks", action="store_true", help="Disable default unwinding checks")
-    parser.add_argument("--dry-run", action="store_true", help="Print commands instead of running them")
-    parser.add_argument("--cbmc-args", nargs=argparse.REMAINDER,
-                        default=[], help="Pass through directly to CBMC")
+
+    crate_group = parser.add_argument_group("Crate", "You can pass in the rust crate positionally or with the --crate flag.")
+    crate_group.add_argument("crate", help="crate to verify", nargs="?")
+    crate_group.add_argument("--crate", help="crate to verify", dest="crate_flag", metavar="CRATE")
+
+    rmc_flags.add_flags(parser)
     args = parser.parse_args()
 
     if args.crate:
@@ -56,6 +41,12 @@ def main():
     if not rmc.dependencies_in_path():
         return 1
 
+    if args.gen_symbols:
+        print("WARNING: --gen-symbols is not supported for cargo-rmc.")
+
+    if args.allow_cbmc_verification_failure:
+        print("WARNING: --allow-cbmc-verification-failure is not supported for cargo-rmc.")
+
     # Add some CBMC flags by default unless `--no-default-checks` is being used
     if not args.no_default_checks:
         rmc.add_selected_default_cbmc_flags(args)
diff --git a/scripts/rmc b/scripts/rmc
index dd9f9d83981f..1873edb9b2c7 100755
--- a/scripts/rmc
+++ b/scripts/rmc
@@ -6,6 +6,7 @@ import argparse
 import os
 import sys
 import rmc
+import rmc_flags
 import pathlib
 
 MY_PATH = pathlib.Path(__file__).parent.parent.absolute()
@@ -16,29 +17,12 @@ CBMC_VERIFICATION_FAILURE_EXIT_CODE = 10
 
 def main():
     parser = argparse.ArgumentParser(description="Verify a single Rust file")
-    parser.add_argument("input", help="Rust file to verify", nargs="?")
-    parser.add_argument("--input", help="Rust file to verify", dest="input_flag")
-    parser.add_argument("--verbose", "-v", action="store_true")
-    parser.add_argument("--quiet", "-q", action="store_true")
-    parser.add_argument("--debug", action="store_true")
-    parser.add_argument("--keep-temps", action="store_true")
-    parser.add_argument("--gen-c", action="store_true")
-    parser.add_argument("--gen-symbols", action="store_true")
-    parser.add_argument("--allow-cbmc-verification-failure", action="store_true")
-    parser.add_argument("--mangler", default="v0")
-    parser.add_argument("--visualize", action="store_true")
-    parser.add_argument("--c-lib", nargs="*", default=[], action="extend")
-    parser.add_argument("--srcdir", default=".")
-    parser.add_argument("--target-dir", default=".",
-                        help="Directory for all generated artifacts")
-    parser.add_argument("--wkdir", default=".")
-    parser.add_argument("--no-default-checks", action="store_true", help="Disable all default checks")
-    parser.add_argument("--no-memory-safety-checks", action="store_true", help="Disable default memory safety checks")
-    parser.add_argument("--no-overflow-checks", action="store_true", help="Disable default overflow checks")
-    parser.add_argument("--no-unwinding-checks", action="store_true", help="Disable default unwinding checks")
-    parser.add_argument("--dry-run", action="store_true", help="Print commands instead of running them")
-    parser.add_argument("--cbmc-args", nargs=argparse.REMAINDER,
-                        default=[], help="Pass through directly to CBMC")
+
+    input_group = parser.add_argument_group("Input", "You can pass in the rust file positionally or with the --input flag.")
+    input_group.add_argument("input", help="Rust file to verify", nargs="?")
+    input_group.add_argument("--input", help="Rust file to verify", dest="input_flag", metavar="INPUT")
+
+    rmc_flags.add_flags(parser, exclude_flags=["--function"])
     args = parser.parse_args()
 
     # In the future we hope to make this configurable in the command line.
diff --git a/scripts/rmc_flags.py b/scripts/rmc_flags.py
new file mode 100644
index 000000000000..09eb2a05924d
--- /dev/null
+++ b/scripts/rmc_flags.py
@@ -0,0 +1,88 @@
+import argparse
+
+def add_loudness_flags(make_group, add_flag):
+    group = make_group("Loudness flags", "Determine how much textual output to produce.")
+    add_flag(group, "--verbose", "-v", action="store_true")
+    add_flag(group, "--quiet", "-q", action="store_true")
+    add_flag(group, "--debug", action="store_true")
+
+def add_um_flags(make_group, add_flag):
+    group = make_group("Um flags", "Um")
+    add_flag(group, "--c-lib", nargs="*", default=[], action="extend")
+    add_flag(group, "--function", default="main")
+
+def add_artifact_flags(make_group, add_flag):
+    group = make_group("Artifact flags", "Produce artifacts in addition to a basic RMC report.")
+    add_flag(group, "--target-dir", default=".",
+                       help="Directory for all generated artifacts")
+    add_flag(group, "--keep-temps", action="store_true")
+    add_flag(group, "--gen-c", action="store_true")
+    add_flag(group, "--gen-symbols", action="store_true")
+
+def add_check_flags(make_group, add_flag):
+    group = make_group("Check flags", "Disable some or all default checks.")
+    add_flag(group, "--no-default-checks", action="store_true", help="Disable all default checks")
+    add_flag(group, "--no-memory-safety-checks", action="store_true", help="Disable default memory safety checks")
+    add_flag(group, "--no-overflow-checks", action="store_true", help="Disable default overflow checks")
+    add_flag(group, "--no-unwinding-checks", action="store_true", help="Disable default unwinding checks")
+
+def add_visualizer_flags(make_group, add_flag):
+    group = make_group("Visualizer flags", "Generate an HTML-based UI for the generated RMC report.")
+    add_flag(group, "--srcdir", default=".")
+    add_flag(group, "--wkdir", default=".")
+    add_flag(group, "--visualize", action="store_true")
+
+def add_other_flags(make_group, add_flag):
+    group = make_group("Other flags")
+    add_flag(group, "--allow-cbmc-verification-failure", action="store_true")
+    add_flag(group, "--mangler", default="v0")
+    add_flag(group, "--dry-run", action="store_true", help="Print commands instead of running them")
+
+def add_developer_flags(make_group, add_flag):
+    group = make_group("Developer flags", "These are generally meant for use by RMC developers, and are not necessarily stable.")
+    add_flag(group, "--cbmc-args", nargs=argparse.REMAINDER,
+                        default=[], help="Pass through directly to CBMC")
+
+def add_flags(
+    parser, 
+    exclude_flags=[],
+    exclude_groups=[]):
+
+    excluded_flags = set()
+    excluded_groups = set()
+    
+    def make_group(title=None, description=None):
+        return parser.add_argument_group(title, description)
+
+    def add_flag(group, flag, *args, **kwargs):
+        if group.title in exclude_groups:
+            excluded_groups.add(group.title)
+            return
+
+        if flag in exclude_flags:
+            excluded_flags.add(flag)
+            return
+        
+        group.add_argument(flag, *args, **kwargs)
+
+    add_groups = [
+        add_loudness_flags,
+        add_um_flags,
+        add_artifact_flags,
+        add_check_flags,
+        add_visualizer_flags,
+        add_other_flags,
+        add_developer_flags
+    ]
+
+    for add_group in add_groups:
+        add_group(make_group, add_flag)
+
+    extra_groups = set(exclude_groups) - excluded_groups
+    if extra_groups:
+        print(f"WARNING: Attempt to exclude groups which don't exist: {extra_groups}")
+
+    extra_flags = set(exclude_flags) - excluded_flags
+    if extra_flags:
+        print(f"WARNING: Attempt to exclude flags which don't exist: {extra_flags}")
+

From 922a3150ebba0101fe702922f1d42867565d9762 Mon Sep 17 00:00:00 2001
From: Thomas Del Vecchio <vecchiot@amazon.com>
Date: Thu, 15 Jul 2021 17:16:55 -0400
Subject: [PATCH 02/14] Add help strings to flags.

---
 scripts/rmc_flags.py | 48 +++++++++++++++++++++++++++-----------------
 1 file changed, 30 insertions(+), 18 deletions(-)

diff --git a/scripts/rmc_flags.py b/scripts/rmc_flags.py
index 09eb2a05924d..df78219cfd30 100644
--- a/scripts/rmc_flags.py
+++ b/scripts/rmc_flags.py
@@ -2,22 +2,30 @@
 
 def add_loudness_flags(make_group, add_flag):
     group = make_group("Loudness flags", "Determine how much textual output to produce.")
-    add_flag(group, "--verbose", "-v", action="store_true")
-    add_flag(group, "--quiet", "-q", action="store_true")
-    add_flag(group, "--debug", action="store_true")
+    add_flag(group, "--debug", action="store_true", 
+        help="Produce full debug information")
+    add_flag(group, "--verbose", "-v", action="store_true",
+        help="Output processing stages and commands, along with minor debug information")
+    add_flag(group, "--quiet", "-q", action="store_true",
+        help="Produces no output, just an exit code and requested artifacts. Overrides --verbose")
 
 def add_um_flags(make_group, add_flag):
-    group = make_group("Um flags", "Um")
-    add_flag(group, "--c-lib", nargs="*", default=[], action="extend")
-    add_flag(group, "--function", default="main")
+    group = make_group("Um flags", "Um") # TODO: Come up with name and description
+    add_flag(group, "--c-lib", nargs="*", default=[], action="extend",
+        help="External C files referenced by Rust code")
+    add_flag(group, "--function", default="main",
+        help="Entry point for verification")
 
 def add_artifact_flags(make_group, add_flag):
     group = make_group("Artifact flags", "Produce artifacts in addition to a basic RMC report.")
     add_flag(group, "--target-dir", default=".",
-                       help="Directory for all generated artifacts")
-    add_flag(group, "--keep-temps", action="store_true")
-    add_flag(group, "--gen-c", action="store_true")
-    add_flag(group, "--gen-symbols", action="store_true")
+        help="Directory for all generated artifacts")
+    add_flag(group, "--keep-temps", action="store_true",
+        help="Keep temporary files generated throughout RMC process")
+    add_flag(group, "--gen-c", action="store_true",
+        help="Generate C file equivalent to inputted program")
+    add_flag(group, "--gen-symbols", action="store_true",
+        help="Generate a symbol table")
 
 def add_check_flags(make_group, add_flag):
     group = make_group("Check flags", "Disable some or all default checks.")
@@ -28,20 +36,24 @@ def add_check_flags(make_group, add_flag):
 
 def add_visualizer_flags(make_group, add_flag):
     group = make_group("Visualizer flags", "Generate an HTML-based UI for the generated RMC report.")
-    add_flag(group, "--srcdir", default=".")
-    add_flag(group, "--wkdir", default=".")
-    add_flag(group, "--visualize", action="store_true")
+    add_flag(group, "--srcdir", default=".") # TODO: help?
+    add_flag(group, "--wkdir", default=".") # TODO: help?
+    add_flag(group, "--visualize", action="store_true",
+        help="Generate visualizer report; open report/html/index.html")
 
 def add_other_flags(make_group, add_flag):
     group = make_group("Other flags")
-    add_flag(group, "--allow-cbmc-verification-failure", action="store_true")
-    add_flag(group, "--mangler", default="v0")
-    add_flag(group, "--dry-run", action="store_true", help="Print commands instead of running them")
+    add_flag(group, "--allow-cbmc-verification-failure", action="store_true",
+        help="Do not produce error retcode on CBMC verification failure")
+    add_flag(group, "--mangler", default="v0",
+        help="Change what mangler is used by the Rust compiler")
+    add_flag(group, "--dry-run", action="store_true", 
+        help="Print commands instead of running them")
 
 def add_developer_flags(make_group, add_flag):
     group = make_group("Developer flags", "These are generally meant for use by RMC developers, and are not necessarily stable.")
-    add_flag(group, "--cbmc-args", nargs=argparse.REMAINDER,
-                        default=[], help="Pass through directly to CBMC")
+    add_flag(group, "--cbmc-args", nargs=argparse.REMAINDER, default=[], 
+                        help="Pass through directly to CBMC; must be the last flag")
 
 def add_flags(
     parser, 

From 3768cbe809b0904112dfe146cdc7e1908905a8e1 Mon Sep 17 00:00:00 2001
From: Thomas Del Vecchio <vecchiot@amazon.com>
Date: Thu, 15 Jul 2021 17:18:19 -0400
Subject: [PATCH 03/14] Add copyright.

---
 scripts/rmc_flags.py | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/scripts/rmc_flags.py b/scripts/rmc_flags.py
index df78219cfd30..97a48b18be70 100644
--- a/scripts/rmc_flags.py
+++ b/scripts/rmc_flags.py
@@ -1,3 +1,7 @@
+#!/usr/bin/env python3
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
 import argparse
 
 def add_loudness_flags(make_group, add_flag):
@@ -97,4 +101,3 @@ def add_flag(group, flag, *args, **kwargs):
     extra_flags = set(exclude_flags) - excluded_flags
     if extra_flags:
         print(f"WARNING: Attempt to exclude flags which don't exist: {extra_flags}")
-

From 5cd86b1daf0399aa3f58ddb70d652361e9fb814c Mon Sep 17 00:00:00 2001
From: Thomas Del Vecchio <vecchiot@amazon.com>
Date: Mon, 19 Jul 2021 09:47:35 -0400
Subject: [PATCH 04/14] PR review updates.

---
 scripts/cargo-rmc    |  2 +-
 scripts/rmc_flags.py | 84 +++++++++++++++++++++++++-------------------
 2 files changed, 49 insertions(+), 37 deletions(-)

diff --git a/scripts/cargo-rmc b/scripts/cargo-rmc
index cb43e58706ad..9ff293ec2c29 100755
--- a/scripts/cargo-rmc
+++ b/scripts/cargo-rmc
@@ -20,7 +20,7 @@ def main():
     if len(sys.argv) >= 2 and sys.argv[1] == "rmc":
         del sys.argv[1]
 
-    parser = argparse.ArgumentParser(description="Verify a Rust crate")
+    parser = argparse.ArgumentParser(prog="cargo rmc", description="Verify a Rust crate")
 
     crate_group = parser.add_argument_group("Crate", "You can pass in the rust crate positionally or with the --crate flag.")
     crate_group.add_argument("crate", help="crate to verify", nargs="?")
diff --git a/scripts/rmc_flags.py b/scripts/rmc_flags.py
index 97a48b18be70..0dadb0081ae2 100644
--- a/scripts/rmc_flags.py
+++ b/scripts/rmc_flags.py
@@ -5,68 +5,80 @@
 import argparse
 
 def add_loudness_flags(make_group, add_flag):
-    group = make_group("Loudness flags", "Determine how much textual output to produce.")
-    add_flag(group, "--debug", action="store_true", 
-        help="Produce full debug information")
+    group = make_group(
+        "Loudness flags", "Determine how much textual output to produce.")
+    add_flag(group, "--debug", action="store_true",
+             help="Produce full debug information")
     add_flag(group, "--verbose", "-v", action="store_true",
-        help="Output processing stages and commands, along with minor debug information")
+             help="Output processing stages and commands, along with minor debug information")
     add_flag(group, "--quiet", "-q", action="store_true",
-        help="Produces no output, just an exit code and requested artifacts. Overrides --verbose")
+             help="Produces no output, just an exit code and requested artifacts. Overrides --verbose")
 
-def add_um_flags(make_group, add_flag):
-    group = make_group("Um flags", "Um") # TODO: Come up with name and description
+
+def add_proof_harness_flags(make_group, add_flag):
+    group = make_group("Proof harness flags",
+                       "Provide information about the proof harness for RMC.")
     add_flag(group, "--c-lib", nargs="*", default=[], action="extend",
-        help="External C files referenced by Rust code")
+             help="External C files referenced by Rust code")
     add_flag(group, "--function", default="main",
-        help="Entry point for verification")
+             help="Entry point for verification")
+
 
 def add_artifact_flags(make_group, add_flag):
-    group = make_group("Artifact flags", "Produce artifacts in addition to a basic RMC report.")
+    group = make_group(
+        "Artifact flags", "Produce artifacts in addition to a basic RMC report.")
     add_flag(group, "--target-dir", default=".",
-        help="Directory for all generated artifacts")
+             help="Directory for all generated artifacts")
     add_flag(group, "--keep-temps", action="store_true",
-        help="Keep temporary files generated throughout RMC process")
+             help="Keep temporary files generated throughout RMC process")
     add_flag(group, "--gen-c", action="store_true",
-        help="Generate C file equivalent to inputted program")
+             help="Generate C file equivalent to inputted program")
     add_flag(group, "--gen-symbols", action="store_true",
-        help="Generate a symbol table")
+             help="Generate a symbol table")
+
 
 def add_check_flags(make_group, add_flag):
     group = make_group("Check flags", "Disable some or all default checks.")
-    add_flag(group, "--no-default-checks", action="store_true", help="Disable all default checks")
-    add_flag(group, "--no-memory-safety-checks", action="store_true", help="Disable default memory safety checks")
-    add_flag(group, "--no-overflow-checks", action="store_true", help="Disable default overflow checks")
-    add_flag(group, "--no-unwinding-checks", action="store_true", help="Disable default unwinding checks")
+    add_flag(group, "--no-default-checks", action="store_true",
+             help="Disable all default checks")
+    add_flag(group, "--no-memory-safety-checks", action="store_true",
+             help="Disable default memory safety checks")
+    add_flag(group, "--no-overflow-checks", action="store_true",
+             help="Disable default overflow checks")
+    add_flag(group, "--no-unwinding-checks", action="store_true",
+             help="Disable default unwinding checks")
+
 
 def add_visualizer_flags(make_group, add_flag):
-    group = make_group("Visualizer flags", "Generate an HTML-based UI for the generated RMC report.")
-    add_flag(group, "--srcdir", default=".") # TODO: help?
-    add_flag(group, "--wkdir", default=".") # TODO: help?
+    group = make_group(
+        "Visualizer flags", "Generate an HTML-based UI for the generated RMC report.\nSee https://github.com/awslabs/aws-viewer-for-cbmc.")
+    add_flag(group, "--srcdir", default=".")  # TODO: help?
+    add_flag(group, "--wkdir", default=".")  # TODO: help?
     add_flag(group, "--visualize", action="store_true",
-        help="Generate visualizer report; open report/html/index.html")
+             help="Generate visualizer report; open report/html/index.html")
+
 
 def add_other_flags(make_group, add_flag):
     group = make_group("Other flags")
     add_flag(group, "--allow-cbmc-verification-failure", action="store_true",
-        help="Do not produce error retcode on CBMC verification failure")
+             help="Do not produce error return code on CBMC verification failure")
     add_flag(group, "--mangler", default="v0",
-        help="Change what mangler is used by the Rust compiler")
-    add_flag(group, "--dry-run", action="store_true", 
-        help="Print commands instead of running them")
+             help="Change what mangler is used by the Rust compiler")
+    add_flag(group, "--dry-run", action="store_true",
+             help="Print commands instead of running them")
+
 
 def add_developer_flags(make_group, add_flag):
-    group = make_group("Developer flags", "These are generally meant for use by RMC developers, and are not necessarily stable.")
-    add_flag(group, "--cbmc-args", nargs=argparse.REMAINDER, default=[], 
-                        help="Pass through directly to CBMC; must be the last flag")
+    group = make_group(
+        "Developer flags", "These are generally meant for use by RMC developers, and are not stable.")
+    add_flag(group, "--cbmc-args", nargs=argparse.REMAINDER, default=[],
+             help="Pass through directly to CBMC; must be the last flag")
 
-def add_flags(
-    parser, 
-    exclude_flags=[],
-    exclude_groups=[]):
 
+def add_flags(parser, exclude_flags=[], exclude_groups=[]):
     excluded_flags = set()
     excluded_groups = set()
-    
+
     def make_group(title=None, description=None):
         return parser.add_argument_group(title, description)
 
@@ -78,12 +90,12 @@ def add_flag(group, flag, *args, **kwargs):
         if flag in exclude_flags:
             excluded_flags.add(flag)
             return
-        
+
         group.add_argument(flag, *args, **kwargs)
 
     add_groups = [
         add_loudness_flags,
-        add_um_flags,
+        add_proof_harness_flags,
         add_artifact_flags,
         add_check_flags,
         add_visualizer_flags,

From fa25498375defb1fdae6a5cb5942b770b029e1a4 Mon Sep 17 00:00:00 2001
From: Thomas Del Vecchio <vecchiot@amazon.com>
Date: Thu, 22 Jul 2021 15:40:21 -0400
Subject: [PATCH 05/14] Switch warn to fail on unsupported flags.

---
 scripts/cargo-rmc | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/scripts/cargo-rmc b/scripts/cargo-rmc
index 9ff293ec2c29..a45cfddf811a 100755
--- a/scripts/cargo-rmc
+++ b/scripts/cargo-rmc
@@ -42,10 +42,12 @@ def main():
         return 1
 
     if args.gen_symbols:
-        print("WARNING: --gen-symbols is not supported for cargo-rmc.")
+        print("Error: --gen-symbols is not supported for cargo-rmc.")
+        return 1
 
     if args.allow_cbmc_verification_failure:
-        print("WARNING: --allow-cbmc-verification-failure is not supported for cargo-rmc.")
+        print("Error: --allow-cbmc-verification-failure is not supported for cargo-rmc.")
+        return 1
 
     # Add some CBMC flags by default unless `--no-default-checks` is being used
     if not args.no_default_checks:

From ee21c949604bbfc1cfa3c7c33743a9358412ec8c Mon Sep 17 00:00:00 2001
From: Thomas Del Vecchio <vecchiot@amazon.com>
Date: Thu, 22 Jul 2021 15:49:07 -0400
Subject: [PATCH 06/14] Added help messages for --wkdir and --srcdir

---
 scripts/rmc_flags.py | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/scripts/rmc_flags.py b/scripts/rmc_flags.py
index 0dadb0081ae2..50f4d1632a14 100644
--- a/scripts/rmc_flags.py
+++ b/scripts/rmc_flags.py
@@ -52,8 +52,13 @@ def add_check_flags(make_group, add_flag):
 def add_visualizer_flags(make_group, add_flag):
     group = make_group(
         "Visualizer flags", "Generate an HTML-based UI for the generated RMC report.\nSee https://github.com/awslabs/aws-viewer-for-cbmc.")
-    add_flag(group, "--srcdir", default=".")  # TODO: help?
-    add_flag(group, "--wkdir", default=".")  # TODO: help?
+    add_flag(group, "--srcdir", default="."
+             help="The source directory. The root of the source tree.")
+    add_flag(group, "--wkdir", default="."
+             help="""
+                  The working directory. Used to determine source locations in output.
+                  This is generally the location from which rmc is currently being invoked.
+                  """)
     add_flag(group, "--visualize", action="store_true",
              help="Generate visualizer report; open report/html/index.html")
 

From 02dbbad643d26ceab64f6ea9ad9a368f5e22eb89 Mon Sep 17 00:00:00 2001
From: Thomas Del Vecchio <vecchiot@amazon.com>
Date: Thu, 22 Jul 2021 16:10:35 -0400
Subject: [PATCH 07/14] Add documentation and rearrange error handling.

---
 scripts/cargo-rmc    | 11 ++---------
 scripts/rmc          |  3 ++-
 scripts/rmc_flags.py | 42 +++++++++++++++++++++++++++++-------------
 3 files changed, 33 insertions(+), 23 deletions(-)

diff --git a/scripts/cargo-rmc b/scripts/cargo-rmc
index a45cfddf811a..b9711bb06a00 100755
--- a/scripts/cargo-rmc
+++ b/scripts/cargo-rmc
@@ -26,7 +26,8 @@ def main():
     crate_group.add_argument("crate", help="crate to verify", nargs="?")
     crate_group.add_argument("--crate", help="crate to verify", dest="crate_flag", metavar="CRATE")
 
-    rmc_flags.add_flags(parser)
+    if not rmc_flags.add_flags(parser, exclude_flags=["--gen-symbols, --allow-cbmc-verification-failure"]):
+        return 1
     args = parser.parse_args()
 
     if args.crate:
@@ -41,14 +42,6 @@ def main():
     if not rmc.dependencies_in_path():
         return 1
 
-    if args.gen_symbols:
-        print("Error: --gen-symbols is not supported for cargo-rmc.")
-        return 1
-
-    if args.allow_cbmc_verification_failure:
-        print("Error: --allow-cbmc-verification-failure is not supported for cargo-rmc.")
-        return 1
-
     # Add some CBMC flags by default unless `--no-default-checks` is being used
     if not args.no_default_checks:
         rmc.add_selected_default_cbmc_flags(args)
diff --git a/scripts/rmc b/scripts/rmc
index 1873edb9b2c7..8f5563868c67 100755
--- a/scripts/rmc
+++ b/scripts/rmc
@@ -22,7 +22,8 @@ def main():
     input_group.add_argument("input", help="Rust file to verify", nargs="?")
     input_group.add_argument("--input", help="Rust file to verify", dest="input_flag", metavar="INPUT")
 
-    rmc_flags.add_flags(parser, exclude_flags=["--function"])
+    if not rmc_flags.add_flags(parser, exclude_flags=["--function"]):
+        return 1
     args = parser.parse_args()
 
     # In the future we hope to make this configurable in the command line.
diff --git a/scripts/rmc_flags.py b/scripts/rmc_flags.py
index 50f4d1632a14..ebb095900bf0 100644
--- a/scripts/rmc_flags.py
+++ b/scripts/rmc_flags.py
@@ -4,6 +4,7 @@
 
 import argparse
 
+# Add flags related to debugging output.
 def add_loudness_flags(make_group, add_flag):
     group = make_group(
         "Loudness flags", "Determine how much textual output to produce.")
@@ -14,7 +15,7 @@ def add_loudness_flags(make_group, add_flag):
     add_flag(group, "--quiet", "-q", action="store_true",
              help="Produces no output, just an exit code and requested artifacts. Overrides --verbose")
 
-
+# Add flags which specify configurations for the proof.
 def add_proof_harness_flags(make_group, add_flag):
     group = make_group("Proof harness flags",
                        "Provide information about the proof harness for RMC.")
@@ -23,7 +24,7 @@ def add_proof_harness_flags(make_group, add_flag):
     add_flag(group, "--function", default="main",
              help="Entry point for verification")
 
-
+# Add flags that produce extra artifacts.
 def add_artifact_flags(make_group, add_flag):
     group = make_group(
         "Artifact flags", "Produce artifacts in addition to a basic RMC report.")
@@ -36,7 +37,7 @@ def add_artifact_flags(make_group, add_flag):
     add_flag(group, "--gen-symbols", action="store_true",
              help="Generate a symbol table")
 
-
+# Add flags to turn off default checks.
 def add_check_flags(make_group, add_flag):
     group = make_group("Check flags", "Disable some or all default checks.")
     add_flag(group, "--no-default-checks", action="store_true",
@@ -48,13 +49,13 @@ def add_check_flags(make_group, add_flag):
     add_flag(group, "--no-unwinding-checks", action="store_true",
              help="Disable default unwinding checks")
 
-
+# Add flags needed only for visualizer.
 def add_visualizer_flags(make_group, add_flag):
     group = make_group(
         "Visualizer flags", "Generate an HTML-based UI for the generated RMC report.\nSee https://github.com/awslabs/aws-viewer-for-cbmc.")
-    add_flag(group, "--srcdir", default="."
+    add_flag(group, "--srcdir", default=".",
              help="The source directory. The root of the source tree.")
-    add_flag(group, "--wkdir", default="."
+    add_flag(group, "--wkdir", default=".",
              help="""
                   The working directory. Used to determine source locations in output.
                   This is generally the location from which rmc is currently being invoked.
@@ -62,7 +63,7 @@ def add_visualizer_flags(make_group, add_flag):
     add_flag(group, "--visualize", action="store_true",
              help="Generate visualizer report; open report/html/index.html")
 
-
+# Add flags for ad-hoc features.
 def add_other_flags(make_group, add_flag):
     group = make_group("Other flags")
     add_flag(group, "--allow-cbmc-verification-failure", action="store_true",
@@ -72,24 +73,33 @@ def add_other_flags(make_group, add_flag):
     add_flag(group, "--dry-run", action="store_true",
              help="Print commands instead of running them")
 
-
+# Add flags we don't expect end-users to use.
 def add_developer_flags(make_group, add_flag):
     group = make_group(
         "Developer flags", "These are generally meant for use by RMC developers, and are not stable.")
     add_flag(group, "--cbmc-args", nargs=argparse.REMAINDER, default=[],
              help="Pass through directly to CBMC; must be the last flag")
 
-
+# Adds the flags common to both rmc and cargo-rmc.
+# Allows you to specify flags/groups of flags to not add.
+# This does not return the parser, but mutates the one provided.
 def add_flags(parser, exclude_flags=[], exclude_groups=[]):
+    # Keep track of what excluded flags and groups we've seen
+    # so we can warn for possibly incorrect names passed in.
     excluded_flags = set()
     excluded_groups = set()
 
+    # Add a group to the parser with title/description, and get a handler for it.
     def make_group(title=None, description=None):
+        if title in exclude_groups:
+            excluded_groups.add(group.title)
+            return None
+
         return parser.add_argument_group(title, description)
 
+    # Add the flag to the group, 
     def add_flag(group, flag, *args, **kwargs):
-        if group.title in exclude_groups:
-            excluded_groups.add(group.title)
+        if group == None:
             return
 
         if flag in exclude_flags:
@@ -111,10 +121,16 @@ def add_flag(group, flag, *args, **kwargs):
     for add_group in add_groups:
         add_group(make_group, add_flag)
 
+    # Error if any excluded flags/groups don't exist.
     extra_groups = set(exclude_groups) - excluded_groups
     if extra_groups:
-        print(f"WARNING: Attempt to exclude groups which don't exist: {extra_groups}")
+        print(f"ERROR: Attempt to exclude groups which don't exist: {extra_groups}")
 
     extra_flags = set(exclude_flags) - excluded_flags
     if extra_flags:
-        print(f"WARNING: Attempt to exclude flags which don't exist: {extra_flags}")
+        print(f"ERROR: Attempt to exclude flags which don't exist: {extra_flags}")
+
+    if extra_groups or extra_flags:
+        return False
+
+    return True
\ No newline at end of file

From b17a39ebf069f59b4d01c1f056328cf9fb1559e7 Mon Sep 17 00:00:00 2001
From: Thomas Del Vecchio <vecchiot@amazon.com>
Date: Thu, 22 Jul 2021 16:18:10 -0400
Subject: [PATCH 08/14] Fix incorrect 'exclude_flags' value in cargo-rmc.

---
 scripts/cargo-rmc    | 2 +-
 scripts/rmc_flags.py | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/scripts/cargo-rmc b/scripts/cargo-rmc
index b9711bb06a00..e1474a23584b 100755
--- a/scripts/cargo-rmc
+++ b/scripts/cargo-rmc
@@ -26,7 +26,7 @@ def main():
     crate_group.add_argument("crate", help="crate to verify", nargs="?")
     crate_group.add_argument("--crate", help="crate to verify", dest="crate_flag", metavar="CRATE")
 
-    if not rmc_flags.add_flags(parser, exclude_flags=["--gen-symbols, --allow-cbmc-verification-failure"]):
+    if not rmc_flags.add_flags(parser, exclude_flags=["--gen-symbols", "--allow-cbmc-verification-failure"]):
         return 1
     args = parser.parse_args()
 
diff --git a/scripts/rmc_flags.py b/scripts/rmc_flags.py
index ebb095900bf0..61fd468a15c0 100644
--- a/scripts/rmc_flags.py
+++ b/scripts/rmc_flags.py
@@ -133,4 +133,4 @@ def add_flag(group, flag, *args, **kwargs):
     if extra_groups or extra_flags:
         return False
 
-    return True
\ No newline at end of file
+    return True

From 23b9438ab00ec216c858612b85a9c745b9ed266a Mon Sep 17 00:00:00 2001
From: Thomas Del Vecchio <vecchiot@amazon.com>
Date: Fri, 23 Jul 2021 14:14:14 -0400
Subject: [PATCH 09/14] Changes from deep dive.

---
 scripts/cargo-rmc    | 17 ++++++-------
 scripts/rmc          | 17 ++++++-------
 scripts/rmc.py       | 13 ++++++----
 scripts/rmc_flags.py | 58 +++++++++++++++++++++-----------------------
 4 files changed, 50 insertions(+), 55 deletions(-)

diff --git a/scripts/cargo-rmc b/scripts/cargo-rmc
index e1474a23584b..963ddfc24e41 100755
--- a/scripts/cargo-rmc
+++ b/scripts/cargo-rmc
@@ -20,27 +20,25 @@ def main():
     if len(sys.argv) >= 2 and sys.argv[1] == "rmc":
         del sys.argv[1]
 
-    parser = argparse.ArgumentParser(prog="cargo rmc", description="Verify a Rust crate")
+    parser = argparse.ArgumentParser(prog="cargo rmc", description="Verify a Rust crate. For more information, see https://github.com/model-checking/rmc.")
 
     crate_group = parser.add_argument_group("Crate", "You can pass in the rust crate positionally or with the --crate flag.")
     crate_group.add_argument("crate", help="crate to verify", nargs="?")
     crate_group.add_argument("--crate", help="crate to verify", dest="crate_flag", metavar="CRATE")
 
-    if not rmc_flags.add_flags(parser, exclude_flags=["--gen-symbols", "--allow-cbmc-verification-failure"]):
-        return 1
+    rmc_flags.add_flags(parser, {"default-target", "target"}, exclude_flags=["--gen-symbols", "--allow-cbmc-verification-failure"])
     args = parser.parse_args()
 
     if args.crate:
-        assert args.crate_flag is None, "Please provide a single crate to verify."
+        rmc.ensure(args.crate_flag is None, "Please provide a single crate to verify.")
     else:
-        assert args.crate_flag is not None, "Please provide a crate to verify."
+        rmc.ensure(args.crate_flag is not None, "Please provide a crate to verify.")
         args.crate = args.crate_flag
 
     if args.quiet:
         args.verbose = False
 
-    if not rmc.dependencies_in_path():
-        return 1
+    rmc.ensure_dependencies_in_path()
 
     # Add some CBMC flags by default unless `--no-default-checks` is being used
     if not args.no_default_checks:
@@ -51,9 +49,8 @@ def main():
 
     pattern = os.path.join(args.target_dir, "debug", "deps", "*.json")
     jsons = glob.glob(pattern)
-    if len(jsons) != 1:
-        print("ERROR: unexpected number of json outputs")
-        return 1
+    rmc.ensure(len(jsons) == 1, "Unexpected number of json outputs.")
+
     cbmc_filename = os.path.join(args.target_dir, "cbmc.out")
     c_filename = os.path.join(args.target_dir, "cbmc.c")
     if EXIT_CODE_SUCCESS != rmc.symbol_table_to_gotoc(jsons[0], cbmc_filename, args.verbose, args.keep_temps, args.dry_run):
diff --git a/scripts/rmc b/scripts/rmc
index 8f5563868c67..98fb138a7b03 100755
--- a/scripts/rmc
+++ b/scripts/rmc
@@ -16,14 +16,13 @@ CBMC_VERIFICATION_FAILURE_EXIT_CODE = 10
 
 
 def main():
-    parser = argparse.ArgumentParser(description="Verify a single Rust file")
+    parser = argparse.ArgumentParser(description="Verify a single Rust file. For more information, see https://github.com/model-checking/rmc.")
 
     input_group = parser.add_argument_group("Input", "You can pass in the rust file positionally or with the --input flag.")
     input_group.add_argument("input", help="Rust file to verify", nargs="?")
     input_group.add_argument("--input", help="Rust file to verify", dest="input_flag", metavar="INPUT")
 
-    if not rmc_flags.add_flags(parser, exclude_flags=["--function"]):
-        return 1
+    rmc_flags.add_flags(parser, {"default-target", "."}, exclude_flags=["--function"])
     args = parser.parse_args()
 
     # In the future we hope to make this configurable in the command line.
@@ -32,25 +31,23 @@ def main():
     args.function = "main"
 
     if args.input:
-        assert args.input_flag is None, "Please provide a single file to verify."
+        rmc.ensure(args.input_flag is None, "Please provide a single file to verify.")
     else:
-        assert args.input_flag is not None, "Please provide a file to verify."
+        rmc.ensure(args.input_flag is not None, "Please provide a file to verify.")
         args.input = args.input_flag
     
     if args.quiet:
         args.verbose = False
 
-    if not rmc.dependencies_in_path():
-        return 1
+    rmc.ensure_dependencies_in_path()
     
     # Add some CBMC flags by default unless `--no-default-checks` is being used
     if not args.no_default_checks:
         rmc.add_selected_default_cbmc_flags(args)
 
     base, ext = os.path.splitext(args.input)
-    if ext != ".rs":
-        print("ERROR: Expecting .rs input file")
-        return 1
+    rmc.ensure(ext == ".rs", "Expecting .rs input file.")
+
     json_filename = base + ".json"
     goto_filename = base + ".goto"
     c_filename = base + ".c"
diff --git a/scripts/rmc.py b/scripts/rmc.py
index 4bd3e8349d89..2c096da72fad 100644
--- a/scripts/rmc.py
+++ b/scripts/rmc.py
@@ -5,6 +5,7 @@
 import atexit
 import os
 import os.path
+import sys
 import re
 
 
@@ -40,17 +41,19 @@ def match(self, text):
     def edit_output(self, text):
         return self.edit_fun(text)
 
+def ensure(condition, message, retcode=1):
+    if not condition:
+        print(f"ERROR: {message}")
+        sys.exit(retcode)
+
 def is_exe(name):
     from shutil import which
     return which(name) is not None
 
 
-def dependencies_in_path():
+def ensure_dependencies_in_path():
     for program in [RMC_RUSTC_EXE, "symtab2gb", "cbmc", "cbmc-viewer", "goto-instrument", "goto-cc"]:
-        if not is_exe(program):
-            print("ERROR: Could not find {} in PATH".format(program))
-            return False
-    return True
+        ensure(is_exe(program), f"Could not find {program} in PATH")
 
 
 def delete_file(filename):
diff --git a/scripts/rmc_flags.py b/scripts/rmc_flags.py
index 61fd468a15c0..1f13f1b30d8a 100644
--- a/scripts/rmc_flags.py
+++ b/scripts/rmc_flags.py
@@ -5,7 +5,7 @@
 import argparse
 
 # Add flags related to debugging output.
-def add_loudness_flags(make_group, add_flag):
+def add_loudness_flags(make_group, add_flag, config):
     group = make_group(
         "Loudness flags", "Determine how much textual output to produce.")
     add_flag(group, "--debug", action="store_true",
@@ -16,29 +16,34 @@ def add_loudness_flags(make_group, add_flag):
              help="Produces no output, just an exit code and requested artifacts. Overrides --verbose")
 
 # Add flags which specify configurations for the proof.
-def add_proof_harness_flags(make_group, add_flag):
-    group = make_group("Proof harness flags",
-                       "Provide information about the proof harness for RMC.")
+def add_linking_flags(make_group, add_flag, config):
+    group = make_group("Linking flags",
+                       "Provide information about how to link the prover for RMC.")
     add_flag(group, "--c-lib", nargs="*", default=[], action="extend",
-             help="External C files referenced by Rust code")
+             help="Link external C files referenced by Rust code")
     add_flag(group, "--function", default="main",
              help="Entry point for verification")
 
 # Add flags that produce extra artifacts.
-def add_artifact_flags(make_group, add_flag):
+def add_artifact_flags(make_group, add_flag, config):
+    default_target = config["default-target"]
+    assert default_target is not None, \
+        f"Missing item in parser config: \"default-target\".\n" \
+        "This is a bug; please report this to https://github.com/model-checking/rmc/issues."
+
     group = make_group(
         "Artifact flags", "Produce artifacts in addition to a basic RMC report.")
-    add_flag(group, "--target-dir", default=".",
-             help="Directory for all generated artifacts")
+    add_flag(group, "--target-dir", default=default_target, metavar="DIR",
+             help=f"Directory for all generated artifacts. Defaults to \"{default_target}\"")
     add_flag(group, "--keep-temps", action="store_true",
              help="Keep temporary files generated throughout RMC process")
     add_flag(group, "--gen-c", action="store_true",
              help="Generate C file equivalent to inputted program")
     add_flag(group, "--gen-symbols", action="store_true",
-             help="Generate a symbol table")
+             help="Generate a goto symbol table")
 
 # Add flags to turn off default checks.
-def add_check_flags(make_group, add_flag):
+def add_check_flags(make_group, add_flag, config):
     group = make_group("Check flags", "Disable some or all default checks.")
     add_flag(group, "--no-default-checks", action="store_true",
              help="Disable all default checks")
@@ -50,7 +55,7 @@ def add_check_flags(make_group, add_flag):
              help="Disable default unwinding checks")
 
 # Add flags needed only for visualizer.
-def add_visualizer_flags(make_group, add_flag):
+def add_visualizer_flags(make_group, add_flag, config):
     group = make_group(
         "Visualizer flags", "Generate an HTML-based UI for the generated RMC report.\nSee https://github.com/awslabs/aws-viewer-for-cbmc.")
     add_flag(group, "--srcdir", default=".",
@@ -61,29 +66,29 @@ def add_visualizer_flags(make_group, add_flag):
                   This is generally the location from which rmc is currently being invoked.
                   """)
     add_flag(group, "--visualize", action="store_true",
-             help="Generate visualizer report; open report/html/index.html")
+             help="Generate visualizer report to <target-dir>/report/html/index.html")
 
 # Add flags for ad-hoc features.
-def add_other_flags(make_group, add_flag):
+def add_other_flags(make_group, add_flag, config):
     group = make_group("Other flags")
     add_flag(group, "--allow-cbmc-verification-failure", action="store_true",
              help="Do not produce error return code on CBMC verification failure")
-    add_flag(group, "--mangler", default="v0",
-             help="Change what mangler is used by the Rust compiler")
     add_flag(group, "--dry-run", action="store_true",
              help="Print commands instead of running them")
 
 # Add flags we don't expect end-users to use.
-def add_developer_flags(make_group, add_flag):
+def add_developer_flags(make_group, add_flag, config):
     group = make_group(
         "Developer flags", "These are generally meant for use by RMC developers, and are not stable.")
     add_flag(group, "--cbmc-args", nargs=argparse.REMAINDER, default=[],
              help="Pass through directly to CBMC; must be the last flag")
+    add_flag(group, "--mangler", default="v0", choices=["v0", "legacy"],
+             help="Change what mangler is used by the Rust compiler")
 
 # Adds the flags common to both rmc and cargo-rmc.
 # Allows you to specify flags/groups of flags to not add.
 # This does not return the parser, but mutates the one provided.
-def add_flags(parser, exclude_flags=[], exclude_groups=[]):
+def add_flags(parser, config, exclude_flags=[], exclude_groups=[]):
     # Keep track of what excluded flags and groups we've seen
     # so we can warn for possibly incorrect names passed in.
     excluded_flags = set()
@@ -110,7 +115,7 @@ def add_flag(group, flag, *args, **kwargs):
 
     add_groups = [
         add_loudness_flags,
-        add_proof_harness_flags,
+        add_linking_flags,
         add_artifact_flags,
         add_check_flags,
         add_visualizer_flags,
@@ -119,18 +124,11 @@ def add_flag(group, flag, *args, **kwargs):
     ]
 
     for add_group in add_groups:
-        add_group(make_group, add_flag)
+        add_group(make_group, add_flag, config)
 
     # Error if any excluded flags/groups don't exist.
-    extra_groups = set(exclude_groups) - excluded_groups
-    if extra_groups:
-        print(f"ERROR: Attempt to exclude groups which don't exist: {extra_groups}")
-
     extra_flags = set(exclude_flags) - excluded_flags
-    if extra_flags:
-        print(f"ERROR: Attempt to exclude flags which don't exist: {extra_flags}")
-
-    if extra_groups or extra_flags:
-        return False
-
-    return True
+    extra_groups = set(exclude_groups) - excluded_groups
+    assert len(extra_flags.union(extra_groups)) == 0, \
+        f"Attempt to exclude parser options which don't exist: {extra_groups.union(extra_flags)}\n" \
+        "This is a bug; please report this to https://github.com/model-checking/rmc/issues."

From 76b1f20dbbcb4a6997ae2d29be417b090f02cd01 Mon Sep 17 00:00:00 2001
From: Thomas Del Vecchio <vecchiot@amazon.com>
Date: Fri, 23 Jul 2021 14:21:27 -0400
Subject: [PATCH 10/14] Rearrange, and add documentation.

---
 scripts/rmc.py | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/scripts/rmc.py b/scripts/rmc.py
index 2c096da72fad..e2fdee7b2ca1 100644
--- a/scripts/rmc.py
+++ b/scripts/rmc.py
@@ -41,21 +41,21 @@ def match(self, text):
     def edit_output(self, text):
         return self.edit_fun(text)
 
-def ensure(condition, message, retcode=1):
-    if not condition:
-        print(f"ERROR: {message}")
-        sys.exit(retcode)
-
 def is_exe(name):
     from shutil import which
     return which(name) is not None
-
-
+    
 def ensure_dependencies_in_path():
     for program in [RMC_RUSTC_EXE, "symtab2gb", "cbmc", "cbmc-viewer", "goto-instrument", "goto-cc"]:
         ensure(is_exe(program), f"Could not find {program} in PATH")
 
+# Assert a condition holds, or produce a user error message.
+def ensure(condition, message, retcode=1):
+    if not condition:
+        print(f"ERROR: {message}")
+        sys.exit(retcode)
 
+# Deletes a file; used by atexit.register to remove temporary files on exit
 def delete_file(filename):
     try:
         os.remove(filename)

From cd7352c1428cf0ba7e1cc5f8be6a62578765e303 Mon Sep 17 00:00:00 2001
From: Thomas Del Vecchio <vecchiot@amazon.com>
Date: Fri, 23 Jul 2021 14:22:57 -0400
Subject: [PATCH 11/14] Fix typo.

---
 scripts/cargo-rmc | 2 +-
 scripts/rmc       | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/scripts/cargo-rmc b/scripts/cargo-rmc
index 963ddfc24e41..f2865665c38a 100755
--- a/scripts/cargo-rmc
+++ b/scripts/cargo-rmc
@@ -26,7 +26,7 @@ def main():
     crate_group.add_argument("crate", help="crate to verify", nargs="?")
     crate_group.add_argument("--crate", help="crate to verify", dest="crate_flag", metavar="CRATE")
 
-    rmc_flags.add_flags(parser, {"default-target", "target"}, exclude_flags=["--gen-symbols", "--allow-cbmc-verification-failure"])
+    rmc_flags.add_flags(parser, {"default-target": "target"}, exclude_flags=["--gen-symbols", "--allow-cbmc-verification-failure"])
     args = parser.parse_args()
 
     if args.crate:
diff --git a/scripts/rmc b/scripts/rmc
index 98fb138a7b03..65cf9849be6a 100755
--- a/scripts/rmc
+++ b/scripts/rmc
@@ -22,7 +22,7 @@ def main():
     input_group.add_argument("input", help="Rust file to verify", nargs="?")
     input_group.add_argument("--input", help="Rust file to verify", dest="input_flag", metavar="INPUT")
 
-    rmc_flags.add_flags(parser, {"default-target", "."}, exclude_flags=["--function"])
+    rmc_flags.add_flags(parser, {"default-target": "."}, exclude_flags=["--function"])
     args = parser.parse_args()
 
     # In the future we hope to make this configurable in the command line.

From 54168ac1f00cfb428c691de781033a1d93629ba6 Mon Sep 17 00:00:00 2001
From: Thomas Del Vecchio <vecchiot@amazon.com>
Date: Fri, 23 Jul 2021 14:27:23 -0400
Subject: [PATCH 12/14] Fix formatting of help strings to be consistent.

---
 scripts/rmc_flags.py | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/scripts/rmc_flags.py b/scripts/rmc_flags.py
index 1f13f1b30d8a..5361febf932d 100644
--- a/scripts/rmc_flags.py
+++ b/scripts/rmc_flags.py
@@ -13,7 +13,7 @@ def add_loudness_flags(make_group, add_flag, config):
     add_flag(group, "--verbose", "-v", action="store_true",
              help="Output processing stages and commands, along with minor debug information")
     add_flag(group, "--quiet", "-q", action="store_true",
-             help="Produces no output, just an exit code and requested artifacts. Overrides --verbose")
+             help="Produces no output, just an exit code and requested artifacts; overrides --verbose")
 
 # Add flags which specify configurations for the proof.
 def add_linking_flags(make_group, add_flag, config):
@@ -34,7 +34,7 @@ def add_artifact_flags(make_group, add_flag, config):
     group = make_group(
         "Artifact flags", "Produce artifacts in addition to a basic RMC report.")
     add_flag(group, "--target-dir", default=default_target, metavar="DIR",
-             help=f"Directory for all generated artifacts. Defaults to \"{default_target}\"")
+             help=f"Directory for all generated artifacts; defaults to \"{default_target}\"")
     add_flag(group, "--keep-temps", action="store_true",
              help="Keep temporary files generated throughout RMC process")
     add_flag(group, "--gen-c", action="store_true",
@@ -59,11 +59,11 @@ def add_visualizer_flags(make_group, add_flag, config):
     group = make_group(
         "Visualizer flags", "Generate an HTML-based UI for the generated RMC report.\nSee https://github.com/awslabs/aws-viewer-for-cbmc.")
     add_flag(group, "--srcdir", default=".",
-             help="The source directory. The root of the source tree.")
+             help="The source directory: the root of the source tree")
     add_flag(group, "--wkdir", default=".",
              help="""
-                  The working directory. Used to determine source locations in output.
-                  This is generally the location from which rmc is currently being invoked.
+                  The working directory: used to determine source locations in output;
+                  this is generally the location from which rmc is currently being invoked
                   """)
     add_flag(group, "--visualize", action="store_true",
              help="Generate visualizer report to <target-dir>/report/html/index.html")

From eeba9d27432d9d5fba81a90a885fbb2d7f3dba4b Mon Sep 17 00:00:00 2001
From: Thomas Del Vecchio <vecchiot@amazon.com>
Date: Mon, 26 Jul 2021 10:42:42 -0400
Subject: [PATCH 13/14] Add reasons for excluding flags.

---
 scripts/cargo-rmc |  8 +++++++-
 scripts/rmc       | 12 +++++++-----
 2 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/scripts/cargo-rmc b/scripts/cargo-rmc
index f2865665c38a..b1444a823fbd 100755
--- a/scripts/cargo-rmc
+++ b/scripts/cargo-rmc
@@ -26,7 +26,13 @@ def main():
     crate_group.add_argument("crate", help="crate to verify", nargs="?")
     crate_group.add_argument("--crate", help="crate to verify", dest="crate_flag", metavar="CRATE")
 
-    rmc_flags.add_flags(parser, {"default-target": "target"}, exclude_flags=["--gen-symbols", "--allow-cbmc-verification-failure"])
+    exclude_flags = [
+        # This should be able to be supported; https://github.com/model-checking/rmc/issues/359
+        "--gen-symbols",
+        # This should be able to be supported; https://github.com/model-checking/rmc/issues/360
+        "--allow-cbmc-verification-failure",
+    ]
+    rmc_flags.add_flags(parser, {"default-target": "target"}, exclude_flags=exclude_flags)
     args = parser.parse_args()
 
     if args.crate:
diff --git a/scripts/rmc b/scripts/rmc
index 65cf9849be6a..6f0d14c840d8 100755
--- a/scripts/rmc
+++ b/scripts/rmc
@@ -22,12 +22,14 @@ def main():
     input_group.add_argument("input", help="Rust file to verify", nargs="?")
     input_group.add_argument("--input", help="Rust file to verify", dest="input_flag", metavar="INPUT")
 
-    rmc_flags.add_flags(parser, {"default-target": "."}, exclude_flags=["--function"])
+    exclude_flags = [
+        # In the future we hope to make this configurable in the command line.
+        # For now, however, changing this from "main" breaks rmc.
+        # Issue: https://github.com/model-checking/rmc/issues/169
+        "--function"
+    ]
+    rmc_flags.add_flags(parser, {"default-target": "."}, exclude_flags=exclude_flags)
     args = parser.parse_args()
-
-    # In the future we hope to make this configurable in the command line.
-    # For now, however, changing this from "main" breaks rmc.
-    # Issue: https://github.com/model-checking/rmc/issues/169
     args.function = "main"
 
     if args.input:

From 9742fdda4be7210f7b16efebdcaa88bc8e361cb6 Mon Sep 17 00:00:00 2001
From: Thomas Del Vecchio <vecchiot@amazon.com>
Date: Mon, 26 Jul 2021 10:44:45 -0400
Subject: [PATCH 14/14] Sorted flags alphabetically.

---
 scripts/rmc_flags.py | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/scripts/rmc_flags.py b/scripts/rmc_flags.py
index 5361febf932d..2a3ef783c23e 100644
--- a/scripts/rmc_flags.py
+++ b/scripts/rmc_flags.py
@@ -10,10 +10,10 @@ def add_loudness_flags(make_group, add_flag, config):
         "Loudness flags", "Determine how much textual output to produce.")
     add_flag(group, "--debug", action="store_true",
              help="Produce full debug information")
-    add_flag(group, "--verbose", "-v", action="store_true",
-             help="Output processing stages and commands, along with minor debug information")
     add_flag(group, "--quiet", "-q", action="store_true",
              help="Produces no output, just an exit code and requested artifacts; overrides --verbose")
+    add_flag(group, "--verbose", "-v", action="store_true",
+             help="Output processing stages and commands, along with minor debug information")
 
 # Add flags which specify configurations for the proof.
 def add_linking_flags(make_group, add_flag, config):
@@ -33,14 +33,14 @@ def add_artifact_flags(make_group, add_flag, config):
 
     group = make_group(
         "Artifact flags", "Produce artifacts in addition to a basic RMC report.")
-    add_flag(group, "--target-dir", default=default_target, metavar="DIR",
-             help=f"Directory for all generated artifacts; defaults to \"{default_target}\"")
-    add_flag(group, "--keep-temps", action="store_true",
-             help="Keep temporary files generated throughout RMC process")
     add_flag(group, "--gen-c", action="store_true",
              help="Generate C file equivalent to inputted program")
     add_flag(group, "--gen-symbols", action="store_true",
              help="Generate a goto symbol table")
+    add_flag(group, "--keep-temps", action="store_true",
+             help="Keep temporary files generated throughout RMC process")
+    add_flag(group, "--target-dir", default=default_target, metavar="DIR",
+             help=f"Directory for all generated artifacts; defaults to \"{default_target}\"")
 
 # Add flags to turn off default checks.
 def add_check_flags(make_group, add_flag, config):
@@ -60,13 +60,13 @@ def add_visualizer_flags(make_group, add_flag, config):
         "Visualizer flags", "Generate an HTML-based UI for the generated RMC report.\nSee https://github.com/awslabs/aws-viewer-for-cbmc.")
     add_flag(group, "--srcdir", default=".",
              help="The source directory: the root of the source tree")
+    add_flag(group, "--visualize", action="store_true",
+             help="Generate visualizer report to <target-dir>/report/html/index.html")
     add_flag(group, "--wkdir", default=".",
              help="""
                   The working directory: used to determine source locations in output;
                   this is generally the location from which rmc is currently being invoked
                   """)
-    add_flag(group, "--visualize", action="store_true",
-             help="Generate visualizer report to <target-dir>/report/html/index.html")
 
 # Add flags for ad-hoc features.
 def add_other_flags(make_group, add_flag, config):