Require --unsafe option with --no-verification

Closes #987
AdaCore · Sep 2, 2022 · bcee7a7 · bcee7a7
1 parent 69d6522
commit bcee7a7
Show file tree

Hide file tree

Showing 4 changed files with 54 additions and 1 deletion.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -12,6 +12,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 CLI:
 
 - `rflx setup_ide` subcommand for installing IDE integration (#795)
+- `rflx` option `--unsafe` (#987)
 
 ## [0.6.0] - 2022-08-31
 

diff --git a/ide/gnatstudio/recordflux.py b/ide/gnatstudio/recordflux.py
@@ -302,7 +302,7 @@ def run(files, mode, skip_verification=False, options=None):
     GPS.Locations.remove_category("RecordFlux")
 
     return "rflx {skip_verification}{mode} {options} {files}".format(
-        skip_verification="--no-verification " if skip_verification else "",
+        skip_verification="--unsafe --no-verification " if skip_verification else "",
         mode=mode,
         files=" ".join(files),
         options=" ".join(options),

diff --git a/rflx/cli.py b/rflx/cli.py
@@ -52,6 +52,11 @@ def main(argv: List[str]) -> Union[int, str]:  # pylint: disable = too-many-stat
         metavar=("NUM"),
         help="parallelize proofs among NUM workers (default: %(default)d)",
     )
+    parser.add_argument(
+        "--unsafe",
+        action="store_true",
+        help=("allow unsafe options (WARNING: may lead to erronous behavior"),
+    )
 
     subparsers = parser.add_subparsers(dest="subcommand")
 
@@ -209,13 +214,24 @@ def main(argv: List[str]) -> Union[int, str]:  # pylint: disable = too-many-stat
     if args.quiet:
         logging.disable(logging.CRITICAL)
 
+    if not args.unsafe:
+        if args.no_verification:
+            return 'cli: error: unsafe option "--no-verification" given without "--unsafe"'
+
     ERROR_CONFIG.fail_after_value = args.max_errors
 
     try:
         args.func(args)
     except RecordFluxError as e:
         return f"{e}"
     except Exception:  # pylint: disable = broad-except
+        if args.unsafe:
+            return f"""
+----------------------------------------------------------------------------
+EXCEPTION IN UNSAFE MODE, PLEASE RERUN WITHOUT UNSAFE OPTIONS
+----------------------------------------------------------------------------
+{traceback.format_exc()}
+----------------------------------------------------------------------------"""
         return f"""
 ------------------------------ RecordFlux Bug ------------------------------
 {version()}

diff --git a/tests/unit/cli_test.py b/tests/unit/cli_test.py
@@ -481,3 +481,39 @@ def test_setup_gnat_studio_plugin() -> None:
     plugin = Path.home() / ".gnatstudio/plug-ins/recordflux.py"
     assert plugin.exists()
     assert plugin.is_file()
+
+
+def test_missing_unsafe_option() -> None:
+    assert (
+        cli.main(
+            [
+                "rflx",
+                "--no-verification",
+                "check",
+                MESSAGE_SPEC_FILE,
+            ]
+        )
+        == 'cli: error: unsafe option "--no-verification" given without "--unsafe"'
+    )
+
+
+def test_exception_in_unsafe_mode(monkeypatch: MonkeyPatch, tmp_path: Path) -> None:
+    monkeypatch.setattr(cli, "generate", lambda x: raise_fatal_error())
+    assert re.fullmatch(
+        r"\n-*\nEXCEPTION IN UNSAFE MODE, PLEASE RERUN WITHOUT UNSAFE OPTIONS\n-*\n"
+        r"Traceback.*\n-*$",
+        str(
+            cli.main(
+                [
+                    "rflx",
+                    "--unsafe",
+                    "generate",
+                    "-d",
+                    str(tmp_path),
+                    MESSAGE_SPEC_FILE,
+                    SESSION_SPEC_FILE,
+                ]
+            )
+        ),
+        re.DOTALL,
+    )