Attributes

chb/api/AppFunctionSemantics.py

@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2023  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
@@ -35,6 +35,7 @@
 from chb.util.IndexedTable import IndexedTableValue
 
 if TYPE_CHECKING:
+    from chb.api.FunctionQualifiers import FunctionQualifiers
     from chb.api.InterfaceDictionary import InterfaceDictionary
     from chb.api.XXPredicate import XXPredicate
 
@@ -46,6 +47,8 @@ class AppFunctionSemantics(InterfaceDictionaryRecord):
     args[1]: index of postcondition list in interfacedictionary
     args[2]: index of error-postcondition list in interfacedictionary
     args[3]: index of side-effect list in interfacedictionary
+    args[4]: index of post requests in interfacedictionary
+    args[5]: index of function-qualifiers in interfacedictionary
     """
 
     def __init__(
@@ -68,6 +71,14 @@ def errorpostcondition_list(self) -> List["XXPredicate"]:
     def sideeffect_list(self) -> List["XXPredicate"]:
         return self.id.xpredicate_list(self.args[3])
 
+    @property
+    def postrequest_list(self) -> List["XXPredicate"]:
+        return self.id.xpredicate_list(self.args[4])
+
+    @property
+    def qualifiers(self) -> "FunctionQualifiers":
+        return self.id.function_qualifiers(self.args[5])
+
     def __str__(self) -> str:
         lines: List[str] = []
         if len(self.precondition_list) > 0:
@@ -86,4 +97,5 @@ def __str__(self) -> str:
             lines.append("Side-effects")
             for p in self.sideeffect_list:
                 lines.append("  " + str(p))
+        lines.append("Qualifiers: " + str(self.qualifiers))
         return "\n".join(lines)

chb/api/AppFunctionSignature.py

@@ -67,6 +67,10 @@ def calling_convention(self) -> str:
     def parameter_list(self) -> List["FtsParameter"]:
         return self.id.fts_parameter_list(self.args[0])
 
+    @property
+    def is_vararg(self) -> bool:
+        return self.args[1] == 1
+
     @property
     def returntype(self) -> "BCTyp":
         return self.bcd.typ(self.args[3])

chb/api/FunctionQualifiers.py

@@ -0,0 +1,88 @@
+# ------------------------------------------------------------------------------
+# CodeHawk Binary Analyzer
+# Author: Henny Sipma
+# ------------------------------------------------------------------------------
+# The MIT License (MIT)
+#
+# 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
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+# ------------------------------------------------------------------------------
+
+
+from typing import List, Optional, TYPE_CHECKING
+
+from chb.api.InterfaceDictionaryRecord import InterfaceDictionaryRecord
+
+import chb.util.fileutil as UF
+
+from chb.util.IndexedTable import IndexedTableValue
+
+if TYPE_CHECKING:
+    from chb.api.InterfaceDictionary import InterfaceDictionary
+    from chb.api.XXPredicate import XXPredicate
+
+
+class FunctionQualifiers(InterfaceDictionaryRecord):
+
+    def __init__(
+            self, ixd: "InterfaceDictionary", ixval: IndexedTableValue) -> None:
+        InterfaceDictionaryRecord.__init__(self, ixd, ixval)
+
+    def _optional_bool(self, index: int) -> Optional[bool]:
+        r = self.args[index]
+        if r == 2:
+            return True
+        elif r == 1:
+            return False
+        else:
+            return None
+
+    @property
+    def fq_noreturn(self) -> Optional[bool]:
+        return self._optional_bool(0)
+
+    @property
+    def fq_functional(self) -> Optional[str]:
+        r = self.args[1]
+        if r == 2:
+            return "FConst"
+        elif r == 1:
+            return "FPure"
+        else:
+            return None
+
+    @property
+    def fq_sets_errno(self) -> Optional[bool]:
+        return self._optional_bool(2)
+
+    @property
+    def fq_must_use_return(self) -> Optional[bool]:
+        return self._optional_bool(3)
+
+    def __str__(self) -> str:
+        return (
+            ("fq_noreturn: " + str(self.fq_noreturn) + "; "
+             if self.fq_noreturn is not None else "")
+            + ("fq_functional: " + str(self.fq_functional) + "; "
+               if self.fq_functional is not None else "")
+            + ("fq_sets_errno: " + str(self.fq_sets_errno) + "; "
+               if self.fq_sets_errno is not None else "")
+            + ("fq_must_use_return: " + str(self.fq_must_use_return) + ";"
+               if self.fq_must_use_return is not None else ""))

chb/api/InterfaceDictionary.py

@@ -40,6 +40,7 @@
 from chb.api.AppFunctionSignature import AppFunctionSignature
 from chb.api.CallTarget import CallTarget
 from chb.api.FunctionStub import FunctionStub
+from chb.api.FunctionQualifiers import FunctionQualifiers
 from chb.api.XXPredicate import XXPredicate
 
 from chb.api.InterfaceDictionaryRecord import apiregistry
@@ -67,6 +68,7 @@ def __init__(
             IT.IndexedTable("parameter-location-list-table"))
         self.fts_parameter_list_table = IT.IndexedTable("fts-parameter-list-table")
         self.fts_parameter_table = IT.IndexedTable("fts-parameter-table")
+        self.function_qualifiers_table = IT.IndexedTable("function-qualifiers-table")
         self.function_interface_table = IT.IndexedTable("function-interface-table")
         self.function_semantics_table = IT.IndexedTable("function-semantics-table")
         self.function_signature_table = IT.IndexedTable("function-signature-table")
@@ -78,6 +80,7 @@ def __init__(
             self.parameter_location_list_table,
             self.function_stub_table,
             self.call_target_table,
+            self.function_qualifiers_table,
             self.function_interface_table,
             self.function_semantics_table,
             self.function_signature_table,
@@ -119,6 +122,10 @@ def call_target(self, ix: int) -> CallTarget:
         return apiregistry.mk_instance(
             self, self.call_target_table.retrieve(ix), CallTarget)
 
+    def function_qualifiers(self, ix: int) -> FunctionQualifiers:
+        return FunctionQualifiers(
+            self, self.function_qualifiers_table.retrieve(ix))
+
     def function_interface(self, ix: int) -> AppFunctionInterface:
         return AppFunctionInterface(
             self, self.function_interface_table.retrieve(ix))

chb/api/XXPredicate.py

@@ -65,10 +65,6 @@ def is_xp_buffer(self) -> bool:
     def is_xp_enum(self) -> bool:
         return False
 
-    @property
-    def is_xp_constant_false(self) -> bool:
-        return False
-
     @property
     def is_xp_freed(self) -> bool:
         return False
@@ -157,10 +153,6 @@ def is_xp_relational_expr(self) -> bool:
     def is_xp_sets_errno(self) -> bool:
         return False
 
-    @property
-    def is_xp_starts_thread(self) -> bool:
-        return False
-
     @property
     def is_xp_tainted(self) -> bool:
         return False
@@ -341,22 +333,6 @@ def __str__(self) -> str:
             + ")")
 
 
-@apiregistry.register_tag("f", XXPredicate)
-class XXPFalse(XXPredicate):
-    """Constant false predicate."""
-
-    def __init__(
-            self, ixd: "InterfaceDictionary", ixval: IndexedTableValue) -> None:
-        XXPredicate.__init__(self, ixd, ixval)
-
-    @property
-    def is_xp_constant_false(self) -> bool:
-        return True
-
-    def __str__(self) -> str:
-        return "false"
-
-
 @apiregistry.register_tag("fr", XXPredicate)
 class XXPFreed(XXPredicate):
     """Pointer to memory region has been freed.
