API: remove candidate contract

Author: sipma

chc/api/ApiAssumption.py

@@ -5,8 +5,8 @@
 # The MIT License (MIT)
 #
 # Copyright (c) 2017-2020 Kestrel Technology LLC
-# Copyright (c) 2021-2022 Henny Sipma
-# Copyright (c) 2023      Aarno Labs LLC
+# Copyright (c) 2021-2022 Henny B. Sipma
+# Copyright (c) 2023-2024 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
@@ -26,6 +26,9 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 # ------------------------------------------------------------------------------
+"""Assumption on the function api.
+
+"""
 
 from typing import List, TYPE_CHECKING
 
@@ -36,6 +39,19 @@
 
 
 class ApiAssumption:
+    """Assumption on the function api.
+
+    Args:
+        capi (CFunctionApi): parent function api
+        id (int): identification number
+        predicate (CPOPredicate): expression of the assumption
+        ppos (List[int]): list of primary proof obligation id's that depend on
+           this assumption
+        spos (List[int]): list of supporting proof obligation id's that depend
+           on this assumption
+        isglobal (bool=False): assumption holds globally
+        isfile (bool=False): assumption holds for the entire c-file
+    """
 
     def __init__(
         self,

chc/api/ApiParameter.py

@@ -26,15 +26,7 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 # ------------------------------------------------------------------------------
-"""Object representation of api_parameter_t
-
-cchlib/CCHLibTypes.api_parameter_t =      predicate       properties
-                               -------------------------------------------------
-type api_parameter_t =
-  | ParFormal of int                      is_formal       index: int
-  | ParGlobal of string                   is_global       name: str
-
-"""
+"""Object representation of api_parameter_t"""
 
 from typing import List, TYPE_CHECKING
 
@@ -48,6 +40,13 @@
 
 
 class ApiParameter(InterfaceDictionaryRecord):
+    """Base class of formal parameter of a function.
+
+    Args:
+        cd (InterfaceDictionary): The parent dictionary to resolve
+            subexpressions
+        ixval (IndexedTableValue): The backing record of the value
+    """
 
     def __init__(
         self, cd: "InterfaceDictionary", ixval: IT.IndexedTableValue) -> None:
@@ -69,7 +68,7 @@ def __str__(self) -> str:
 class APFormal(ApiParameter):
     """Formal parameter of a function.
 
-    args[0]: parameter index (starting at 1)
+    * args[0]: parameter index (starting at 1)
     """
 
     def __init__(
@@ -90,6 +89,7 @@ def __str__(self) -> str:
 
 @ifdregistry.register_tag("pg", ApiParameter)
 class APGlobal(ApiParameter):
+    """Global variable used in a function; treated as a formal parameter."""
 
     def __init__(
         self, cd: "InterfaceDictionary", ixval: IT.IndexedTableValue) -> None:

chc/api/CFileCandidateContracts.py

@@ -5,8 +5,8 @@
 # The MIT License (MIT)
 #
 # Copyright (c) 2017-2020 Kestrel Technology LLC
-# Copyright (c) 2020-2022 Henny Sipma
-# Copyright (c) 2023      Aarno Labs LLC
+# Copyright (c) 2020-2022 Henny B. Sipma
+# Copyright (c) 2023-2024 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
@@ -26,12 +26,14 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 # ------------------------------------------------------------------------------
+"""User-provided contracts for variables and functions in a c-file."""
 
 import xml.etree.ElementTree as ET
 
 from typing import Callable, Dict, List, Optional, TYPE_CHECKING
 
 import chc.util.fileutil as UF
+from chc.util.loggingutil import chklogger
 
 from chc.api.CFunctionContract import CFunctionContract
 
@@ -64,10 +66,10 @@ class CFileContracts:
     def __init__(self, cfile: "CFile", contractpath: str) -> None:
         self._cfile = cfile
         self._contractpath = contractpath
-        self.xnode = UF.get_contracts(self._contractpath, self._cfile.name)
+        # self.xnode = UF.get_contracts(self._contractpath, self._cfile.name)
         self._functions: Dict[str, CFunctionContract] = {}
         self._globalvariables: Dict[str, CFileContractGlobalVar] = {}
-        self._initialize(self.xnode)
+        self._initialize()
 
     @property
     def cfile(self) -> "CFile":
@@ -92,6 +94,8 @@ def function_contract(self, name: str) -> CFunctionContract:
             raise UF.CHCError("No function contract found for " + name)
 
     def has_function_contract(self, name: str) -> bool:
+        """Returns true if this contract contains a function contract for name."""
+
         return name in self.functions
 
     def has_assertions(self) -> bool:
@@ -152,7 +156,8 @@ def __str__(self) -> str:
             lines.append("-" * 80)
         return "\n".join(lines)
 
-    def _initialize(self, xnode: Optional[ET.Element]) -> None:
+    def _initialize(self) -> None:
+        xnode = UF.get_contracts(self.contractpath, self.cfile.name)
         if xnode is None:
             return
         gvnode = xnode.find("global-variables")
@@ -161,7 +166,7 @@ def _initialize(self, xnode: Optional[ET.Element]) -> None:
                 name = gnode.get("name")
                 if name is None:
                     raise UF.CHCError("No name specified for global variable")
-                gvinfo = self.cfile.declarations.get_global_varinfo_by_name(name)
+                gvinfo = self.cfile.get_global_varinfo_by_name(name)
                 gconst = "const" in gnode.attrib and gnode.get("const") == "yes"
                 gval = gnode.get("value")
                 gvalue = int(gval) if gval else None
@@ -172,4 +177,5 @@ def _initialize(self, xnode: Optional[ET.Element]) -> None:
         if ffnode is not None:
             for fnode in ffnode.findall("function"):
                 fn = CFunctionContract(self, fnode)
+                chklogger.logger.info("Function contract found for %s", fn.name)
                 self._functions[fn.name] = fn

chc/api/CFileContracts.py

@@ -5,8 +5,8 @@
 # The MIT License (MIT)
 #
 # Copyright (c) 2017-2020 Kestrel Technology LLC
-# Copyright (c) 2020-2022 Henny Sipma
-# Copyright (c) 2023      Aarno Labs LLC
+# Copyright (c) 2020-2022 Henny B. Sipma
+# Copyright (c) 2023-2024 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
@@ -29,7 +29,7 @@
 
 import xml.etree.ElementTree as ET
 
-from typing import Callable, Dict, List, Optional, Tuple, TYPE_CHECKING
+from typing import Callable, cast, Dict, List, Optional, Tuple, TYPE_CHECKING
 
 from chc.api.ApiAssumption import ApiAssumption
 from chc.api.ContractAssumption import ContractAssumption
@@ -44,7 +44,7 @@
     from chc.api.XPredicate import XPredicate
     from chc.app.CApplication import CApplication
     from chc.app.CFile import CFile
-    from chc.app.CTyp import CFunArg
+    from chc.app.CTyp import CFunArg, CTypFun
     from chc.app.CFunction import CFunction
 
 memory_free_functions = ["free", "realloc"]
@@ -187,7 +187,7 @@ def global_assumption_requests(self) -> Dict[int, GlobalAssumption]:
                             self.xmsg(
                                 "ipr attribute missing in global-assumption-requests"))
                     id = int(xid)
-                    p = self.cfile.predicatedictionary.get_predicate(id)
+                    p = self.cfile.interfacedictionary.get_xpredicate(id)
                     ppos = IT.get_attribute_int_list(x, "ppos")
                     spos = IT.get_attribute_int_list(x, "spos")
                     gas = GlobalAssumption(self, id, p, ppos, spos)
@@ -226,7 +226,11 @@ def contract_condition_failures(self) -> List[Tuple[str, str]]:
 
     @property
     def parameters(self) -> List["CFunArg"]:
-        return self.cfun.ftype.funargs.arguments
+        ftype = cast("CTypFun", self.cfun.ftype)
+        if ftype.funargs is not None:
+            return ftype.funargs.arguments
+        else:
+            raise UF.CHCError("Function signature without parameters")
         # return self.cfun.ftype.get_args().get_args()
 
     @property