Expose -Wno via ignore-warnings kompile option (#4471)

Address #4470
runtimeverification · Jun 25, 2024 · 3bc2373 · 3bc2373
1 parent 94a069d
commit 3bc2373
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 0 deletions.
diff --git a/pyk/src/pyk/__main__.py b/pyk/src/pyk/__main__.py
@@ -346,6 +346,7 @@ def exec_kompile(options: KompileCommandOptions) -> None:
             type_inference_mode=options.type_inference_mode,
             warnings=options.warnings,
             warnings_to_errors=options.warnings_to_errors,
+            ignore_warnings=options.ignore_warnings,
             no_exc_wrap=options.no_exc_wrap,
         )
     except RuntimeError as err:

diff --git a/pyk/src/pyk/cli/args.py b/pyk/src/pyk/cli/args.py
@@ -206,6 +206,7 @@ class KompileOptions(Options):
     bison_lists: bool
     no_exc_wrap: bool
     outer_parsed_json: bool
+    ignore_warnings: list[str]
 
     @staticmethod
     def default() -> dict[str, Any]:
@@ -230,6 +231,7 @@ def default() -> dict[str, Any]:
             'bison_lists': False,
             'no_exc_wrap': False,
             'outer_parsed_json': False,
+            'ignore_warnings': [],
         }
 
     @staticmethod
@@ -475,6 +477,9 @@ def kompile_args(self) -> ArgumentParser:
             action='store_true',
             help='Do not wrap the output on the CLI.',
         )
+        args.add_argument(
+            '--ignore-warnings', '-Wno', dest='ignore_warnings', action='append', help='Ignore provided warnings'
+        )
         return args
 
     @cached_property

diff --git a/pyk/src/pyk/ktool/kompile.py b/pyk/src/pyk/ktool/kompile.py
@@ -58,6 +58,7 @@ def kompile(
     type_inference_mode: str | TypeInferenceMode | None = None,
     warnings: str | Warnings | None = None,
     warnings_to_errors: bool = False,
+    ignore_warnings: Iterable[str] = (),
     no_exc_wrap: bool = False,
     # ---
     debug: bool = False,
@@ -78,6 +79,7 @@ def kompile(
             type_inference_mode=type_inference_mode,
             warnings=warnings,
             warnings_to_errors=warnings_to_errors,
+            ignore_warnings=ignore_warnings,
             no_exc_wrap=no_exc_wrap,
             debug=debug,
             verbose=verbose,
@@ -96,6 +98,7 @@ def kompile(
         type_inference_mode=type_inference_mode,
         warnings=warnings,
         warnings_to_errors=warnings_to_errors,
+        ignore_warnings=ignore_warnings,
         no_exc_wrap=no_exc_wrap,
         debug=debug,
         verbose=verbose,
@@ -111,6 +114,7 @@ def _booster_kompile(
     type_inference_mode: str | TypeInferenceMode | None,
     warnings: str | Warnings | None,
     warnings_to_errors: bool,
+    ignore_warnings: Iterable[str],
     no_exc_wrap: bool,
     # ---
     debug: bool,
@@ -146,6 +150,7 @@ def kompile_llvm() -> None:
             type_inference_mode=type_inference_mode,
             warnings=warnings,
             warnings_to_errors=warnings_to_errors,
+            ignore_warnings=ignore_warnings,
             no_exc_wrap=no_exc_wrap,
             debug=debug,
             verbose=verbose,
@@ -161,6 +166,7 @@ def kompile_haskell() -> None:
             type_inference_mode=type_inference_mode,
             warnings=warnings,
             warnings_to_errors=warnings_to_errors,
+            ignore_warnings=ignore_warnings,
             no_exc_wrap=no_exc_wrap,
             debug=debug,
             verbose=verbose,
@@ -273,6 +279,7 @@ def __call__(
         type_inference_mode: str | TypeInferenceMode | None = None,
         warnings: str | Warnings | None = None,
         warnings_to_errors: bool = False,
+        ignore_warnings: Iterable[str] = (),
         no_exc_wrap: bool = False,
         debug: bool = False,
         verbose: bool = False,
@@ -321,6 +328,9 @@ def __call__(
         if outer_parsed_json:
             args += ['--outer-parsed-json']
 
+        if ignore_warnings:
+            args += ['-Wno', ','.join(ignore_warnings)]
+
         try:
             proc_res = run_process(args, logger=_LOGGER, cwd=cwd, check=check)
         except CalledProcessError as err: