Merge remote-tracking branch 'origin/master' into abakst/errno

Author: abakst

chc/app/CExp.py

@@ -730,7 +730,7 @@ def accept(self, visitor: "CVisitor") -> None:
         visitor.visit_startof(self)
 
     def __str__(self) -> str:
-        return "&(" + str(self.lval) + ")"
+        return "&s(" + str(self.lval) + ")"
 
 
 @cdregistry.register_tag("fnapp", CExp)

chc/app/CHVersion.py

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

chc/app/CLval.py

@@ -6,7 +6,7 @@
 #
 # Copyright (c) 2017-2020 Kestrel Technology LLC
 # Copyright (c) 2020-2022 Henny B. Sipma
-# 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
@@ -28,15 +28,15 @@
 # ------------------------------------------------------------------------------
 """Left-hand side value."""
 
-from typing import Dict, List, Tuple, TYPE_CHECKING
+from typing import cast, Dict, List, Tuple, TYPE_CHECKING
 
 from chc.app.CDictionaryRecord import CDictionaryRecord
 
 import chc.util.IndexedTable as IT
 
 if TYPE_CHECKING:
     from chc.app.CDictionary import CDictionary
-    from chc.app.CLHost import CLHost
+    from chc.app.CLHost import CLHost, CLHostMem
     from chc.app.COffset import COffset
     from chc.app.CVisitor import CVisitor
 
@@ -94,4 +94,11 @@ def accept(self, visitor: "CVisitor") -> None:
         visitor.visit_lval(self)
 
     def __str__(self) -> str:
-        return str(self.lhost) + str(self.offset)
+        if self.lhost.is_mem:
+            if self.offset.is_no_offset or self.offset.is_field:
+                return str(self.lhost) + str(self.offset)
+            else:
+                lhost = cast("CLHostMem", self.lhost)
+                return "(" + str(lhost.exp) + ")" + str(self.offset)
+        else:
+            return str(self.lhost) + str(self.offset)

chc/cmdline/AnalysisManager.py

@@ -6,7 +6,7 @@
 #
 # Copyright (c) 2017-2020 Kestrel Technology LLC
 # Copyright (c) 2020-2022 Henny Sipma