@@ -380,22 +356,6 @@ def __str__(self) -> str:
         return "freed(" + str(self.pointer) + ")"
 
 
-@apiregistry.register_tag("fn", XXPredicate)
-class XXPFunctional(XXPredicate):
-    """Function has no side effects."""
-
-    def __init__(
-            self, ixd: "InterfaceDictionary", ixval: IndexedTableValue) -> None:
-        XXPredicate.__init__(self, ixd, ixval)
-
-    @property
-    def is_xp_functional(self) -> bool:
-        return True
-
-    def __str__(self) -> str:
-        return "functional"
-
-
 @apiregistry.register_tag("fp", XXPredicate)
 class XXPFunctionPointer(XXPredicate):
     """Term is address of a function.
@@ -878,22 +838,6 @@ def __str__(self) -> str:
             + str(self.term2))
 
 
-@apiregistry.register_tag("errno", XXPredicate)
-class XXPSetsErrno(XXPredicate):
-    """Function sets errno."""
-
-    def __init__(
-            self, ixd: "InterfaceDictionary", ixval: IndexedTableValue) -> None:
-        XXPredicate.__init__(self, ixd, ixval)
-
-    @property
-    def is_xp_sets_errno(self) -> bool:
-        return True
-
-    def __str__(self) -> str:
-        return "sets-errno"
-
-
 @apiregistry.register_tag("st", XXPredicate)
 class XXPStartsThread(XXPredicate):
     """Starts thread indicated by pointer with given arguments.

chb/app/CHVersion.py

@@ -1,3 +1,3 @@
-chbversion: str = "0.3.0-20260603"
+chbversion: str = "0.3.0-20260611"
 
-minimum_required_chb_version = "0.6.0_20260527"
+minimum_required_chb_version = "0.6.0_20260611"

chb/app/FnProofObligations.py

@@ -159,6 +159,7 @@ def __str__(self) -> str:
             + str(self.xpo)
             + " ("
             + str(self.status)
+            + m
             + ")")
 
 
@@ -192,7 +193,7 @@ def proofobligations(self) -> Dict[str, List[ProofObligation]]:
                         xstatus = xxpo.find("status")
                         if xstatus is not None:
                             status = POStatus(self.xpod, xstatus)
-                            msg = xxpo.get("m", "none")
+                            msg = xstatus.get("m", "none")
                             po = ProofObligation(iaddr, xpo, status, msg)
                             self._store[iaddr].append(po)
         return self._store