Parsing

chc/app/CAttributes.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-2025 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
@@ -40,6 +40,7 @@
     from chc.app.CDictionary import CDictionary
     from chc.app.CTyp import CTyp
     from chc.app.CTypsig import CTypsig
+    from chc.app.CVisitor import CVisitor
 
 
 class CAttr(CDictionaryRecord):
@@ -557,5 +558,8 @@ def attributes(self) -> List[CAttribute]:
     def length(self) -> int:
         return len(self.attributes)
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_attributes(self)
+
     def __str__(self) -> str:
         return ",".join([str(p) for p in self.attributes])

chc/app/CExp.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-2025 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
@@ -39,6 +39,7 @@
     from chc.app.CConst import CConst
     from chc.app.CTyp import CTyp
     from chc.app.CLval import CLval
+    from chc.app.CVisitor import CVisitor
 
 
 binoperatorstrings = {
@@ -147,6 +148,9 @@ def get_strings(self) -> List[str]:
     def get_variable_uses(self, vid: int) -> int:
         return 0
 
+    def accept(self, visitor: "CVisitor") -> None:
+        raise Exception("CExp.accept: " + str(self))
+
     def to_dict(self) -> Dict[str, Any]:
         return {"base": "exp"}
 
@@ -179,6 +183,9 @@ def constant(self) -> "CConst":
     def get_strings(self) -> List[str]:
         return self.constant.get_strings()
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_constexp(self)
+
     def to_dict(self) -> Dict[str, Any]:
         return {"base": "const", "value": str(self.constant)}
 

chc/app/CFile.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-2025 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
@@ -51,6 +51,7 @@
 from chc.app.CFileGlobals import CGVarDecl
 from chc.app.CFileGlobals import CGVarDef
 from chc.app.CGXrefs import CGXrefs
+from chc.app.CPrettyPrinter import CPrettyPrinter
 
 from chc.proof.CFilePredicateDictionary import CFilePredicateDictionary
 from chc.proof.CFunctionPO import CFunctionPO
@@ -183,6 +184,36 @@ def cfileglobals(self) -> CFileGlobals:
     def gfunctions(self) -> Dict[int, "CGFunction"]:
         return self.cfileglobals.gfunctions
 
+    def header_declarations(
+            self,
+            gvarnames: Dict[str, str] = {},
+            fnnames: Dict[str, str] = {}) -> str:
+        lines: List[str] = []
+        srcfilename = self.name + ".c"
+        lines.append("// " + srcfilename + "\n")
+        gvars = self.gvardefs.values()
+        if len(gvars) > 0:
+            lines.append("// static and global variable definitions\n")
+        for gvar in gvars:
+            pp = CPrettyPrinter()
+            binloc: Optional[str] = gvarnames.get(gvar.varinfo.vname)
+            gvardef = pp.gvar_definition_str(
+                gvar.varinfo, srcloc=srcfilename, binloc=binloc)
+            lines.append(gvardef)
+
+        fns = self.gfunctions.values()
+        if len(gvars) > 0 and len(fns) > 0:
+            lines.append("// function signatures\n")
+        for fn in fns:
+            if fn.is_system_function:
+                continue
+            pp = CPrettyPrinter()
+            binloc = fnnames.get(fn.varinfo.vname)
+            fndecl = pp.function_declaration_str(
+                fn.varinfo, srcloc=srcfilename, binloc=binloc)
+            lines.append(fndecl)
+        return "\n".join(lines)
+
     @property
     def functioncount(self) -> int:
         return self.cfileglobals.functioncount

chc/app/CFileGlobals.py

@@ -6,7 +6,7 @@
 #
 # Copyright (c) 2017-2020 Kestrel Technology LLC
 # Copyright (c) 2020-2023 Henny B. Sipma
-# Copyright (c) 2024      Aarno Labs LLC
+# Copyright (c) 2024-2025 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
@@ -105,6 +105,11 @@ def vtype(self) -> "CTyp":
     def line(self) -> int:
         return self.varinfo.line
 
+    @property
+    def is_system_function(self) -> bool:
+        vdecl = self.varinfo.vdecl
+        return vdecl is None or vdecl.file.startswith("/")
+
     def __str__(self) -> str:
         return f"{self.vname}: {self.vtype}"