diff --git a/chc/app/CAttributes.py b/chc/app/CAttributes.py
index 2a72e62..891b406 100644
--- a/chc/app/CAttributes.py
+++ b/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])
diff --git a/chc/app/CExp.py b/chc/app/CExp.py
index 6c26089..3c0a3ee 100644
--- a/chc/app/CExp.py
+++ b/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)}
 
diff --git a/chc/app/CFile.py b/chc/app/CFile.py
index b154cb9..4a4e0a0 100644
--- a/chc/app/CFile.py
+++ b/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
diff --git a/chc/app/CFileGlobals.py b/chc/app/CFileGlobals.py
index c352ae2..a908803 100644
--- a/chc/app/CFileGlobals.py
+++ b/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}"
 
diff --git a/chc/app/CPrettyPrinter.py b/chc/app/CPrettyPrinter.py
new file mode 100644
index 0000000..d74f4df
--- /dev/null
+++ b/chc/app/CPrettyPrinter.py
@@ -0,0 +1,367 @@
+# ------------------------------------------------------------------------------
+# CodeHawk C Analyzer
+# Author: Henny Sipma
+# ------------------------------------------------------------------------------
+# The MIT License (MIT)
+#
+# Copyright (c) 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
+# 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 cast, List, Optional, TYPE_CHECKING
+
+import chc.app.CAttributes as CA
+import chc.app.CExp as CE
+import chc.app.CTyp as CT
+from chc.app.CVarInfo import CVarInfo
+
+from chc.app.CVisitor import CVisitor
+
+
+integernames = {
+    "ichar": "char",
+    "ischar": "signed char",
+    "iuchar": "unsigned char",
+    "ibool": "bool",
+    "iint": "int",
+    "iuint": "unsigned int",
+    "ishort": "short",
+    "iushort": "unsigned short",
+    "ilong": "long",
+    "iulong": "unsigned long",
+    "ilonglong": "long long",
+    "iulonglong": "unsigned long long",
+}
+
+floatnames = {"float": "float", "fdouble": "double", "flongdouble": "long double"}
+
+
+class CPrettyCode:
+
+    def __init__(self) -> None:
+        self._outputlines: List[str] = []
+        self._pos: int = 0
+
+    @property
+    def outputlines(self) -> List[str]:
+        return self._outputlines
+
+    @property
+    def pos(self) -> int:
+        return self._pos
+
+    def newline(self, indent: int = 0) -> None:
+        self._outputlines.append(" " * indent)
+        self._pos = indent
+
+    def write(self, s: str) -> None:
+        self._outputlines[-1] += s
+        self._pos += len(s)
+
+    def __str__(self) -> str:
+        return "\n".join(self.outputlines)
+
+
+class CPrettyPrinter(CVisitor):
+
+    def __init__(self, indentation: int = 2) -> None:
+        self._indentation = indentation
+        self._indent = 0
+        self._ccode = CPrettyCode()
+
+    @property
+    def indentation(self) -> int:
+        return self._indentation
+
+    @property
+    def indent(self) -> int:
+        return self._indent
+
+    @property
+    def ccode(self) -> CPrettyCode:
+        return self._ccode
+
+    def increase_indent(self) -> None:
+        self._indent += self.indentation
+
+    def decrease_indent(self) -> None:
+        self._indent -= self.indentation
+
+    def visit_voidtyp(self, t: CT.CTypVoid) -> None:
+        t.attributes.accept(self)
+        self.ccode.write("void")
+
+    def visit_inttyp(self, t: CT.CTypInt) -> None:
+        t.attributes.accept(self)
+        self.ccode.write(integernames[t.ikind])
+
+    def visit_floattyp(self, t: CT.CTypFloat) -> None:
+        t.attributes.accept(self)
+        self.ccode.write(str(t))
+
+    def visit_namedtyp(self, t: CT.CTypNamed) -> None:
+        t.attributes.accept(self)
+        t.expand().accept(self)
+
+    def visit_comptyp(self, t: CT.CTypComp) -> None:
+        t.attributes.accept(self)
+        if t.is_comp:
+            self.ccode.write("struct " + self.de_anon_name(t.name))
+        else:
+            self.ccode.write("union " + self.de_anon_name(t.name))
+
+    def de_anon_name(self, name: str) -> str:
+        if name.startswith("__anonstruct_") and len(name) > 24:
+            return name[13:-10] + "st"
+        else:
+            return name
+
+    def visit_enumtyp(self, t: CT.CTypEnum) -> None:
+        t.attributes.accept(self)
+        self.ccode.write("enum " + t.name)
+
+    def visit_builtinvaargs(self, t: CT.CTypBuiltinVaargs) -> None:
+        pass
+
+    def visit_ptrtyp(self, t: CT.CTypPtr) -> None:
+        t.attributes.accept(self)
+        t.pointedto_type.accept(self)
+        self.ccode.write(" *")
+
+    def visit_arraytyp(self, t: CT.CTypArray) -> None:
+        t.array_basetype.accept(self)
+        self.ccode.write("[")
+        if t.array_size_expr is not None:
+            # self.ccode.write("?")
+            t.array_size_expr.accept(self)
+        self.ccode.write("]")
+
+    def visit_funtyp(self, t: CT.CTypFun) -> None:
+        """Emits a function type without name."""
+
+        t.return_type.accept(self)
+        self.ccode.write(" (")
+        if t.funargs is not None:
+            t.funargs.accept(self)
+        self.ccode.write(")")
+
+    def write_chkx_srcloc_attribute(
+            self, srcfile: str, line: int, binloc: Optional[str]) -> None:
+        self.ccode.newline(indent=3)
+        self.ccode.write("__attribute__ (( chkc_srcloc(")
+        self.ccode.write('"')
+        self.ccode.write(srcfile)
+        self.ccode.write('"')
+        self.ccode.write(",")
+        self.ccode.write(str(line))
+        self.ccode.write(")")
+        if binloc is not None:
+            self.ccode.write(", chkx_binloc(")
+            self.ccode.write('"')
+            self.ccode.write(binloc)
+            self.ccode.write('"')
+            self.ccode.write(")")
+        self.ccode.write(" ))")
+
+    def gvar_definition_str(
+            self,
+            vinfo: CVarInfo,
+            srcloc: Optional[str] = None,
+            binloc: Optional[str] = None) -> str:
+        if vinfo.vtype.is_function:
+            return "error"
+
+        if vinfo.vtype.is_array:
+            sizexps: List[Optional[CE.CExp]] = []
+            self.ccode.newline()
+            atype = cast(CT.CTypArray, vinfo.vtype)
+            sizexps.append(atype.array_size_expr)
+            basetype = atype.array_basetype
+            while basetype.is_array:
+                atype = cast(CT.CTypArray, basetype)
+                sizexps.append(atype.array_size_expr)
+                basetype = atype.array_basetype
+            basetype.accept(self)
+            self.ccode.write(" ")
+            self.ccode.write(vinfo.vname)
+            for s in sizexps:
+                self.ccode.write("[")
+                if s:
+                    s.accept(self)
+                self.ccode.write("]")
+            self.ccode.write(";")
+            self.ccode.newline()
+            return str(self.ccode)
+
+        self.ccode.newline()
+        vinfo.vtype.accept(self)
+        self.ccode.write(" ")
+        self.ccode.write(vinfo.vname)
+        if srcloc is not None:
+            self.write_chkx_srcloc_attribute(srcloc, vinfo.line, binloc)
+        self.ccode.write(";")
+        self.ccode.newline()
+        return str(self.ccode)
+
+    def function_declaration_str(
+            self,
+            vinfo: CVarInfo,
+            srcloc: Optional[str] = None,
+            binloc: Optional[str] = None) -> str:
+        if not vinfo.vtype.is_function:
+            return "error"
+
+        self.ccode.newline()
+        ftype = cast(CT.CTypFun, vinfo.vtype)
+        if ftype.return_type.is_function_pointer:
+            returntyp = cast(CT.CTypPtr, ftype.return_type)
+            retfntyp = cast(CT.CTypFun, returntyp.pointedto_type)
+            retfntyp.return_type.accept(self)
+            self.ccode.write(" (*")
+            self.ccode.write(vinfo.vname)
+            self.ccode.write("(")
+            if ftype.funargs is not None:
+                ftype.funargs.accept(self)
+            self.ccode.write("))(")
+            if retfntyp.funargs is not None:
+                retfntyp.funargs.accept(self)
+            self.ccode.write(")")
+            if srcloc is not None:
+                self.write_chkx_srcloc_attribute(srcloc, vinfo.line, binloc)
+            self.ccode.write(";")
+            self.ccode.newline()
+            return str(self.ccode)
+
+        else:
+            ftype.return_type.accept(self)
+            self.ccode.write(" ")
+            self.ccode.write(vinfo.vname)
+        self.ccode.write("(")
+        if ftype.funargs is not None:
+            ftype.funargs.accept(self)
+        if ftype.is_vararg:
+            self.ccode.write(", ...")
+        self.ccode.write(")")
+        if srcloc is not None:
+            self.write_chkx_srcloc_attribute(srcloc, vinfo.line, binloc)
+        self.ccode.write(";")
+        self.ccode.newline()
+        return str(self.ccode)
+
+    def funtypptr_with_name(self, t: CT.CTypFun, name: str) -> None:
+        if t.return_type.is_function_pointer:
+            returntyp = cast(CT.CTypPtr, t.return_type)
+            retty = cast(CT.CTypFun, returntyp.pointedto_type)
+            self.funtypptr_with_name(retty, name)
+            self.ccode.write("(")
+            if t.funargs is not None:
+                t.funargs.accept(self)
+            self.ccode.write(")")
+        else:
+            t.return_type.accept(self)
+            self.ccode.write(" (*")
+            self.ccode.write(name)
+            self.ccode.write(")(")
+            if t.funargs is not None:
+                t.funargs.accept(self)
+            self.ccode.write(")")
+
+    def visit_funargs(self, funargs: CT.CFunArgs) -> None:
+        args = funargs.arguments
+        if len(args) == 0:
+            self.ccode.write("void")
+        else:
+            for arg in args[:-1]:
+                arg.accept(self)
+                self.ccode.write(", ")
+            args[-1].accept(self)
+
+    def visit_funarg(self, funarg: CT.CFunArg) -> None:
+        if funarg.typ.is_function_pointer:
+            argtyp = cast(CT.CTypPtr, funarg.typ)
+            fnptr = cast(CT.CTypFun, argtyp.pointedto_type)
+            self.funtypptr_with_name(fnptr, funarg.name)
+            return
+
+        if funarg.typ.is_pointer:
+            argtyp = cast(CT.CTypPtr, funarg.typ)
+            ptargtyp = argtyp.pointedto_type
+            if ptargtyp.is_named_type:
+                ptx = cast(CT.CTypNamed, ptargtyp).expand()
+                if ptx.is_function:
+                    ptx = cast(CT.CTypFun, ptx)
+                    self.funtypptr_with_name(ptx, funarg.name)
+                    return
+
+            if (
+                    argtyp.attributes.length > 0
+                    and argtyp.attributes.attributes[0].name == "arraylen"):
+                self.ptrarg_with_attribute_length(
+                    ptargtyp, argtyp.attributes.attributes[0], funarg.name)
+                return
+
+        funarg.typ.accept(self)
+        self.ccode.write(" ")
+        self.ccode.write(funarg.name)
+
+    def ptrarg_with_attribute_length(
+            self, t: CT.CTyp, a: CA.CAttribute, name: str) -> None:
+        """retrieve arraylength from arraylen attribute.
+
+        In C arrays passed as arguments to functions become pointers,
+        that is, the function call:
+
+        f(int a[20]);
+
+        is compiled into
+
+        f(int *a);
+
+        It appears that CIL in this case records the length in an
+        attribute with the name arraylen.
+        """
+        if not a.name == "arraylen":
+            raise Exception("Not an arraylen attribute")
+        if not (len(a.params) == 1):
+            raise Exception("Expected one argument for arraylen")
+        aparam = a.params[0]
+        if not aparam.is_int:
+            raise Exception("Expected an integer argument for arraylen")
+        aparam = cast(CA.CAttrInt, aparam)
+
+        t.accept(self)
+        self.ccode.write(" ")
+        self.ccode.write(name)
+        self.ccode.write("[")
+        self.ccode.write(str(aparam.intvalue))
+        self.ccode.write("]")
+
+    def visit_attributes(self, a: CA.CAttributes) -> None:
+        if a.length == 0:
+            return
+        if a.attributes[0].name in ["const", "pconst"]:
+            self.ccode.write("const ")
+        elif a.attributes[0].name == "volatile":
+            self.ccode.write("volatile ")
+        else:
+            self.ccode.write("[[" + a.attributes[0].name + " not yet supported]]")
+
+    def visit_constexp(self, e: CE.CExpConst) -> None:
+        self.ccode.write(str(e))
diff --git a/chc/app/CTyp.py b/chc/app/CTyp.py
index a5906da..3c9e666 100644
--- a/chc/app/CTyp.py
+++ b/chc/app/CTyp.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
@@ -44,6 +44,7 @@
     from chc.app.CAttributes import CAttributes
     from chc.app.CCompInfo import CCompInfo
     from chc.app.CConst import CConst, CConstInt