-# Copyright (c) 2023-2024 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
@@ -237,7 +237,7 @@ def create_file_primary_proofobligations(
                 print_status(self.targetpath)
                 result = subprocess.call(
                     cmd, cwd=self.targetpath, stderr=subprocess.STDOUT)
-                print("\nResult: " + str(result))
+                print_status("\nResult: " + str(result))
             else:
                 result = subprocess.call(
                     cmd,
@@ -293,7 +293,7 @@ def f(cfile: "CFile") -> None:
             self.capp.iter_files(f)
 
     def _generate_and_check_file_cmd_partial(
-            self, cfilepath: Optional[str], domains: str) -> List[str]:
+            self, cfilepath: Optional[str], domains: str, iteration: int) -> List[str]:
         cmd: List[str] = [
             self.canalyzer,
             "-summaries",
@@ -309,6 +309,7 @@ def _generate_and_check_file_cmd_partial(
         if not (self.contractpath is None):
             cmd.extend(["-contractpath", self.contractpath])
         cmd.extend(["-projectname", self.capp.projectname])
+        cmd.extend(["-iteration", str(iteration)])
         if self.keep_system_includes:
             cmd.append("-keep_system_includes")
         if self.wordsize > 0:
@@ -331,27 +332,28 @@ def generate_and_check_file(
             self,
             cfilename: str,
             cfilepath: Optional[str],
-            domains: str) -> None:
+            domains: str,
+            iteration: int) -> None:
         """Generate invariants and check proof obligations for a single file."""
 
         try:
-            cmd = self._generate_and_check_file_cmd_partial(cfilepath, domains)
+            cmd = self._generate_and_check_file_cmd_partial(cfilepath, domains, iteration)
             cmd.append(cfilename)
             chklogger.logger.info(
                 "Calling AI to generate invariants: %s",
                 " ".join(cmd))
             if self.verbose:
                 result = subprocess.call(
                     cmd, cwd=self.targetpath, stderr=subprocess.STDOUT)
-                print("\nResult: " + str(result))
+                print_status("\nResult: " + str(result))
             else:
                 result = subprocess.call(
                     cmd,
                     cwd=self.targetpath,
                     stdout=open(os.devnull, "w"),
                     stderr=subprocess.STDOUT,
                 )
-                print("\nResult: " + str(result))
+                print_status("\nGenerate-and-check: result: " + str(result))
             if result != 0:
                 chklogger.logger.error(
                     "Error in generating invariants for %s", cfilename)
@@ -361,14 +363,14 @@ def generate_and_check_file(
             print(args)
             exit(1)
 
-    def generate_and_check_app(self, domains: str, processes: int = 1) -> None:
+    def generate_and_check_app(self, domains: str, iteration: int, processes: int = 1) -> None:
         """Generate invariants and check proof obligations for application."""
 
         if processes > 1:
 
             def f(cfile: "CFile") -> None:
                 cmd = self._generate_and_check_file_cmd_partial(
-                    cfile.cfilepath, domains)
+                    cfile.cfilepath, domains, iteration)
                 cmd.append(cfile.cfilename)
                 self._execute_cmd(cmd)
 
@@ -377,7 +379,7 @@ def f(cfile: "CFile") -> None:
 
             def f(cfile: "CFile") -> None:
                 self.generate_and_check_file(
-                    cfile.cfilename, cfile.cfilepath, domains)
+                    cfile.cfilename, cfile.cfilepath, domains, iteration)
 
             self.capp.iter_files(f)
         self.capp.iter_files(self.reset_tables)

chc/cmdline/c_file/cfileutil.py

@@ -569,13 +569,13 @@ def cfile_analyze_file(args: argparse.Namespace) -> NoReturn:
     am.reset_tables(cfile)
     capp.collect_post_assumes()
 
-    am.generate_and_check_file(cfilename, None, analysisdomains)
+    am.generate_and_check_file(cfilename, None, analysisdomains, 0)
     am.reset_tables(cfile)
     capp.collect_post_assumes()
 
     for k in range(5):
         capp.update_spos()
-        am.generate_and_check_file(cfilename, None, analysisdomains)
+        am.generate_and_check_file(cfilename, None, analysisdomains, k + 1)
         am.reset_tables(cfile)
 
     chklogger.logger.info("cfile analyze completed")
@@ -803,13 +803,13 @@ def cfile_run_file(args: argparse.Namespace) -> NoReturn:
     am.reset_tables(cfile)
     capp.collect_post_assumes()
 
-    am.generate_and_check_file(cfilename, None, analysisdomains)
+    am.generate_and_check_file(cfilename, None, analysisdomains, 0)
     am.reset_tables(cfile)
     capp.collect_post_assumes()
 
     for k in range(5):
         capp.update_spos()
-        am.generate_and_check_file(cfilename, None, analysisdomains)
+        am.generate_and_check_file(cfilename, None, analysisdomains, k + 1)
         am.reset_tables(cfile)
 
     chklogger.logger.info("cfile analyze completed")
@@ -1073,13 +1073,13 @@ def cfile_testlibc_summary(args: argparse.Namespace) -> NoReturn:
     am.reset_tables(cfile)
     capp.collect_post_assumes()
 
-    am.generate_and_check_file(cfilename, None, "llrvisp")
+    am.generate_and_check_file(cfilename, None, "llrvisp", 0)
     am.reset_tables(cfile)
     capp.collect_post_assumes()
 
     for k in range(5):
         capp.update_spos()
-        am.generate_and_check_file(cfilename, None, "llrvisp")
+        am.generate_and_check_file(cfilename, None, "llrvisp", k + 1)
         am.reset_tables(cfile)
 
     chklogger.logger.info("cfile analyze completed")

chc/cmdline/c_project/cprojectutil.py

@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2024-2025  Aarno Labs, LLC
+# Copyright (c) 2024-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
@@ -577,7 +577,7 @@ def check_continuation() -> int:
 
         if exitcode == 0:
             for i in range(1):
-                am.generate_and_check_app(analysisdomains, processes=maxprocesses)
+                am.generate_and_check_app(analysisdomains, 0, processes=maxprocesses)
                 capp.reinitialize_tables()
                 capp.update_spos()
 
@@ -586,7 +586,7 @@ def check_continuation() -> int:
         if exitcode == 0:
             for i in range(5):
                 capp.update_spos()
-                am.generate_and_check_app(analysisdomains, processes=maxprocesses)
+                am.generate_and_check_app(analysisdomains, i + 1, processes=maxprocesses)
                 capp.reinitialize_tables()
 
                 exitcode = check_continuation()

chc/cmdline/jsonresultutil.py

@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2024  Aarno Labs LLC
+# Copyright (c) 2024-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
@@ -203,12 +203,12 @@ def ppo_to_json_result(po: "CFunctionPO") -> JSONResult:
     content["predicate"] = str(po.predicate)
     content["context"] = programcontext_to_json_result(po.context).content
     if po.is_closed:
-        content["expl"] = po.explanation
+        content["expl"] = po.explanation_txt
     else:
         if po.has_diagnostic():
-            content["argdiagnostics"] = po.diagnostic.argument_msgs
+            content["argdiagnostics"] = po.diagnostic.argument_msgs_txt
             content["keydiagnostics"] = po.diagnostic.keyword_msgs
-            content["msgdiagnostics"] = po.diagnostic.msgs
+            content["msgdiagnostics"] = po.diagnostic.msgs_txt
     return JSONResult("ppo", content, "ok")
 
 

chc/cmdline/juliet/julietutil.py

@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2024  Aarno Labs, LLC
+# Copyright (c) 2024-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
@@ -381,13 +381,13 @@ def save_xrefs(f: "CFile") -> None:
         exit(1)
 
     for i in range(1):
-        am.generate_and_check_app("llrvisp", processes=jmaxproc)
+        am.generate_and_check_app("llrvisp", 0, processes=jmaxproc)
         capp.reinitialize_tables()
         capp.update_spos()
 
     for i in range(5):
         capp.update_spos()
-        am.generate_and_check_app("llrvisp", processes=jmaxproc)
+        am.generate_and_check_app("llrvisp", i + 1, processes=jmaxproc)
         capp.reinitialize_tables()
 
     def filefilter(filename: str) -> bool:

chc/cmdline/kendra/TestManager.py

@@ -6,7 +6,7 @@
 #
 # Copyright (c) 2017-2020 Kestrel Technology LLC
 # Copyright (c) 2020-2022 Henny B. Sipma
-# Copyright (c) 2023-2024 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
@@ -591,7 +591,7 @@ def test_ppo_proofs(self, delaytest: bool = False) -> None:
                 for d in creffile.domains:
                     am = AnalysisManager(
                         capp, verbose=self.verbose, disable_timing=True)
-                    am.generate_and_check_file(cfilename, None, d)
+                    am.generate_and_check_file(cfilename, None, d, 0)
             cfile.reinitialize_tables()
             ppos = cfile.get_ppos()
             if delaytest:
@@ -672,7 +672,7 @@ def test_spo_proofs(self, delaytest: bool = False) -> None:
                 for d in creffile.domains:
                     am = AnalysisManager(
                         capp, verbose=self.verbose, disable_timing=True)
-                    am.generate_and_check_file(cfilename, None, d)
+                    am.generate_and_check_file(cfilename, None, d, 0)
             cappfile.reinitialize_tables()
             spos = cappfile.get_spos()
             if delaytest:

chc/proof/CFunctionPO.py

@@ -6,7 +6,7 @@
 #
 # Copyright (c) 2017-2020 Kestrel Technology LLC
 # Copyright (c) 2020-2022 Henny B. Sipma
-# Copyright (c) 2023-2024 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
@@ -185,6 +185,16 @@ def has_dependencies(self) -> bool:
     def explanation(self) -> Optional["SituatedMsg"]:
         return self._explanation
 
+    @property
+    def explanation_txt(self) -> Optional[str]:
+        """Returns the text of the explanation message without the additional
+        details."""
+
+        if self.explanation is not None:
+            return self.explanation.msg
+        else:
+            return None
+
     def has_explanation(self) -> bool:
         return self._explanation is not None