Runtests

chc/app/CHVersion.py

@@ -1 +1 @@
-chcversion: str = "0.2.0-2026-02-26"
+chcversion: str = "0.2.0-2026-06-06"

chc/cmdline/AnalysisManager.py

@@ -217,9 +217,18 @@ def create_file_primary_proofobligations(
             self,
             cfilename: str,
             cfilepath: Optional[str] = None,
-            po_cmd: str = "undefined-behavior-primary"
-    ) -> None:
-        """Call analyzer to create primary proof obligations for a single file."""
+            po_cmd: str = "undefined-behavior-primary",
+            return_status: bool = False,
+            chloglevel: str = "WARNING"
+    ) -> int:
+        """Call analyzer to create primary proof obligations for a single file.
+
+        If return_status is False this method exits with 1 if the call to the
+        ocaml analyzer fails. If return_status is True this method always returns
+        the return status of the ocaml analyzer to the caller. The latter is
+        typically used for the regression tests, such that subsequent tests will
+        still be run.
+        """
 
         chklogger.logger.info(
             "Create primiary proof obligations for file %s with path %s",
@@ -230,6 +239,7 @@ def create_file_primary_proofobligations(
             cmd.append(cfilename)
             if cfilepath is not None:
                 cmd.extend(["-cfilepath", cfilepath])
+            cmd.extend(["-loglevel", chloglevel])
             chklogger.logger.info(
                 "Ocaml analyzer is called with %s", str(cmd))
             if self.verbose:
@@ -246,6 +256,8 @@ def create_file_primary_proofobligations(
                 )
             if result != 0:
                 print("Error in creating primary proof obligations")
+                if return_status:
+                    return 1
                 exit(1)
             pcfilename = (
                 cfilename if cfilepath is None
@@ -255,10 +267,14 @@ def create_file_primary_proofobligations(
             cfile.reload_ppos()
             cfile.reload_spos()
         except subprocess.CalledProcessError as args:
+            if return_status:
+                return 1
             print(args.output)
             print(args)
             exit(1)
 
+        return 0
+
     def create_app_primary_proofobligations(
             self,
             po_cmd: str = "undefined-behavior-primary",
@@ -332,12 +348,22 @@ def generate_and_check_file(
             cfilename: str,
             cfilepath: Optional[str],
             domains: str,
-            iteration: int) -> None:
-        """Generate invariants and check proof obligations for a single file."""
+            iteration: int,
+            return_status=False,
+            chloglevel: str = "WARNING") -> int:
+        """Generate invariants and check proof obligations for a single file.
+
+        If return_status is False this method exits with 1 if the call to the
+        ocaml analyzer fails. If return_status is True this method always returns
+        the return status of the ocaml analyzer to the caller. The latter is
+        typically used for the regression tests, such that subsequent tests will
+        still be run.
+"""
 
         try:
             cmd = self._generate_and_check_file_cmd_partial(cfilepath, domains, iteration)
             cmd.append(cfilename)
+            cmd.extend(["-loglevel", chloglevel])
             chklogger.logger.info(
                 "Calling AI to generate invariants: %s",
                 " ".join(cmd))
@@ -354,14 +380,20 @@ def generate_and_check_file(
                 )
                 print_status("\nGenerate-and-check: result: " + str(result))
             if result != 0:
+                if return_status:
+                    return 1
                 chklogger.logger.error(
                     "Error in generating invariants for %s", cfilename)
                 exit(1)
         except subprocess.CalledProcessError as args:
+            if return_status:
+                return 1
             print(args.output)
             print(args)
             exit(1)
 
+        return 0
+
     def generate_and_check_app(self, domains: str, iteration: int, processes: int = 1) -> None:
         """Generate invariants and check proof obligations for application."""
 

chc/cmdline/ParseManager.py

@@ -225,7 +225,9 @@ def preprocess_file_with_cc(
             self,
             cfilename: str,
             copyfiles: bool = True,
-            moreoptions: List[str] = []) -> str:
+            moreoptions: List[str] = [],
+            chloglevel: str = "WARNING"
+    ) -> str:
         """Invoke C preprocessor on c source file.
 
         Args:
@@ -518,7 +520,7 @@ def parse_cfiles(self, copyfiles: bool = True) -> None:
                     targetfiles.add_file(self.normalize_filename(fname))
         targetfiles.save_xml_file(self.analysisresultspath)
 
-    def parse_ifile(self, ifilename: str) -> int:
+    def parse_ifile(self, ifilename: str, chloglevel: str = "WARNING") -> int:
         """Invoke the CodeHawk C parser frontend on preprocessed source file
 
         Args:
@@ -539,6 +541,7 @@ def parse_ifile(self, ifilename: str) -> int:
         ]
         if not self.keep_system_includes:
             cmd.append("-keep_system_includes")
+        cmd.extend(["-loglevel", chloglevel])
         if self.keepUnused:
             cmd.append("-keepUnused")
         cmd.append(ifilename)

chc/cmdline/chkc

@@ -5,7 +5,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2023-2025  Aarno Labs, LLC
+# Copyright (c) 2023-2026  Aarno Labs, LLC
 #
 # Permission is hereby granted, free of charge, to any person obtaining a copy
 # of this software and associated documentation files (the "Software"), to deal
@@ -64,6 +64,7 @@ import chc.cmdline.c_file.cfiletableutil as CT
 import chc.cmdline.c_project.cprojectutil as P
 import chc.cmdline.juliet.julietutil as J
 import chc.cmdline.kendra.kendrautil as K
+import chc.cmdline.regression.regressionutil as R
 
 from chc.util.Config import Config
 import chc.util.loggingutil as UL
@@ -418,6 +419,30 @@ def parse() -> argparse.Namespace:
         help="name of table")
     kendrashowfunctiontable.set_defaults(func=K.kendra_show_function_table)
 
+    # ----------------------------------------------------- regression tests ---
+
+    regressioncmd = subparsers.add_parser("regression")
+    regressionparsers = regressioncmd.add_subparsers(title="show options")
+
+    # --- regression list
+    regressionlist = regressionparsers.add_parser("list")
+    regressionlist.set_defaults(func=R.regression_list)
+
+    # --- regression test-file
+    regressiontestfile = regressionparsers.add_parser("test-file")
+    regressiontestfile.add_argument(
+        "cfilename", help="name of testfile to run (e.g., bool_integer_promotion.c)")
+    regressiontestfile.set_defaults(func=R.regression_test_file)
+
+    # --- regressions run-tests
+    regressionruntests = regressionparsers.add_parser("run-tests")
+    regressionruntests.add_argument(
+        "--loglevel", "-log",
+        choices=UL.LogLevel.options(),
+        default="WARNING",
+        help="activate logging in CHC with given level")
+    regressionruntests.set_defaults(func=R.regression_run_tests)
+
     # --------------------------------------------------------------- juliet ---
 
     julietcmd = subparsers.add_parser("juliet")

chc/cmdline/regression/__init__.py

@@ -0,0 +1 @@
+"""Support for analyzing the kendra (regression) tests."""