+    from chc.app.CVisitor import CVisitor
 
 
 integernames = {
@@ -163,6 +164,10 @@ def is_float(self) -> bool:
     def is_function(self) -> bool:
         return False
 
+    @property
+    def is_function_pointer(self) -> bool:
+        return False
+
     @property
     def is_int(self) -> bool:
         return False
@@ -187,6 +192,9 @@ def is_void(self) -> bool:
     def is_default_function_prototype(self) -> bool:
         return False
 
+    def accept(self, visitor: "CVisitor") -> None:
+        raise Exception("CTyp.accept: " + str(self))
+
     def writexml(self, cnode: ET.Element) -> None:
         cnode.set("ix", str(self.index))
         cnode.set("tags", ",".join(self.tags))
@@ -216,6 +224,9 @@ def __init__(self, cd: "CDictionary", ixval: IT.IndexedTableValue) -> None:
     def is_void(self) -> bool:
         return True
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_voidtyp(self)
+
     def get_opaque_type(self) -> CTyp:
         return self
 
@@ -242,6 +253,9 @@ def __init__(self, cd: "CDictionary", ixval: IT.IndexedTableValue) -> None:
     def is_int(self) -> bool:
         return True
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_inttyp(self)
+
     @property
     def size(self) -> int:
         k = self.ikind
@@ -280,6 +294,9 @@ def __init__(self, cd: "CDictionary", ixval: IT.IndexedTableValue) -> None:
     def is_float(self) -> bool:
         return True
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_floattyp(self)
+
     @property
     def fkind(self) -> str:
         return self.tags[1]
@@ -317,6 +334,9 @@ def name(self) -> str:
     def expand(self) -> CTyp:
         return self.cd.decls.expand(self.name)
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_namedtyp(self)
+
     @property
     def size(self) -> int:
         return self.expand().size
@@ -368,6 +388,9 @@ def name(self) -> str:
     def is_struct(self) -> bool:
         return self.compinfo.is_struct
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_comptyp(self)
+
     @property
     def size(self) -> int:
         return self.compinfo.size
@@ -419,6 +442,9 @@ def size(self) -> int:
     def is_enum(self) -> bool:
         return True
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_enumtyp(self)
+
     def get_opaque_type(self) -> CTyp:
         tags = ["tint", "iint"]
         args: List[int] = []
@@ -446,6 +472,9 @@ def __init__(self, cd: "CDictionary", ixval: IT.IndexedTableValue) -> None:
     def is_builtin_vaargs(self) -> bool:
         return True
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_builtinvaargs(self)
+
     def get_opaque_type(self) -> CTyp:
         return self
 
@@ -479,6 +508,13 @@ def size(self) -> int:
     def is_pointer(self) -> bool:
         return True
 
+    @property
+    def is_function_pointer(self) -> bool:
+        return self.pointedto_type.is_function
+
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_ptrtyp(self)
+
     def get_opaque_type(self) -> CTyp:
         tgttype = self.pointedto_type.get_opaque_type()
         tags = ["tptr"]
@@ -536,6 +572,9 @@ def size(self) -> int:
     def is_array(self) -> bool:
         return True
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_arraytyp(self)
+
     def get_opaque_type(self) -> CTyp:
         tags = ["tvoid"]
         args: List[int] = []
@@ -582,6 +621,9 @@ def size(self) -> int:
     def is_function(self) -> bool:
         return True
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_funtyp(self)
+
     def get_opaque_type(self) -> CTyp:
         tags = ["tvoid"]
         args: List[int] = []
@@ -652,6 +694,9 @@ def name(self) -> str:
     def typ(self) -> CTyp:
         return self.cd.get_typ(self.args[0])
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_funarg(self)
+
     def to_dict(self) -> Dict[str, Any]:
         return self.typ.to_dict()
 
@@ -672,6 +717,9 @@ def __init__(self, cd: "CDictionary", ixval: IT.IndexedTableValue) -> None:
     def arguments(self) -> List[CFunArg]:
         return [self.cd.get_funarg(i) for i in self.args]
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_funargs(self)
+
     def to_dict(self) -> List[Dict[str, Any]]:
         return [a.to_dict() for a in self.arguments]
 
diff --git a/chc/app/CVisitor.py b/chc/app/CVisitor.py
new file mode 100644
index 0000000..0844c5d
--- /dev/null
+++ b/chc/app/CVisitor.py
@@ -0,0 +1,96 @@
+# ------------------------------------------------------------------------------
+# CodeHawk C Analyzer
+# Author: Henny Sipma
+# ------------------------------------------------------------------------------
+# The MIT License (MIT)
+#
+# Copyright (c) 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
+# 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 abc import ABC, abstractmethod
+
+import chc.app.CAttributes as CA
+import chc.app.CExp as CE
+import chc.app.CTyp as CT
+from chc.app.CVarInfo import CVarInfo
+
+
+class CVisitor(ABC):
+
+    def __init__(self) -> None:
+        pass
+
+    @abstractmethod
+    def visit_voidtyp(self, ctyp: CT.CTypVoid) -> None:
+        ...
+
+    @abstractmethod
+    def visit_inttyp(self, ctyp: CT.CTypInt) -> None:
+        ...
+
+    @abstractmethod
+    def visit_floattyp(self, ctyp: CT.CTypFloat) -> None:
+        ...
+
+    @abstractmethod
+    def visit_namedtyp(self, ctyp: CT.CTypNamed) -> None:
+        ...
+
+    @abstractmethod
+    def visit_comptyp(self, ctyp: CT.CTypComp) -> None:
+        ...
+
+    @abstractmethod
+    def visit_enumtyp(self, ctyp: CT.CTypEnum) -> None:
+        ...
+
+    @abstractmethod
+    def visit_builtinvaargs(self, ctyp: CT.CTypBuiltinVaargs) -> None:
+        ...
+
+    @abstractmethod
+    def visit_ptrtyp(self, ctyp: CT.CTypPtr) -> None:
+        ...
+
+    @abstractmethod
+    def visit_arraytyp(self, ctyp: CT.CTypArray) -> None:
+        ...
+
+    @abstractmethod
+    def visit_funtyp(self, ctyp: CT.CTypFun) -> None:
+        ...
+
+    @abstractmethod
+    def visit_funarg(self, ctyp: CT.CFunArg) -> None:
+        ...
+
+    @abstractmethod
+    def visit_funargs(self, ctyp: CT.CFunArgs) -> None:
+        ...
+
+    @abstractmethod
+    def visit_attributes(self, a: CA.CAttributes) -> None:
+        ...
+
+    @abstractmethod
+    def visit_constexp(self, a: CE.CExpConst) -> None:
+        ...
diff --git a/chc/cmdline/c_file/cfileutil.py b/chc/cmdline/c_file/cfileutil.py
index 0253fdc..abdc97c 100644
--- a/chc/cmdline/c_file/cfileutil.py
+++ b/chc/cmdline/c_file/cfileutil.py
@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# 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
@@ -174,6 +174,80 @@ def cfile_parse_file(args: argparse.Namespace) -> NoReturn:
     exit(0)
 
 
+def cfile_mk_headerfile(args: argparse.Namespace) -> NoReturn:
+    """Produces a .c file with prototype definitions of functions and global variables.
+
+    This command uses the results of the parse command to create a .c file
+    that contains prototypes of all function definitions and the definitions
+    of all global variables.
+    """
+
+    # arguments
+    xcfilename: str = args.filename
+    opttgtpath: Optional[str] = args.tgtpath
+    loglevel: str = args.loglevel
+    logfilename: Optional[str] = args.logfilename
+    logfilemode: str = args.logfilemode
+    xoutput: Optional[str] = args.output
+
+    projectpath = os.path.dirname(os.path.abspath(xcfilename))
+    targetpath = projectpath if opttgtpath is None else opttgtpath
+    targetpath = os.path.abspath(targetpath)
+    cfilename_ext = os.path.basename(xcfilename)
+    cfilename = cfilename_ext[:-2]
+    projectname = cfilename
+
+    set_logging(
+        loglevel,
+        targetpath,
+        logfilename=logfilename,
+        mode=logfilemode,
+        msg="Command cfile mk-headerfile was invoked")
+
+    chklogger.logger.info(
+        "Project path: %s; target path: %s", projectpath, targetpath)
+
+    parsearchive = UF.get_parse_archive(targetpath, projectname)
+
+    if not os.path.isfile(parsearchive):
+        print_error("Please run parser first on c file")
+        exit(1)
+
+    if os.path.isfile(parsearchive):
+        chklogger.logger.info("Directory is changed to %s", targetpath)
+        os.chdir(targetpath)
+        tarname = os.path.basename(parsearchive)
+        cmd = ["tar", "xfz", os.path.basename(tarname)]
+        chklogger.logger.info("Semantics is extracted from %s", tarname)
+        result = subprocess.call(cmd, cwd=targetpath, stderr=subprocess.STDOUT)
+        if result != 0:
+            print_error("Error in extracting " + tarname)
+            exit(1)
+        chklogger.logger.info(
+            "Semantics was successfully extracted from %s", tarname)
+
+    contractpath = os.path.join(targetpath, "chc_contracts")
+
+    capp = CApplication(
+        projectpath, projectname, targetpath, contractpath, singlefile=True)
+
+    capp.initialize_single_file(cfilename)
+    cfile = capp.get_cfile()
+
+    fheader = cfile.header_declarations()
+
+    if xoutput is not None:
+        outputfilename = xoutput + ".c"
+        with open(outputfilename, "w") as fp:
+            fp.write(fheader)
+        print("Header data written to " + outputfilename)
+
+    else:
+        print(fheader)
+
+    exit(0)
+
+
 def cfile_analyze_file(args: argparse.Namespace) -> NoReturn:
     """Analyzes a single c-file and saves the results in the .cch directory.
 
diff --git a/chc/cmdline/c_project/cprojectutil.py b/chc/cmdline/c_project/cprojectutil.py
index c474f17..d134fc2 100644
--- a/chc/cmdline/c_project/cprojectutil.py
+++ b/chc/cmdline/c_project/cprojectutil.py
@@ -161,6 +161,86 @@ def cproject_parse_project(args: argparse.Namespace) -> NoReturn:
     exit(0)
 
 
+def cproject_mk_headerfile(args: argparse.Namespace) -> NoReturn:
+
+    # arguments
+    tgtpath: str = args.tgtpath
+    projectname: str = args.projectname
+    userdatafile: Optional[str] = args.userdata
+    includepaths: List[str] = args.includepaths
+    includedirs: List[str] = args.includedirs
+    excludepaths: List[str] = args.excludepaths
+    loglevel: str = args.loglevel
+    logfilename: Optional[str] = args.logfilename
+    logfilemode: str = args.logfilemode
+
+    if not os.path.isdir(tgtpath):
+        print_error(f"Target directory {tgtpath} not found")
+        exit(1)
+
+    if userdatafile and not os.path.isfile(userdatafile):
+        print_error(f"Userdata file {userdatafile} not found")
+        exit(1)
+
+    targetpath = os.path.abspath(tgtpath)
+    projectpath = targetpath
+    contractpath = os.path.join(projectpath, "cch_contracts")
+
+    if userdatafile:
+        with open(userdatafile, "r") as fp:
+            userdata = json.load(fp).get("userdata", {})
+    else:
+        userdata = {}
+
+    fnnames: Dict[str, str] = userdata.get("function-names", {})
+    gvarnames: Dict[str, str] = userdata.get("symbolic-addresses", {})
+
+    fnnames = {v: k for (k, v) in fnnames.items()}
+    gvarnames = {v: k for (k, v) in gvarnames.items()}
+
+    set_logging(
+        loglevel,
+        targetpath,
+        logfilename=logfilename,
+        mode=logfilemode,
+        msg="c-project mk-headerfile invoked")
+
+    capp = CApplication(
+        projectpath, projectname, targetpath, contractpath)
+
+    if not UF.has_analysisresults_path(targetpath, projectname):
+        print_error(
+            f"No analysis results found for {projectname} in {targetpath}")
+        exit(1)
+
+    capp = CApplication(
+        projectpath, projectname, targetpath, contractpath)
+
+    lines: List[str] = []
+
+    def is_included(path: Optional[str]) -> bool:
+        if path is None:
+            return True
+        if len(includepaths) > 0:
+            return any(path.startswith(p) for p in includepaths)
+        elif len(includedirs) > 0:
+            return path in includedirs
+        elif len(excludepaths) > 0:
+            return not (any(path.startswith(p) for p in excludepaths))
+        else:
+            return True
+
+    for cfile in capp.cfiles:
+        if not is_included(cfile.cfilepath):
+            continue
+        fheader = cfile.header_declarations(gvarnames, fnnames)
+        lines.append(fheader)
+
+    print("\n\n".join(lines))
+
+    exit(0)
+
+
 def cproject_analyze_project(args: argparse.Namespace) -> NoReturn:
 
     # arguments
@@ -637,3 +717,30 @@ def get_fi_missing_summaries(cfile: "CFile") -> None:
     print("\n".join(lines))
 
     exit(0)
+
+
+def cproject_create_header_file(args: argparse.Namespace) -> NoReturn:
+
+    # arguments
+    tgtpath: str = args.tgtpath
+    projectname: str = args.projectname
+
+    targetpath = os.path.abspath(tgtpath)
+    projectpath = targetpath
+    contractpath = os.path.join(targetpath, "chc_contracts")
+
+    if not UF.has_analysisresults_path(targetpath, projectname):
+        print_error(
+            f"No analysis results found for {projectname} in {targetpath}")
+        exit(1)
+
+    capp = CApplication(
+        projectpath, projectname, targetpath, contractpath)
+
+    for cfile in capp.cfiles:
+        for gfun in cfile.gfunctions.values():
+            if gfun.is_system_function:
+                continue
+            print(str(gfun.varinfo))
+
+    exit(0)
diff --git a/chc/cmdline/chkc b/chc/cmdline/chkc
index e7bdfa6..fa14016 100755
--- a/chc/cmdline/chkc
+++ b/chc/cmdline/chkc
@@ -650,6 +650,34 @@ def parse() -> argparse.Namespace:
 
     cfileparse.set_defaults(func=C.cfile_parse_file)
 
+    # --- mk-headerfile
+    cfilemkheader = cfileparsers.add_parser("mk-headerfile")
+    cfilemkheader.add_argument(
+        "filename",
+        help="name of file to analyze ((<cpath/>)<cfilename>)")
+    cfilemkheader.add_argument(
+        "--tgtpath",
+        help="directory in which to store the analysis artifacts "
+        + "(default: <cpath>)")
+    cfilemkheader.add_argument(
+        "--output", "-o",
+        help=("basename of file to save output "
+              + "(without extension): a file with extension .c will be created"))
+    cfilemkheader.add_argument(
+        "--loglevel", "-log",
+        choices=UL.LogLevel.options(),
+        default="NONE",
+        help="activate logging with given level (default to stderr)")
+    cfilemkheader.add_argument(
+        "--logfilename",
+        help="name of file to write log messages")
+    cfilemkheader.add_argument(
+        "--logfilemode",
+        choices=["a", "w"],
+        default="a",
+        help="file mode for log file: append (a, default), or write (w)")
+    cfilemkheader.set_defaults(func=C.cfile_mk_headerfile)
+
     # --- analyze
     cfileanalyze = cfileparsers.add_parser("analyze")
     cfileanalyze.add_argument(
@@ -1326,6 +1354,44 @@ def parse() -> argparse.Namespace:
 
     cprojectparse.set_defaults(func=P.cproject_parse_project)
 
+    # --- mk-headerfile
+    cprojectmkheader = cprojectparsers.add_parser("mk-headerfile")
+    cprojectmkheader.add_argument(
+        "tgtpath", help="directory that contains the analysis results")
+    cprojectmkheader.add_argument(
+        "projectname", help="name of the project")
+    cprojectmkheader.add_argument(
+        "--userdata", help="name of json file with userdata")
+    cprojectmkheader.add_argument(
+        "--includepaths",
+        nargs="*",
+        default=[],
+        help="names of (relative) paths from which to include source files")
+    cprojectmkheader.add_argument(
+        "--includedirs",
+        nargs="*",
+        default=[],
+        help="names of (relative) directories from which to include source files")
+    cprojectmkheader.add_argument(
+        "--excludepaths",
+        nargs="*",
+        default=[],
+        help="names of (relative) path from which not to include source files")
+    cprojectmkheader.add_argument(
+        "--loglevel", "-log",
+        choices=UL.LogLevel.options(),
+        default="NONE",
+        help="activate logging with given level (default to stderr)")
+    cprojectmkheader.add_argument(
+        "--logfilename",
+        help="name of file to write log messages")
+    cprojectmkheader.add_argument(
+        "--logfilemode",
+        choices=["a", "w"],
+        default="a",
+        help="file mode for log file: append (a, default), or write (w)")
+    cprojectmkheader.set_defaults(func=P.cproject_mk_headerfile)
+
     # --- analyze
     cprojectanalyze = cprojectparsers.add_parser("analyze")
     cprojectanalyze.add_argument(
@@ -1427,6 +1493,14 @@ def parse() -> argparse.Namespace:
         help="show for all files (including application files)")
     cprojectmissingsummaries.set_defaults(func=P.cproject_missing_summaries)
 
+    # --- create_header_file
+    cprojectcreateheader = cprojectparsers.add_parser("create-header-file")
+    cprojectcreateheader.add_argument(
+        "tgtpath", help="directory that contains the analysis results")
+    cprojectcreateheader.add_argument(
+        "projectname", help="name of the project")
+    cprojectcreateheader.set_defaults(func=P.cproject_create_header_file)
+
     args = parser.parse_args()
     return args