diff --git a/chc/app/CApplication.py b/chc/app/CApplication.py
index 39e4fa9..71d030f 100644
--- a/chc/app/CApplication.py
+++ b/chc/app/CApplication.py
@@ -54,6 +54,7 @@
 if TYPE_CHECKING:
     from chc.app.CFunction import CFunction
     from chc.app.CInstr import CCallInstr
+    from chc.proof.CandidateOutputParameter import CandidateOutputParameter
     from chc.proof.CFunctionCallsiteSPOs import CFunctionCallsiteSPOs
     from chc.proof.CFunctionPO import CFunctionPO
 
@@ -93,12 +94,14 @@ def __init__(
             targetpath: str,
             contractpath: str,
             singlefile: bool = False,
+            keep_system_includes: bool = False,
             excludefiles: List[str] = []) -> None:
         self._projectpath = projectpath
         self._projectname = projectname
         self._targetpath = targetpath
         self._contractpath = contractpath
         self._singlefile = singlefile
+        self._keep_system_includes = keep_system_includes
         self._excludefiles = excludefiles
         self._indexmanager = IndexManager(singlefile)
         self._globalcontract: Optional[CGlobalContract] = None
@@ -138,6 +141,19 @@ def globalcontract(self) -> CGlobalContract:
     def is_singlefile(self) -> bool:
         return self._singlefile
 
+    @property
+    def keep_system_includes(self) -> bool:
+        """Returns true if functions from the system path ('/') must be included
+
+        This property is false by default and must be enabled via a command-line
+        option.
+
+        It is intended to, by default, filter out functions defined in header
+        files, that would otherwise be included in every source file.
+        """
+
+        return self._keep_system_includes
+
     @property
     def excludefiles(self) -> List[str]:
         return self._excludefiles
@@ -300,6 +316,34 @@ def g(fi: CFile) -> None:
 
         self.iter_files_parallel(g, maxprocesses)
 
+    def check_digests(self) -> bool:
+        for cfile in list(self.cfiles):
+            for cfun in cfile.get_functions():
+                if cfun.analysis_digests.is_active:
+                    return True
+        return False
+
+    def outputparameters(self) -> Dict[str, List["CandidateOutputParameter"]]:
+        result: Dict[str, List["CandidateOutputParameter"]] = {}
+        for cfile in list(self.cfiles):
+            for cfun in cfile.get_functions():
+                result[cfun.name] = cfun.analysis_digests.outputparameters()
+        return result
+
+    def viable_outputparameters(self) -> Dict[str, List["CandidateOutputParameter"]]:
+        result: Dict[str, List["CandidateOutputParameter"]] = {}
+        for cfile in list(self.cfiles):
+            for cfun in cfile.get_functions():
+                result[cfun.name] = cfun.analysis_digests.viable_outputparameters()
+        return result
+
+    def maybe_outputparameters(self) -> Dict[str, List["CandidateOutputParameter"]]:
+        result: Dict[str, List["CandidateOutputParameter"]] = {}
+        for cfile in list(self.cfiles):
+            for cfun in cfile.get_functions():
+                result[cfun.name] = cfun.analysis_digests.maybe_outputparameters()
+        return result
+
     def resolve_vid_function(
             self, filevar: FileVarReference) -> Optional["CFunction"]:
         """Returns the function def for the local file-index fid and vid.
diff --git a/chc/app/CAttributes.py b/chc/app/CAttributes.py
index 891b406..3a93aa7 100644
--- a/chc/app/CAttributes.py
+++ b/chc/app/CAttributes.py
@@ -113,6 +113,9 @@ def is_index(self) -> bool:
     def is_question(self) -> bool:
         return False
 
+    def accept(self, visitor: "CVisitor") -> None:
+        raise UF.CHCError("visitor not yet implemented for " + str(self))
+
     def __str__(self) -> str:
         return "attrparam:" + self.tags[0]
 
@@ -135,6 +138,9 @@ def intvalue(self) -> int:
     def is_int(self) -> bool:
         return True
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_attr_int(self)
+
     def __str__(self) -> str:
         return "aint(" + str(self.intvalue) + ")"
 
@@ -157,6 +163,9 @@ def stringvalue(self) -> str:
     def is_str(self) -> bool:
         return True
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_attr_str(self)
+
     def __str__(self) -> str:
         return "astr(" + str(self.stringvalue) + ")"
 
@@ -184,6 +193,9 @@ def params(self) -> List[CAttr]:
     def is_cons(self) -> bool:
         return True
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_attr_cons(self)
+
     def __str__(self) -> str:
         return "acons(" + str(self.name) + ")"
 
@@ -206,6 +218,9 @@ def typ(self) -> "CTyp":
     def is_sizeof(self) -> bool:
         return True
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_attr_sizeof(self)
+
     def __str__(self) -> str:
         return "asizeof(" + str(self.typ) + ")"
 
@@ -228,6 +243,9 @@ def param(self) -> CAttr:
     def is_sizeofe(self) -> bool:
         return True
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_attr_sizeofe(self)
+
     def __str__(self) -> str:
         return "asizeofe(" + str(self.param) + ")"
 
@@ -250,6 +268,9 @@ def typsig(self) -> "CTypsig":
     def is_sizeofs(self) -> bool:
         return True
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_attr_sizeofs(self)
+
     def __str__(self) -> str:
         return "asizeofs(" + str(self.typsig) + ")"
 
@@ -272,6 +293,9 @@ def typ(self) -> "CTyp":
     def is_alignof(self) -> bool:
         return True
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_attr_alignof(self)
+
     def __str__(self) -> str:
         return "aalignof(" + str(self.typ) + ")"
 
@@ -294,6 +318,9 @@ def param(self) -> CAttr:
     def is_alignofe(self) -> bool:
         return True
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_attr_alignofe(self)
+
     def __str__(self) -> str:
         return "aalignofe(" + str(self.param) + ")"
 
@@ -316,6 +343,9 @@ def typsig(self) -> "CTypsig":
     def is_alignofs(self) -> bool:
         return True
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_attr_alignofs(self)
+
     def __str__(self) -> str:
         return "aalignofs(" + str(self.typsig) + ")"
 
@@ -343,6 +373,9 @@ def param(self) -> CAttr:
     def is_unop(self) -> bool:
         return True
 
+    def acecpt(self, visitor: "CVisitor") -> None:
+        visitor.visit_attr_unop(self)
+
     def __str__(self) -> str:
         return "aunop(" + self.op + "," + str(self.param) + ")"
 
@@ -375,6 +408,9 @@ def param2(self) -> CAttr:
     def is_binop(self) -> bool:
         return True
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_attr_binop(self)
+
     def __str__(self) -> str:
         return (
             "abinop("
@@ -410,6 +446,9 @@ def param(self) -> CAttr:
     def is_dot(self) -> bool:
         return True
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_attr_dot(self)
+
     def __str__(self) -> str:
         return "adot(" + str(self.param) + "." + self.suffix + ")"
 
@@ -436,6 +475,9 @@ def param(self) -> CAttr:
     def is_star(self) -> bool:
         return True
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_attr_star(self)
+
     def __str__(self) -> str:
         if self.index == self.args[0]:
             return "astar()"
@@ -461,6 +503,9 @@ def param(self) -> CAttr:
     def is_addrof(self) -> bool:
         return True
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_attr_addrof(self)
+
     def __str__(self) -> str:
         return "aaddrof(" + str(self.param) + ")"
 
@@ -488,6 +533,9 @@ def param2(self) -> CAttr:
     def is_index(self) -> bool:
         return True
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_attr_index(self)
+
     def __str__(self) -> str:
         return "aindex(" + str(self.param1) + "," + str(self.param2) + ")"
 
@@ -516,6 +564,9 @@ def param2(self) -> CAttr:
     def param3(self) -> CAttr:
         return self.cd.get_attrparam(int(self.args[2]))
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_attr_question(self)
+
     def __str__(self) -> str:
         return (
             "aquestion("
@@ -541,6 +592,9 @@ def name(self) -> str:
     def params(self) -> List[CAttr]:
         return [self.cd.get_attrparam(int(i)) for i in self.args]
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_attribute(self)
+
     def __str__(self) -> str:
         return self.name + ": " + ",".join([str(p) for p in self.params])
 
diff --git a/chc/app/CCompInfo.py b/chc/app/CCompInfo.py
index 5c5d2f1..f296182 100644
--- a/chc/app/CCompInfo.py
+++ b/chc/app/CCompInfo.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.CDeclarations import CDeclarations
     from chc.app.CFieldInfo import CFieldInfo
     from chc.app.CGlobalDeclarations import CGlobalDeclarations
+    from chc.app.CVisitor import CVisitor
 
 
 class CCompInfo(CDeclarationsRecord):
@@ -100,6 +101,9 @@ def name(self) -> str:
     def field_strings(self) -> str:
         return ":".join([f.fname for f in self.fields])
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_compinfo(self)
+
     def __str__(self) -> str:
         lines = []
         lines.append("struct " + self.name)
diff --git a/chc/app/CContextDictionary.py b/chc/app/CContextDictionary.py
index 09f22ff..c612a52 100644
--- a/chc/app/CContextDictionary.py
+++ b/chc/app/CContextDictionary.py
@@ -88,6 +88,16 @@ def get_program_context(self, ix: int) -> ProgramContext:
     def get_program_context_map(self) -> Dict[int, IndexedTableValue]:
         return self.context_table.objectmap(self.get_program_context)
 
+    # ----------------- read_xml service ---------------------------------------
+
+    def read_xml_program_context(
+            self, node: ET.Element, tag: str = "ictxt") -> ProgramContext:
+        xtag = node.get(tag)
+        if xtag is not None:
+            return self.get_program_context(int(xtag))
+        else:
+            raise UF.CHCError(f"Xml element {node.tag} is missing attribute {tag}")
+
     # ----------------------- Printing -----------------------------------------
 
     def objectmap_to_string(self, name: str) -> str:
diff --git a/chc/app/CDictionary.py b/chc/app/CDictionary.py
index 349335e..c74bad5 100644
--- a/chc/app/CDictionary.py
+++ b/chc/app/CDictionary.py
@@ -268,6 +268,13 @@ def read_xml_exp(self, node: ET.Element, tag: str = "iexp") -> CExp:
         else:
             raise Exception('xml node was missing the tag "' + tag + '"')
 
+    def read_xml_exp_o(
+            self, node: ET.Element, tag: str = "iexp") -> Optional[CExp]:
+        xtag_o = node.get(tag)
+        if xtag_o is not None:
+            return self.get_exp(int(xtag_o))
+        return None
+
     def write_xml_exp_opt(
         self,
         node: ET.Element,
diff --git a/chc/app/CExp.py b/chc/app/CExp.py
index 3c0a3ee..1afce84 100644
--- a/chc/app/CExp.py
+++ b/chc/app/CExp.py
@@ -32,6 +32,7 @@
 
 from chc.app.CDictionaryRecord import CDictionaryRecord, cdregistry
 
+import chc.util.fileutil as UF
 import chc.util.IndexedTable as IT
 
 if TYPE_CHECKING:
@@ -148,15 +149,15 @@ 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"}
 
     def to_idict(self) -> Dict[str, Any]:
         return {"t": self.tags, "a": self.args}
 
+    def accept(self, visitor: "CVisitor") -> None:
+        raise UF.CHCError("visitor not yet implemented for: " + str(self))
+
     def __str__(self) -> str:
         return "baseexp:" + self.tags[0]
 
@@ -223,6 +224,9 @@ def get_variable_uses(self, vid: int) -> int:
     def to_dict(self) -> Dict[str, Any]:
         return {"base": "lval", "lval": self.lval.to_dict()}
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_explval(self)
+
     def __str__(self) -> str:
         return str(self.lval)
 
@@ -248,6 +252,9 @@ def is_sizeof(self) -> bool:
     def to_dict(self) -> Dict[str, Any]:
         return {"base": "sizeof", "type": self.typ.to_dict()}
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_sizeof(self)
+
     def __str__(self) -> str:
         return "sizeof(" + str(self.typ) + ")"
 
@@ -279,6 +286,9 @@ def get_variable_uses(self, vid: int) -> int:
     def to_dict(self) -> Dict[str, Any]:
         return {"base": "sizeofe", "exp": self.exp.to_dict()}
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_sizeofe(self)
+
     def __str__(self) -> str:
         return "sizeofe(" + str(self.exp) + ")"
 
@@ -307,6 +317,9 @@ def is_sizeofstr(self) -> bool:
     def to_dict(self) -> Dict[str, Any]:
         return {"base": "sizeofstr", "string": self.stringvalue}
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_size_of_str(self)
+
     def __str__(self) -> str:
         return "sizeofstr(" + str(self.stringvalue) + ")"
 
@@ -332,6 +345,9 @@ def is_alignof(self) -> bool:
     def to_dict(self) -> Dict[str, Any]:
         return {"base": "alignof", "type": self.typ.to_dict()}
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_alignof(self)
+
     def __str__(self) -> str:
         return "alignof(" + str(self.typ) + ")"
 
@@ -366,6 +382,9 @@ def get_variable_uses(self, vid: int) -> int:
     def to_dict(self) -> Dict[str, Any]:
         return {"base": "alignofe", "exp": self.exp.to_dict()}
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_alignofe(self)
+
     def __str__(self) -> str:
         return "alignofe(" + str(self.exp) + ")"
 
@@ -411,6 +430,9 @@ def get_variable_uses(self, vid: int) -> int:
     def to_dict(self) -> Dict[str, Any]:
         return {"base": "unop", "op": self.op, "exp": self.exp.to_dict()}
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_unop(self)
+
     def __str__(self) -> str:
         return "(" + unoperatorstrings[self.op] + " " + str(self.exp) + ")"
 
@@ -474,6 +496,9 @@ def to_dict(self) -> Dict[str, Any]:
             "exp2": self.exp2.to_dict(),
         }
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_binop(self)
+
     def __str__(self) -> str:
         return (
             "("
@@ -549,6 +574,9 @@ def to_dict(self) -> Dict[str, object]:
             "type": self.typ.to_dict(),
         }
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_question(self)
+
     def __str__(self) -> str:
         return (
             "("
@@ -600,6 +628,9 @@ def to_dict(self) -> Dict[str, object]:
             "type": self.typ.to_dict(),
         }
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_cast(self)
+
     def __str__(self) -> str:
         return "caste(" + str(self.typ) + "," + str(self.exp) + ")"
 
@@ -634,6 +665,9 @@ def get_variable_uses(self, vid: int) -> int:
     def to_dict(self) -> Dict[str, object]:
         return {"base": "addrof", "lval": self.lval.to_dict()}
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_addrof(self)
+
     def __str__(self) -> str:
         return "&(" + str(self.lval) + ")"
 
@@ -655,6 +689,9 @@ def label_sid(self) -> int:
     def to_dict(self) -> Dict[str, object]:
         return {"base": "addroflabel", "label": self.label_sid}
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_addr_of_label(self)
+
     def __str__(self) -> str:
         return "addroflabel(" + str(self.label_sid) + ")"
 
@@ -689,6 +726,9 @@ def get_variable_uses(self, vid: int) -> int:
     def to_dict(self) -> Dict[str, Any]:
         return {"base": "startof", "lval": self.lval.to_dict()}
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_startof(self)
+
     def __str__(self) -> str:
         return "&(" + str(self.lval) + ")"
 
@@ -722,6 +762,9 @@ def arguments(self) -> List[Optional[CExp]]:
     def has_variable(self, vid: int) -> bool:
         return any([a.has_variable(vid) for a in self.arguments if a])
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_fn_app(self)
+
     def __str__(self) -> str:
         return (
             "fnapp("
@@ -762,6 +805,9 @@ def arguments(self) -> List[Optional[CExp]]:
     def has_variable(self, vid: int) -> bool:
         return any([a.has_variable(vid) for a in self.arguments if a])
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_cn_app(self)
+
     def __str__(self) -> str:
         return (
             "cnapp("
diff --git a/chc/app/CFieldInfo.py b/chc/app/CFieldInfo.py
index 9446c57..43c0665 100644
--- a/chc/app/CFieldInfo.py
+++ b/chc/app/CFieldInfo.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.CFileDeclarations import CFileDeclarations
     from chc.app.CLocation import CLocation
     from chc.app.CTyp import CTyp
+    from chc.app.CVisitor import CVisitor
 
 
 class CFieldInfo(CDeclarationsRecord):
@@ -87,5 +88,8 @@ def attributes(self) -> Optional["CAttributes"]:
             return self.dictionary.get_attributes(self.args[3])
         return None
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_fieldinfo(self)
+
     def __str__(self) -> str:
         return self.fname + ":" + str(self.ftype)
diff --git a/chc/app/CFile.py b/chc/app/CFile.py
index be69244..f868859 100644
--- a/chc/app/CFile.py
+++ b/chc/app/CFile.py
@@ -154,6 +154,10 @@ def name(self) -> str:
     def capp(self) -> "CApplication":
         return self._capp
 
+    @property
+    def keep_system_includes(self) -> bool:
+        return self.capp.keep_system_includes
+
     @property
     def targetpath(self) -> str:
         return self.capp.targetpath
@@ -212,8 +216,40 @@ def header_declarations(
             fndecl = pp.function_declaration_str(
                 fn.varinfo, srcloc=srcfilename, binloc=binloc)
             lines.append(fndecl)
+
         return "\n".join(lines)
 
+    def cil_source(self) -> str:
+        lines: List[str] = []
+        srcfilename = self.name + ".cil.c"
+        lines.append("// " + srcfilename + "\n")
+        gtypes = self.gtypes.values()
+        gcompdefs = self.gcomptagdefs.values()
+        gcompdecls = self.gcomptagdecls.values()
+        genumdefs = self.genumtagdefs.values()
+        genumdecls = self.genumtagdecls.values()
+        gvardefs = self.gvardefs.values()
+        gvardecls = self.gvardecls.values()
+        if len(gtypes) > 0:
+            lines.append("// type definitions")
+        for gtype in gtypes:
+            pp = CPrettyPrinter()
+            lines.append(pp.cgtypedef_str(gtype))
+        if len(gcompdefs) > 0:
+            lines.append("// struct definitions")
+        for gcompdef in gcompdefs:
+            pp = CPrettyPrinter()
+            lines.append(pp.cgcomptag_str(gcompdef))
+        if len(gvardefs) > 0:
+            lines.append("// static and global variable definitions\n")
+        for gvar in gvardefs:
+            pp = CPrettyPrinter()
+            lines.append(pp.cgvardef_str(gvar))
+        for fn in self.functions.values():
+            pp = CPrettyPrinter()
+            lines.append(pp.function_definition_to_string(fn))
+        return "\n\n".join(lines)
+
     @property
     def functioncount(self) -> int:
         return self.cfileglobals.functioncount
diff --git a/chc/app/CFileDeclarations.py b/chc/app/CFileDeclarations.py
index c70dd07..2ad2366 100644
--- a/chc/app/CFileDeclarations.py
+++ b/chc/app/CFileDeclarations.py
@@ -37,6 +37,7 @@
     List,
     Mapping,
     NoReturn,
+    Optional,
     Tuple,
     TYPE_CHECKING)
 import xml.etree.ElementTree as ET
@@ -92,6 +93,10 @@ def xget_int_attr(p: ET.Element, tag: str) -> int:
     return UF.xget_int_attr(p, tag, "CFileDeclarations")
 
 
+def xget_int_attr_o(node: ET.Element, tag: str) -> Optional[int]:
+    return UF.xget_int_attr_o(node, tag)
+
+
 class CFilename(CDeclarationsRecord):
 
     def __init__(self, decls: CDeclarations, ixval: IndexedTableValue):
@@ -266,6 +271,17 @@ def read_xml_location(
             return CLocation(self, itv)
         return self.get_location(index)
 
+    def read_xml_location_o(
+            self, xnode: ET.Element, tag: str = "iloc") -> Optional[CLocation]:
+        index = xget_int_attr_o(xnode, tag)
+        if index is not None:
+            if index == -1:
+                args = [-1, -1, -1]
+                itv = IndexedTableValue(-1, [], args)
+                return CLocation(self, itv)
+            return self.get_location(index)
+        return None
+
     # -------------------- Index items by category ---------------------------
 
     def index_filename(self, name: str) -> int:
diff --git a/chc/app/CFileGlobals.py b/chc/app/CFileGlobals.py
index a908803..5480370 100644
--- a/chc/app/CFileGlobals.py
+++ b/chc/app/CFileGlobals.py
@@ -50,6 +50,7 @@
     from chc.app.CTyp import CTyp
     from chc.app.CTypeInfo import CTypeInfo
     from chc.app.CVarInfo import CVarInfo
+    from chc.app.CVisitor import CVisitor
 
 
 @dataclass
@@ -71,6 +72,9 @@ def ckey(self) -> int:
     def is_struct(self) -> bool:
         return self.compinfo.is_struct
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_cgcomptag(self)
+
     def __str__(self) -> str:
         if self.is_struct:
             return f"struct {self.name} (ckey: {self.ckey})"
@@ -121,6 +125,9 @@ class CGType:
     location: "CLocation"
     typeinfo: "CTypeInfo"
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_cgtype(self)
+
 
 @dataclass
 class CGVarDecl:
@@ -149,6 +156,9 @@ def vname(self) -> str:
     def has_initializer(self) -> bool:
         return self.initializer is not None
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_cgvardef(self)
+
     def __str__(self) -> str:
         if self.initializer is not None:
             return f"{self.varinfo} = {self.initializer}"
@@ -179,6 +189,10 @@ def __init__(self, cfile: "CFile", xnode: ET.Element) -> None:
     def cfile(self) -> "CFile":
         return self._cfile
 
+    @property
+    def keep_system_includes(self) -> bool:
+        return self.cfile.keep_system_includes
+
     @property
     def declarations(self) -> "CFileDeclarations":
         return self.cfile.declarations
@@ -284,6 +298,16 @@ def gfunctions(self) -> Dict[int, CGFunction]:
                     xiloc = xf.get("iloc")
                     if xivinfo is not None and xiloc is not None:
                         vinfo = self.declarations.get_varinfo(int(xivinfo))
+                        if (
+                                not self.keep_system_includes
+                                and vinfo.vdecl is not None
+                                and vinfo.vdecl.file.startswith("/")):
+                            chklogger.logger.info(
+                                "%s: Skip system function %s defined in %s",
+                                self.cfile.cfilename,
+                                vinfo.vname,
+                                vinfo.vdecl.file)
+                            continue
                         loc = self.declarations.get_location(int(xiloc))
                         gfun = CGFunction(loc, vinfo)
                         self._gfunctions[vinfo.vid] = gfun
diff --git a/chc/app/CFunction.py b/chc/app/CFunction.py
index e7799cf..7eba674 100644
--- a/chc/app/CFunction.py
+++ b/chc/app/CFunction.py
@@ -35,9 +35,10 @@
 
 from chc.api.CFunctionApi import CFunctionApi
 
-from chc.app.CLocation import CLocation
 from chc.app.CFunDeclarations import CFunDeclarations
 from chc.app.CInstr import CCallInstr
+from chc.app.CFunctionReturnSite import CFunctionReturnSite
+from chc.app.CLocation import CLocation
 from chc.app.CStmt import CFunctionBody
 from chc.app.IndexManager import FileVarReference
 
@@ -46,12 +47,13 @@
 from chc.invariants.CFunInvariantTable import CFunInvariantTable
 from chc.invariants.CInvariantFact import CInvariantFact
 
-from chc.proof.CFunPODictionary import CFunPODictionary
+from chc.proof.CFunctionAnalysisDigest import CFunctionAnalysisDigests
 from chc.proof.CFunctionCallsiteSPOs import CFunctionCallsiteSPOs
 from chc.proof.CFunctionPO import CFunctionPO
 from chc.proof.CFunctionPPO import CFunctionPPO
 from chc.proof.CFunctionProofs import CFunctionProofs
 from chc.proof.CFunctionSPOs import CFunctionSPOs
+from chc.proof.CFunPODictionary import CFunPODictionary
 
 import chc.util.fileutil as UF
 from chc.util.loggingutil import chklogger
@@ -60,8 +62,10 @@
     from chc.api.CFunctionContract import CFunctionContract
     from chc.api.InterfaceDictionary import InterfaceDictionary
     from chc.app.CApplication import CApplication
+    from chc.app.CDictionary import CDictionary
     from chc.app.CFile import CFile
     from chc.app.CFileDeclarations import CFileDeclarations
+    from chc.app.COffset import COffset
     from chc.app.CTyp import CTyp
     from chc.app.CVarInfo import CVarInfo
 
@@ -78,12 +82,14 @@ def __init__(self, cfile: "CFile", xnode: ET.Element, fname: str) -> None:
         self._formals: Dict[int, "CVarInfo"] = {}  # vid -> CVarInfo
         self._locals: Dict[int, "CVarInfo"] = {}  # vid -> CVarInfo
         self._sbody: Optional[CFunctionBody] = None
+        self._returnsites: Optional[List[CFunctionReturnSite]] = None
         self._podictionary: Optional[CFunPODictionary] = None
         self._api: Optional[CFunctionApi] = None
         self._proofs: Optional[CFunctionProofs] = None
         self._vard: Optional[CFunVarDictionary] = None
         self._invd: Optional[CFunInvDictionary] = None
         self._invarianttable: Optional[CFunInvariantTable] = None
+        self._analysis_digests: Optional[CFunctionAnalysisDigests] = None
 
     def xmsg(self, txt: str) -> str:
         return "Function " + self.name + ": " + txt
@@ -140,6 +146,10 @@ def ftype(self) -> "CTyp":
     def cfiledecls(self) -> "CFileDeclarations":
         return self.cfile.declarations
 
+    @property
+    def cdictionary(self) -> "CDictionary":
+        return self.cfile.dictionary
+
     @property
     def interfacedictionary(self) -> "InterfaceDictionary":
         return self.cfile.interfacedictionary
@@ -287,6 +297,63 @@ def podictionary(self) -> CFunPODictionary:
             self._podictionary = CFunPODictionary(self, pxnode)
         return self._podictionary
 
+    @property
+    def analysis_digests(self) -> CFunctionAnalysisDigests:
+        if self._analysis_digests is None:
+            adnode = UF.get_adg_xnode(
+                self.targetpath,
+                self.projectname,
+                self.cfilepath,
+                self.cfilename,
+                self.name)
+            if adnode is None:
+                chklogger.logger.warning(
+                    "No adg file encountered for function %s", self.name)
+                adgnode = None
+                # raise UF.CHCError(self.xmsg("adg file not found"))
+            else:
+                adgnode = adnode.find("analysis-digests")
+            self._analysis_digests = CFunctionAnalysisDigests(self, adgnode)
+        return self._analysis_digests
+
+    def callsites(self) -> List[CCallInstr]:
+        callinstrs = self.capp.get_callinstrs()
+        result: List[CCallInstr] = []
+        for instr in callinstrs:
+            if str(instr.callee) == self.name:
+                result.append(instr)
+        return result
+
+    @property
+    def returnsites(self) -> List[CFunctionReturnSite]:
+        if self._returnsites is None:
+            self._returnsites = []
+            xsponode = UF.get_spo_xnode(
+                self.targetpath,
+                self.projectname,
+                self.cfilepath,
+                self.cfilename,
+                self.name)
+            if xsponode is None:
+                raise UF.CHCError(self.xmsg("spo file is missing"))
+            xxsponode = xsponode.find("spos")
+            if xxsponode is None:
+                raise UF.CHCError(self.xmsg("spo file has no spos element"))
+            xreturnsites = xxsponode.find("returnsites")
+            if xreturnsites is None:
+                raise UF.CHCError(
+                    self.xmsg("spo file has no returnsites element"))
+            for xreturnsite in xreturnsites.findall("rs"):
+                self._returnsites.append(CFunctionReturnSite(self, xreturnsite))
+        return self._returnsites
+
+    def get_returnsite(
+            self, ctxtid: int) -> Optional[CFunctionReturnSite]:
+        for rs in self.returnsites:
+            if rs.context.index == ctxtid:
+                return rs
+        return None
+
     @property
     def proofs(self) -> CFunctionProofs:
         if self._proofs is None:
@@ -311,7 +378,7 @@ def proofs(self) -> CFunctionProofs:
                 raise UF.CHCError(self.xmsg("spo file is missing"))
             xxsponode = xsponode.find("spos")
             if xxsponode is None:
-                raise UF.CHCError(self.xmsg("_spo file has no spos element"))
+                raise UF.CHCError(self.xmsg("spo file has no spos element"))
             self._proofs = CFunctionProofs(self, xxpponode, xxsponode)
         return self._proofs
 
@@ -319,6 +386,7 @@ def reinitialize_tables(self) -> None:
         self._api = None
         self._podictionary = None
         self._vardictionary = None
+        self._analysis_digests = None
         self._proofs = None
 
     def get_formal_vid(self, name: str) -> int:
@@ -405,7 +473,7 @@ def get_source_code_file(self) -> str:
     def has_line_number(self) -> bool:
         if self.has_source_code_file():
             srcfile = self.get_source_code_file()
-            return self.cfile.cfilename + ".c" == srcfile
+            return self.cfile.name + ".c" == srcfile
         else:
             return False
 
@@ -515,16 +583,28 @@ def get_spos(self) -> List[CFunctionPO]:
         return self.proofs.spolist
 
     def get_open_ppos(self) -> List[CFunctionPO]:
-        return self.proofs.open_ppos
+        try:
+            return self.proofs.open_ppos
+        except UF.CHCFileNotFoundError:
+            return []
 
     def get_open_spos(self) -> List[CFunctionPO]:
         return self.proofs.open_spos
 
     def get_ppos_violated(self) -> List[CFunctionPO]:
-        return self.proofs.ppos_violated
+        try:
+            return self.proofs.ppos_violated
+        except UF.CHCFileNotFoundError:
+            return []
 
     def get_spo_violations(self) -> List[CFunctionPO]:
-        return self.proofs.get_spo_violations()
+        try:
+            return self.proofs.get_spo_violations()
+        except UF.CHCFileNotFoundError:
+            return []
 
     def get_ppos_delegated(self) -> List[CFunctionPO]:
-        return self.proofs.ppos_delegated
+        try:
+            return self.proofs.ppos_delegated
+        except UF.CHCFileNotFoundError:
+            return []
diff --git a/chc/app/CFunctionReturnSite.py b/chc/app/CFunctionReturnSite.py
new file mode 100644
index 0000000..9cdbfcc
--- /dev/null
+++ b/chc/app/CFunctionReturnSite.py
@@ -0,0 +1,92 @@
+# ------------------------------------------------------------------------------
+# 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.
+# ------------------------------------------------------------------------------
+
+import xml.etree.ElementTree as ET
+
+from typing import Optional, TYPE_CHECKING
+
+if TYPE_CHECKING:
+    from chc.app.CContext import ProgramContext
+    from chc.app.CContext import CContextDictionary
+    from chc.app.CDictionary import CDictionary
+    from chc.app.CExp import CExp
+    from chc.app.CFile import CFile
+    from chc.app.CFileDeclarations import CFileDeclarations
+    from chc.app.CFunction import CFunction
+    from chc.app.CLocation import CLocation
+
+
+class CFunctionReturnSite:
+
+    def __init__(self, cfun: "CFunction", xnode: ET.Element) -> None:
+        self._cfun = cfun
+        self._xnode = xnode
+
+    @property
+    def cfun(self) -> "CFunction":
+        return self._cfun
+
+    @property
+    def cdictionary(self) -> "CDictionary":
+        return self.cfun.cdictionary
+
+    @property
+    def cfile(self) -> "CFile":
+        return self.cfun.cfile
+
+    @property
+    def cfiledeclarations(self) -> "CFileDeclarations":
+        return self.cfile.declarations
+
+    @property
+    def contextdictionary(self) -> "CContextDictionary":
+        return self.cfile.contextdictionary
+
+    @property
+    def xnode(self) -> ET.Element:
+        return self._xnode
+
+    @property
+    def location(self) -> "CLocation":
+        return self.cfiledeclarations.read_xml_location(self.xnode)
+
+    @property
+    def returnexp(self) -> Optional["CExp"]:
+        return self.cdictionary.read_xml_exp_o(self.xnode)
+
+    @property
+    def context(self) -> "ProgramContext":
+        return self.contextdictionary.read_xml_program_context(self.xnode)
+
+    def __str__(self):
+        rexp = str(self.returnexp) if self.returnexp else ""
+        return (
+            "return " + rexp + " ("
+            + str(self.location.line) + ", " + str(self.location.byte)
+            + ") ("
+            + str(self.context)
+        )
diff --git a/chc/app/CGlobalDeclarations.py b/chc/app/CGlobalDeclarations.py
index 59e057b..a92fe8d 100644
--- a/chc/app/CGlobalDeclarations.py
+++ b/chc/app/CGlobalDeclarations.py
@@ -594,7 +594,7 @@ def index_init(self, init: CInitInfo, fid: int = -1) -> int:
             args = [self.dictionary.index_exp(init.exp, fid=fid)]
             return self.mk_single_init_index(init.tags, args)
 
-        if init.is_compound:
+        elif init.is_compound:
             init = cast("CCompoundInitInfo", init)
             gtype = self.dictionary.index_typ(init.typ)
             oinits: List[int] = [
@@ -604,7 +604,9 @@ def index_init(self, init: CInitInfo, fid: int = -1) -> int:
             return self.mk_compound_init_index(init.tags, args)
 
         else:
-            raise Exception("InitInfo not recognized")
+            init = cast("COffsetInitInfo", init)
+            args = [self.dictionary.index_offset(init.offset, fid=fid)]
+            return self.mk_offset_init_index(init.tags, args)
 
     def index_offset_init(self, oinit: COffsetInitInfo, fid: int = -1) -> int:
         args: List[int] = [
diff --git a/chc/app/CHVersion.py b/chc/app/CHVersion.py
index 8c97256..7499ea5 100644
--- a/chc/app/CHVersion.py
+++ b/chc/app/CHVersion.py
@@ -1 +1 @@
-chcversion: str = "0.2.0-2024-12-04"
+chcversion: str = "0.2.0-2025-12-06"
diff --git a/chc/app/CInitInfo.py b/chc/app/CInitInfo.py
index b7463c3..ff8a58f 100644
--- a/chc/app/CInitInfo.py
+++ b/chc/app/CInitInfo.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
@@ -32,6 +32,7 @@
 
 from chc.app.CDictionaryRecord import CDeclarationsRecord
 
+import chc.util.fileutil as UF
 import chc.util.IndexedTable as IT
 
 if TYPE_CHECKING:
@@ -39,6 +40,7 @@
     from chc.app.CTyp import CTyp
     from chc.app.CDeclarations import CDeclarations
     from chc.app.COffset import COffset
+    from chc.app.CVisitor import CVisitor
 
 
 class CInitInfo(CDeclarationsRecord):
@@ -55,6 +57,13 @@ def is_single(self) -> bool:
     def is_compound(self) -> bool:
         return False
 
+    @property
+    def is_offset(self) -> bool:
+        return False
+
+    def accept(self, visitor: "CVisitor") -> None:
+        raise UF.CHCError("visitor not yet implemented for " + str(self))
+
 
 class CSingleInitInfo(CInitInfo):
     """Initializer of a simple variable.
@@ -73,6 +82,9 @@ def exp(self) -> "CExp":
     def is_single(self) -> bool:
         return True
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_single_initinfo(self)
+
     def __str__(self) -> str:
         return str(self.exp)
 
@@ -90,19 +102,30 @@ def __init__(self, decls: "CDeclarations", ixval: IT.IndexedTableValue):
     def typ(self) -> "CTyp":
         return self.dictionary.get_typ(self.args[0])
 
+    @property
+    def is_compound(self) -> bool:
+        return True
+
     @property
     def offset_initializers(self) -> List["COffsetInitInfo"]:
         return [self.decls.get_offset_init(x) for x in self.args[1:]]
 
     @property
-    def is_compound(self) -> bool:
-        return True
+    def is_struct(self) -> bool:
+        return self.typ.is_struct
+
+    @property
+    def is_union(self) -> bool:
+        return self.typ.is_union
+
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_compound_initinfo(self)
 
     def __str__(self) -> str:
         return "\n".join([str(x) for x in self.offset_initializers])
 
 
-class COffsetInitInfo(CDeclarationsRecord):
+class COffsetInitInfo(CInitInfo):
     """Component of a compound initializer.
 
     - args[0]: index of offset expression in cdictionary
@@ -116,9 +139,16 @@ def __init__(self, decls: "CDeclarations", ixval: IT.IndexedTableValue):
     def offset(self) -> "COffset":
         return self.dictionary.get_offset(self.args[0])
 
+    @property
+    def is_offset(self) -> bool:
+        return True
+
     @property
     def initializer(self) -> CInitInfo:
         return self.decls.get_initinfo(self.args[1])
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_offset_initinfo(self)
+
     def __str__(self) -> str:
         return str(self.offset) + ":=" + str(self.initializer)
diff --git a/chc/app/CInstr.py b/chc/app/CInstr.py
index 0808659..fade09a 100644
--- a/chc/app/CInstr.py
+++ b/chc/app/CInstr.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,8 +39,10 @@
     from chc.app.CFile import CFile
     from chc.app.CFileDictionary import CFileDictionary
     from chc.app.CFunction import CFunction
+    from chc.app.CLocation import CLocation
     from chc.app.CLval import CLval
     from chc.app.CStmt import CStmt
+    from chc.app.CVisitor import CVisitor
 
 
 class CInstr:
@@ -62,6 +64,10 @@ def cfun(self) -> "CFunction":
     def cdictionary(self) -> "CFileDictionary":
         return self.parent.cdictionary
 
+    @property
+    def location(self) -> "CLocation":
+        return self.cfun.cfiledecls.read_xml_location(self.xnode)
+
     @property
     def is_assign(self) -> bool:
         return False
@@ -81,13 +87,15 @@ def strings(self) -> List[str]:
     def get_variable_uses(self, vid: int) -> int:
         return 0
 
+    def accept(self, visitor: "CVisitor") -> None:
+        raise UF.CHCError("visitor not yet accepted on: " + str(self))
+
 
 class CCallInstr(CInstr):
     """Call instruction."""
 
     def __init__(self, parent: "CStmt", xnode: ET.Element) -> None:
         CInstr.__init__(self, parent, xnode)
-        self._lhs: Optional["CLval"] = None
         self._callee: Optional["CExp"] = None
         self._callargs: Optional[List["CExp"]] = None
 
@@ -96,14 +104,12 @@ def is_call(self) -> bool:
         return True
 
     @property
-    def lhs(self) -> "CLval":
-        if self._lhs is None:
-            xlval = self.xnode.get("ilval")
-            if xlval is not None:
-                self._lhs = self.cdictionary.get_lval(int(xlval))
-            else:
-                raise UF.CHCError("call instruction does not have an lval")
-        return self._lhs
+    def lhs(self) -> Optional["CLval"]:
+        xlval = self.xnode.get("ilval")
+        if xlval is not None:
+            return self.cdictionary.get_lval(int(xlval))
+        else:
+            return None
 
     @property
     def callee(self) -> "CExp":
@@ -141,10 +147,16 @@ def has_lhs(self) -> bool:
         return "ilval" in self.xnode.attrib
 
     def get_variable_uses(self, vid: int) -> int:
-        lhsuse = self.lhs.get_variable_uses(vid) if self.has_lhs() else 0
-        arguse = sum([a.get_variable_uses(vid) for a in self.callargs])
-        calleeuse = self.callee.get_variable_uses(vid)
-        return lhsuse + arguse + calleeuse
+        if self.lhs is not None:
+            lhsuse = self.lhs.get_variable_uses(vid) if self.has_lhs() else 0
+            arguse = sum([a.get_variable_uses(vid) for a in self.callargs])
+            calleeuse = self.callee.get_variable_uses(vid)
+            return lhsuse + arguse + calleeuse
+        else:
+            return 0
+
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_call_instr(self)
 
     def __str__(self) -> str:
         return "      call " + str(self.callee)
@@ -193,6 +205,9 @@ def get_variable_uses(self, vid: int) -> int:
         rhsuse = self.rhs.get_variable_uses(vid)
         return lhsuse + rhsuse
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_assign_instr(self)
+
     def __str__(self) -> str:
         return "     assign: " + str(self.lhs) + " := " + str(self.rhs)
 
@@ -243,6 +258,9 @@ def templates(self) -> List[str]:
                         self._templates.append(ts)
         return self._templates
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_asm_instr(self)
+
     def __str__(self) -> str:
         lines: List[str] = []
         for s in self.templates:
@@ -279,6 +297,9 @@ def lhs(self) -> "CLval":
     def constraint(self) -> str:
         return self.xnode.get("constraint", "none")
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_asm_output(self)
+
     def __str__(self) -> str:
         return self.constraint + "; lval: " + str(self.lhs)
 
@@ -308,5 +329,8 @@ def exp(self) -> "CExp":
     def constraint(self) -> str:
         return self.xnode.get("constraint", "none")
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_asm_input(self)
+
     def __str__(self) -> str:
         return self.constraint + "; exp: " + str(self.exp)
diff --git a/chc/app/CLHost.py b/chc/app/CLHost.py
index 5b85bfa..caadb7a 100644
--- a/chc/app/CLHost.py
+++ b/chc/app/CLHost.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
@@ -32,11 +32,13 @@
 
 from chc.app.CDictionaryRecord import CDictionaryRecord, cdregistry
 
+import chc.util.fileutil as UF
 import chc.util.IndexedTable as IT
 
 if TYPE_CHECKING:
     from chc.app.CDictionary import CDictionary
     from chc.app.CExp import CExp
+    from chc.app.CVisitor import CVisitor
 
 
 class CLHost(CDictionaryRecord):
@@ -75,6 +77,9 @@ def get_variable_uses(self, vid: int) -> int:
     def to_dict(self) -> Dict[str, object]:
         return {"base": "lhost"}
 
+    def accept(self, visitor: "CVisitor") -> None:
+        raise UF.CHCError("visitor not implemented for: " + str(self))
+
     def __str__(self) -> str:
         return "lhostbase:" + self.tags[0]
 
@@ -115,6 +120,9 @@ def get_variable_uses(self, vid: int) -> int:
     def to_dict(self) -> Dict[str, object]:
         return {"base": "var", "var": self.name}
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_lhostvar(self)
+
     def __str__(self) -> str:
         return self.name
 
@@ -152,5 +160,8 @@ def has_variable_deref(self, vid: int) -> bool:
     def to_dict(self) -> Dict[str, object]:
         return {"base": "mem", "exp": self.exp.to_dict()}
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_lhostmem(self)
+
     def __str__(self) -> str:
         return "(*" + str(self.exp) + ")"
diff --git a/chc/app/CLocation.py b/chc/app/CLocation.py
index dabb57d..9522f0a 100644
--- a/chc/app/CLocation.py
+++ b/chc/app/CLocation.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 @@
 if TYPE_CHECKING:
     from chc.app.CDeclarations import CDeclarations
     from chc.app.CFileDeclarations import CFileDeclarations
+    from chc.app.CVisitor import CVisitor
 
 
 class CLocation(CDeclarationsRecord):
@@ -68,6 +69,9 @@ def file(self) -> str:
     def get_loc(self) -> Tuple[str, int, int]:
         return (self.file, self.line, self.byte)
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_location(self)
+
     def __ge__(self, loc: "CLocation") -> bool:
         return self.get_loc() >= loc.get_loc()
 
diff --git a/chc/app/CLval.py b/chc/app/CLval.py
index a45bae4..851644a 100644
--- a/chc/app/CLval.py
+++ b/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-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
@@ -38,6 +38,7 @@
     from chc.app.CDictionary import CDictionary
     from chc.app.CLHost import CLHost
     from chc.app.COffset import COffset
+    from chc.app.CVisitor import CVisitor
 
 
 class CLval(CDictionaryRecord):
@@ -77,6 +78,9 @@ def has_variable_deref(self, vid: int) -> bool:
     def has_ref_type(self) -> bool:
         return self.lhost.has_ref_type()
 
+    def is_var(self) -> bool:
+        return self.lhost.is_var
+
     def to_dict(self) -> Dict[str, object]:
         return {
             "lhost": self.lhost.to_dict(),
@@ -86,5 +90,8 @@ def to_dict(self) -> Dict[str, object]:
     def to_idict(self) -> Dict[str, object]:
         return {"t": self.tags, "a": self.args}
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_lval(self)
+
     def __str__(self) -> str:
         return str(self.lhost) + str(self.offset)
diff --git a/chc/app/COffset.py b/chc/app/COffset.py
index d9fe0b2..453031e 100644
--- a/chc/app/COffset.py
+++ b/chc/app/COffset.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
@@ -32,11 +32,13 @@
 
 from chc.app.CDictionaryRecord import CDictionaryRecord, cdregistry
 
+import chc.util.fileutil as UF
 import chc.util.IndexedTable as IT
 
 if TYPE_CHECKING:
     from chc.app.CDictionary import CDictionary
     from chc.app.CExp import CExp
+    from chc.app.CVisitor import CVisitor
 
 
 class COffset(CDictionaryRecord):
@@ -69,6 +71,9 @@ def get_variable_uses(self, vid: int) -> int:
     def to_dict(self) -> Dict[str, object]:
         return {"base": "offset"}
 
+    def accept(self, visitor: "CVisitor") -> None:
+        raise UF.CHCError("visitor not implemented for: " + str(self))
+
     def __str__(self) -> str:
         return "offsetbase:" + self.tags[0]
 
@@ -89,6 +94,9 @@ def is_no_offset(self) -> bool:
     def to_dict(self) -> Dict[str, object]:
         return {"base": "no-offset"}
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_nooffset(self)
+
     def __str__(self) -> str:
         return ""
 
@@ -129,6 +137,9 @@ def to_dict(self) -> Dict[str, object]:
             result["offset"] = self.offset.to_dict()
         return result
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_fieldoffset(self)
+
     def __str__(self) -> str:
         offset = str(self.offset) if self.has_offset() else ""
         return "." + self.fieldname + offset
@@ -169,6 +180,9 @@ def to_dict(self) -> Dict[str, object]:
             result["offset"] = self.offset.to_dict()
         return result
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_indexoffset(self)
+
     def __str__(self) -> str:
         offset = str(self.offset) if self.has_offset() else ""
         return "[" + str(self.index_exp) + "]" + offset
diff --git a/chc/app/CPrettyPrinter.py b/chc/app/CPrettyPrinter.py
index af1bfd6..54ce2af 100644
--- a/chc/app/CPrettyPrinter.py
+++ b/chc/app/CPrettyPrinter.py
@@ -29,11 +29,27 @@
 
 import chc.app.CAttributes as CA
 import chc.app.CExp as CE
+import chc.app.CInstr as CI
+import chc.app.CLHost as CH
+import chc.app.CLval as CL
+import chc.app.COffset as CO
+import chc.app.CStmt as CS
 import chc.app.CTyp as CT
 from chc.app.CVarInfo import CVarInfo
 
 from chc.app.CVisitor import CVisitor
 
+if TYPE_CHECKING:
+    from chc.app.CFileGlobals import CGCompTag, CGType, CGVarDef
+    from chc.app.CCompInfo import CCompInfo
+    from chc.app.CFieldInfo import CFieldInfo
+    from chc.app.CFunction import CFunction
+    from chc.app.CInitInfo import CSingleInitInfo, CCompoundInitInfo
+    from chc.app.CLocation import CLocation
+    from chc.app.CInitInfo import (
+        CSingleInitInfo, CCompoundInitInfo, COffsetInitInfo)
+    from chc.app.CTypeInfo import CTypeInfo
+
 
 integernames = {
     "ichar": "char",
@@ -50,6 +66,33 @@
     "iulonglong": "unsigned long long",
 }
 
+
+operators = {
+    "band": " & ",
+    "bor": " | ",
+    "bxor": " ^ ",
+    "div": " / ",
+    "eq": " == ",
+    "ge": " >= ",
+    "gt": " > ",
+    "indexpi": " + ",
+    "land": " && ",
+    "le": " <= ",
+    "lor": " || ",
+    "lt": " < ",
+    "minusa": " - ",
+    "minuspi": " - ",
+    "minuspp": " - ",
+    "mod": " % ",
+    "mult": " * ",
+    "ne": " != ",
+    "plusa": " + ",
+    "pluspi": " + ",
+    "shiftlt": " << ",
+    "shiftrt": " >> "
+}
+
+
 floatnames = {"float": "float", "fdouble": "double", "flongdouble": "long double"}
 
 
@@ -86,6 +129,32 @@ def __init__(self, indentation: int = 2) -> None:
         self._indent = 0
         self._ccode = CPrettyCode()
 
+    def cgtypedef_str(self, gty: "CGType") -> str:
+        gty.accept(self)
+        return str(self.ccode)
+
+    def cgcomptag_str(self, gcomp: "CGCompTag") -> str:
+        gcomp.accept(self)
+        return str(self.ccode)
+
+    def cgvardef_str(self, gvardef: "CGVarDef") -> str:
+        gvardef.accept(self)
+        return str(self.ccode)
+
+    def function_definition_to_string(self, cfun: "CFunction") -> str:
+        self.write_function_signature(cfun.svar)
+        self.ccode.write(" {")
+        self.ccode.newline(indent=self.indent)
+        self.increase_indent()
+        if len(cfun.locals) > 0:
+            self.write_function_locals(list(cfun.locals.values()))
+            self.ccode.newline(indent=self.indent)
+        cfun.sbody.accept(self)
+        self.decrease_indent()
+        self.ccode.newline(indent=self.indent)
+        self.ccode.write("}")
+        return str(self.ccode)
+
     @property
     def indentation(self) -> int:
         return self._indentation
@@ -104,6 +173,78 @@ def increase_indent(self) -> None:
     def decrease_indent(self) -> None:
         self._indent -= self.indentation
 
+    def visit_location(self, loc: "CLocation") -> None:
+        self.ccode.newline(indent=0)
+        self.ccode.write(f"// {loc.file}:{loc.line}:{loc.byte}")
+
+    def visit_cgtype(self, cgtype: "CGType") -> None:
+        cgtype.location.accept(self)
+        cgtype.typeinfo.accept(self)
+
+    def visit_cgcomptag(self, cgcomptag: "CGCompTag") -> None:
+        cgcomptag.location.accept(self)
+        self.ccode.newline(indent=0)
+        if cgcomptag.is_struct:
+            self.ccode.write(f"struct {cgcomptag.name}")
+        else:
+            self.ccode.write(f"union {cgcomptag.name}")
+        self.ccode.write(" {")
+        self.increase_indent()
+        cgcomptag.compinfo.accept(self)
+        self.decrease_indent()
+        self.ccode.newline()
+        self.ccode.write("}")
+
+    def visit_cgvardef(self, cgvardef: "CGVarDef") -> None:
+        cgvardef.location.accept(self)
+        self.ccode.newline(indent=0)
+        cgvardef.varinfo.vtype.accept(self)
+        self.ccode.write(" ")
+        self.ccode.write(cgvardef.vname)
+        if cgvardef.initializer is not None:
+            self.ccode.write(" = ")
+            cgvardef.initializer.accept(self)
+
+    def visit_typeinfo(self, typeinfo: "CTypeInfo") -> None:
+        self.ccode.newline(indent=0)
+        self.ccode.write("typedef ")
+        typeinfo.type.accept(self)
+        self.ccode.write(" ")
+        self.ccode.write(typeinfo.name)
+        self.ccode.write(";")
+
+    def visit_compinfo(self, compinfo: "CCompInfo") -> None:
+        for field in compinfo.fields:
+            field.accept(self)
+
+    def visit_fieldinfo(self, fieldinfo: "CFieldInfo") -> None:
+        self.ccode.newline(indent=self.indent)
+        fieldinfo.ftype.accept(self)
+        self.ccode.write(f" {fieldinfo.fname};")
+
+    def visit_single_initinfo(self, initinfo: "CSingleInitInfo") -> None:
+        initinfo.exp.accept(self)
+
+    def visit_compound_initinfo(self, initinfo: "CCompoundInitInfo") -> None:
+        if initinfo.typ.is_struct or initinfo.typ.is_union:
+            self.ccode.write("{")
+        else:
+            self.ccode.write("]")
+        if len(initinfo.offset_initializers) > 0:
+            for oi in initinfo.offset_initializers[:-1]:
+                oi.accept(self)
+                self.ccode.write(", ")
+            initinfo.offset_initializers[-1].accept(self)
+        if initinfo.typ.is_struct or initinfo.is_union:
+            self.ccode.write("}")
+        else:
+            self.ccode.write("]")
+
+    def visit_offset_initinfo(self, initinfo: "COffsetInitInfo") -> None:
+        initinfo.offset.accept(self)
+        self.ccode.write(" = ")
+        initinfo.initializer.accept(self)
+
     def visit_voidtyp(self, t: CT.CTypVoid) -> None:
         t.attributes.accept(self)
         self.ccode.write("void")
@@ -228,6 +369,15 @@ def function_declaration_str(
         if not vinfo.vtype.is_function:
             return "error"
 
+        self.write_function_signature(vinfo, srcloc=srcloc, binloc=binloc)
+        self.ccode.write(";")
+        return str(self.ccode)
+
+    def write_function_signature(
+            self,
+            vinfo: CVarInfo,
+            srcloc: Optional[str] = None,
+            binloc: Optional[str] = None) -> None:
         self.ccode.newline()
         ftype = cast(CT.CTypFun, vinfo.vtype)
         if ftype.return_type.is_function_pointer:
@@ -245,10 +395,6 @@ def function_declaration_str(
             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(" ")
@@ -261,9 +407,14 @@ def function_declaration_str(
         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 write_function_locals(self, vinfos: List["CVarInfo"]) -> None:
+        for vinfo in vinfos:
+            self.ccode.newline(indent=self.indent)
+            vinfo.vtype.accept(self)
+            self.ccode.write(" ")
+            self.ccode.write(vinfo.vname)
+            self.ccode.write(";")
 
     def funtypptr_with_name(self, t: CT.CTypFun, name: str) -> None:
         if t.return_type.is_function_pointer:
@@ -353,6 +504,7 @@ def ptrarg_with_attribute_length(
         self.ccode.write(str(aparam.intvalue))
         self.ccode.write("]")
 
+    '''
     def visit_attributes(self, a: CA.CAttributes) -> None:
         if a.length == 0:
             return
@@ -362,6 +514,237 @@ def visit_attributes(self, a: CA.CAttributes) -> None:
             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))
+
+    def function_body_str(self, cbody: CS.CFunctionBody) -> str:
+        self.ccode.newline()
+        cbody.accept(self)
+        return str(self.ccode)
+
+    def visit_block(self, cblock: CS.CBlock) -> None:
+        for stmt in cblock.stmts.values():
+            stmt.accept(self)
+
+    def visit_function_body(self, cbody: CS.CFunctionBody) -> None:
+        for stmt in cbody.stmts.values():
+            stmt.accept(self)
+
+    def visit_if_stmt(self, ifstmt: CS.CIfStmt) -> None:
+        self.ccode.newline(indent=self.indent)
+        self.ccode.write("if (")
+        ifstmt.condition.accept(self)
+        self.ccode.write(") {")
+        if ifstmt.ifstmt is not None:
+            self.increase_indent()
+            ifstmt.ifstmt.accept(self)
+            self.decrease_indent()
+            self.ccode.newline(indent=self.indent)
+        if ifstmt.elsestmt is not None:
+            self.ccode.write("} else {")
+            self.increase_indent()
+            ifstmt.elsestmt.accept(self)
+            self.decrease_indent()
+            self.ccode.newline(indent=self.indent)
+        self.ccode.write("}")
+
+    def visit_loop_stmt(self, loopstmt: CS.CLoopStmt) -> None:
+        pass
+
+    def visit_switch_stmt(self, switchstmt: CS.CSwitchStmt) -> None:
+        pass
+
+    def visit_break_stmt(self, breakstmt: CS.CBreakStmt) -> None:
+        pass
+
+    def visit_continue_stmt(self, continuestmt: CS.CContinueStmt) -> None:
+        pass
+
+    def visit_goto_stmt(self, gotostmt: CS.CGotoStmt) -> None:
+        pass
+
+    def visit_return_stmt(self, returnstmt: CS.CReturnStmt) -> None:
+        returnstmt.location.accept(self)
+        self.ccode.newline(indent=self.indent)
+        if returnstmt.exp is not None:
+            self.ccode.write("return ")
+            returnstmt.exp.accept(self)
+            self.ccode.write(";")
+        else:
+            self.ccode.write("return;")
+
+    def visit_instrs_stmt(self, instrsstmt: CS.CInstrsStmt) -> None:
+        for instr in instrsstmt.instrs:
+            instr.accept(self)
+
+    def visit_assign_instr(self, assigninstr: CI.CAssignInstr) -> None:
+        self.ccode.newline(indent=self.indent)
+        assigninstr.lhs.accept(self)
+        self.ccode.write(" = ")
+        assigninstr.rhs.accept(self)
+        self.ccode.write(";")
+
+    def visit_call_instr(self, callinstr: CI.CCallInstr) -> None:
+        self.ccode.newline(indent=self.indent)
+        if callinstr.lhs is not None:
+            callinstr.lhs.accept(self)
+            self.ccode.write(" = ")
+        callinstr.callee.accept(self)
+        self.ccode.write("(")
+        if len(callinstr.callargs) > 0:
+            for a in callinstr.callargs[:-1]:
+                a.accept(self)
+                self.ccode.write(", ")
+            callinstr.callargs[-1].accept(self)
+        self.ccode.write(");")
+
+    def visit_asm_instr(self, asminstr: CI.CAsmInstr) -> None:
+        pass
+
+    def visit_asm_output(self, asmoutput: CI.CAsmOutput) -> None:
+        pass
+
+    def visit_asm_input(self, asminput: CI.CAsmInput) -> None:
+        pass
+
+    def visit_lval(self, lval: CL.CLval) -> None:
+        lval.lhost.accept(self)
+        lval.offset.accept(self)
+
+    def visit_lhostvar(self, lhostvar: CH.CLHostVar) -> None:
+        self.ccode.write(lhostvar.name)
+
+    def visit_lhostmem(self, lhostmem: CH.CLHostMem) -> None:
+        self.ccode.write("*(")
+        lhostmem.exp.accept(self)
+        self.ccode.write(")")
+
+    def visit_nooffset(self, nooffset: CO.CNoOffset) -> None:
+        pass
+
+    def visit_fieldoffset(self, fieldoffset: CO.CFieldOffset) -> None:
+        self.ccode.write(".")
+        self.ccode.write(fieldoffset.fieldname)
+        fieldoffset.offset.accept(self)
+
+    def visit_indexoffset(self, indexoffset: CO.CIndexOffset) -> None:
+        pass
+
+    def visit_explval(self, explval: CE.CExpLval) -> None:
+        explval.lval.accept(self)
+
+    def visit_sizeof(self, sizeof: CE.CExpSizeOf) -> None:
+        pass
+
+    def visit_sizeofe(self, sizeofe: CE.CExpSizeOfE) -> None:
+        pass
+
+    def visit_size_of_str(self, sizeofstr: CE.CExpSizeOfStr) -> None:
+        pass
+
+    def visit_alignof(self, alignof: CE.CExpAlignOf) -> None:
+        pass
+
+    def visit_alignofe(self, alignofe: CE.CExpAlignOfE) -> None:
+        pass
+
+    def visit_unop(self, unop: CE.CExpUnOp) -> None:
+        pass
+
+    def visit_binop(self, binop: CE.CExpBinOp) -> None:
+        self.ccode.write("(")
+        binop.exp1.accept(self)
+        self.ccode.write(operators[binop.op])
+        binop.exp2.accept(self)
+        self.ccode.write(")")
+
+    def visit_question(self, question: CE.CExpQuestion) -> None:
+        pass
+
+    def visit_cast(self, ecast: CE.CExpCastE) -> None:
+        self.ccode.write("(")
+        ecast.typ.accept(self)
+        self.ccode.write(")")
+        ecast.exp.accept(self)
+
+    def visit_addrof(self, addrof: CE.CExpAddrOf) -> None:
+        if addrof.lval.is_var:
+            self.ccode.write("&")
+            addrof.lval.accept(self)
+        else:
+            self.ccode.write("&(")
+            addrof.lval.accept(self)
+            self.ccode.write(")")
+
+    def visit_addr_of_label(self, addroflabel: CE.CExpAddrOfLabel) -> None:
+        pass
+
+    def visit_startof(self, startof: CE.CExpStartOf) -> None:
+        pass
+
+    def visit_fn_app(self, fnapp: CE.CExpFnApp) -> None:
+        pass
+
+    def visit_cn_app(self, cnapp: CE.CExpCnApp) -> None:
+        pass
+
+    def visit_attributes(self, a: CA.CAttributes) -> None:
+        for attr in a.attributes:
+            attr.accept(self)
+
+    def visit_attribute(self, a: CA.CAttribute) -> None:
+        if len(a.params) == 0:
+            self.ccode.write(a.name)
+            self.ccode.write(" ")
+        else:
+            self.ccode.write("attribute not yet supported " + str(a))
+
+    def visit_attr_int(self, a: CA.CAttrInt) -> None:
+        pass
+
+    def visit_attr_str(self, a: CA.CAttrStr) -> None:
+        pass
+
+    def visit_attr_cons(self, a: CA.CAttrCons) -> None:
+        pass
+
+    def visit_attr_sizeof(self, a: CA.CAttrSizeOf) -> None:
+        pass
+
+    def visit_attr_sizeofe(self, a: CA.CAttrSizeOfE) -> None:
+        pass
+
+    def visit_attr_sizeofs(self, a: CA.CAttrSizeOfS) -> None:
+        pass
+
+    def visit_attr_alignof(self, a: CA.CAttrAlignOf) -> None:
+        pass
+
+    def visit_attr_alignofe(self, a: CA.CAttrAlignOfE) -> None:
+        pass
+
+    def visit_attr_alignofs(self, a: CA.CAttrAlignOfS) -> None:
+        pass
+
+    def visit_attr_unop(self, a: CA.CAttrUnOp) -> None:
+        pass
+
+    def visit_attr_binop(self, a: CA.CAttrBinOp) -> None:
+        pass
+
+    def visit_attr_dot(self, a: CA.CAttrDot) -> None:
+        pass
+
+    def visit_attr_star(self, a: CA.CAttrStar) -> None:
+        pass
+
+    def visit_attr_addrof(self, a: CA.CAttrAddrOf) -> None:
+        pass
+
+    def visit_attr_index(self, a: CA.CAttrIndex) -> None:
+        pass
+
+    def visit_attr_question(self, a: CA.CAttrQuestion) -> None:
+        pass
diff --git a/chc/app/CStmt.py b/chc/app/CStmt.py
index 2901d6c..be9b871 100644
--- a/chc/app/CStmt.py
+++ b/chc/app/CStmt.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,8 +39,11 @@
 if TYPE_CHECKING:
     from chc.app.CExp import CExp
     from chc.app.CFile import CFile
+    from chc.app.CFileDeclarations import CFileDeclarations
     from chc.app.CFileDictionary import CFileDictionary
     from chc.app.CFunction import CFunction
+    from chc.app.CLocation import CLocation
+    from chc.app.CVisitor import CVisitor
 
 
 stmt_constructors: Dict[str, Callable[["CStmt", ET.Element], "CStmt"]] = {
@@ -93,6 +96,10 @@ def cfun(self) -> "CFunction":
     def cfile(self) -> "CFile":
         return self.cfun.cfile
 
+    @property
+    def declarations(self) -> "CFileDeclarations":
+        return self.cfile.declarations
+
     @property
     def cdictionary(self) -> "CFileDictionary":
         return self.cfile.dictionary
@@ -121,6 +128,14 @@ def kind(self) -> str:
         else:
             raise UF.CHCError("stag missing from stmt")
 
+    @property
+    def location(self) -> "CLocation":
+        xiloc = self.xskind.get("iloc")
+        if xiloc is not None:
+            return self.declarations.get_location(int(xiloc))
+        else:
+            raise UF.CHCError("No location found in statement " + str(self))
+
     @property
     def preds(self) -> List[int]:
         if self._preds is None:
@@ -190,6 +205,9 @@ def strings(self) -> List[str]:
     def get_variable_uses(self, vid: int) -> int:
         return sum(s.get_variable_uses(vid) for s in self.stmts.values())
 
+    def accept(self, visitor: "CVisitor") -> None:
+        raise UF.CHCError("visitor not yet accepted on: " + str(self))
+
     def __str__(self) -> str:
         lines: List[str] = []
         predecessors = ",".join(str(p) for p in self.preds)
@@ -235,6 +253,9 @@ def is_block_stmt(self) -> bool:
     def block_count(self) -> int:
         return sum(s.block_count for s in self.stmts.values()) + 1
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_block(self)
+
 
 class CFunctionBody(CBlock):
 
@@ -250,6 +271,9 @@ def cfun(self) -> "CFunction":
     def is_function_body(self) -> bool:
         return self.parent is None
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_function_body(self)
+
 
 class CIfStmt(CStmt):
 
@@ -273,6 +297,22 @@ def stmts(self) -> Dict[int, "CStmt"]:
                     self._stmts[s.sid] = s
         return self._stmts
 
+    @property
+    def ifstmt(self) -> Optional["CStmt"]:
+        xthen = self.xskind.find("thenblock")
+        if xthen is not None:
+            return CBlock(self, xthen)
+        else:
+            return None
+
+    @property
+    def elsestmt(self) -> Optional["CStmt"]:
+        xelse = self.xskind.find("elseblock")
+        if xelse is not None:
+            return CBlock(self, xelse)
+        else:
+            return None
+
     @property
     def condition(self) -> "CExp":
         xiexp = self.xskind.get("iexp")
@@ -294,6 +334,9 @@ def get_variable_uses(self, vid: int) -> int:
         result: int = sum(s.get_variable_uses(vid) for s in self.stmts.values())
         return result + self.condition.get_variable_uses(vid)
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_if_stmt(self)
+
     def __str__(self) -> str:
         return CStmt.__str__(self) + ": " + str(self.condition)
 
@@ -317,6 +360,9 @@ def stmts(self) -> Dict[int, "CStmt"]:
                 raise UF.CHCError("Loop stmt without nested block")
         return self._stmts
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_loop_stmt(self)
+
 
 class CSwitchStmt(CStmt):
 
@@ -337,24 +383,36 @@ def stmts(self) -> Dict[int, "CStmt"]:
                 raise UF.CHCError("Switch stmt without nested block")
         return self._stmts
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_switch_stmt(self)
+
 
 class CBreakStmt(CStmt):
 
     def __init__(self, parent: "CStmt", xnode: ET.Element) -> None:
         CStmt.__init__(self, parent, xnode)
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_break_stmt(self)
+
 
 class CContinueStmt(CStmt):
 
     def __init__(self, parent: "CStmt", xnode: ET.Element) -> None:
         CStmt.__init__(self, parent, xnode)
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_continue_stmt(self)
+
 
 class CGotoStmt(CStmt):
 
     def __init__(self, parent: "CStmt", xnode: ET.Element) -> None:
         CStmt.__init__(self, parent, xnode)
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_goto_stmt(self)
+
 
 class CReturnStmt(CStmt):
     """Function return."""
@@ -362,6 +420,17 @@ class CReturnStmt(CStmt):
     def __init__(self, parent: "CStmt", xnode: ET.Element) -> None:
         CStmt.__init__(self, parent, xnode)
 
+    @property
+    def exp(self) -> Optional["CExp"]:
+        xreturnval = self.xskind.get("iexp")
+        if xreturnval is not None:
+            return self.cdictionary.get_exp(int(xreturnval))
+        else:
+            return None
+
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_return_stmt(self)
+
 
 class CInstrsStmt(CStmt):
     """Sequence of instructions without control flow."""
@@ -391,6 +460,8 @@ def instrs(self) -> List[CInstr]:
                     self._instrs.append(CAssignInstr(self, xinode))
                 elif xitag == "asm":
                     self._instrs.append(CAsmInstr(self, xinode))
+                elif xitag == "vardecl":
+                    pass
                 else:
                     raise UF.CHCError("unknown instruction tag: " + xitag)
         return self._instrs
@@ -403,6 +474,9 @@ def call_instrs(self) -> List["CCallInstr"]:
                 result.append(cast("CCallInstr", i))
         return result
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_instrs_stmt(self)
+
     def __str__(self) -> str:
         lines: List[str] = []
         lines.append(CStmt.__str__(self))
diff --git a/chc/app/CTypeInfo.py b/chc/app/CTypeInfo.py
index 3442eb3..026a99c 100644
--- a/chc/app/CTypeInfo.py
+++ b/chc/app/CTypeInfo.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
@@ -37,6 +37,7 @@
 if TYPE_CHECKING:
     from chc.app.CDeclarations import CDeclarations
     from chc.app.CTyp import CTyp
+    from chc.app.CVisitor import CVisitor
 
 
 class CTypeInfo(CDeclarationsRecord):
@@ -58,5 +59,8 @@ def name(self) -> str:
     def type(self) -> "CTyp":
         return self.dictionary.get_typ(self.args[0])
 
+    def accept(self, visitor: "CVisitor") -> None:
+        visitor.visit_typeinfo(self)
+
     def __str__(self) -> str:
         return self.name + ":" + str(self.type)
diff --git a/chc/app/CVisitor.py b/chc/app/CVisitor.py
index 0844c5d..61cb9c2 100644
--- a/chc/app/CVisitor.py
+++ b/chc/app/CVisitor.py
@@ -28,17 +28,133 @@
 
 from abc import ABC, abstractmethod
 
+from typing import TYPE_CHECKING
+
 import chc.app.CAttributes as CA
 import chc.app.CExp as CE
+import chc.app.CInstr as CI
+import chc.app.CLHost as CH
+import chc.app.CLval as CL
+import chc.app.COffset as CO
+import chc.app.CStmt as CS
 import chc.app.CTyp as CT
 from chc.app.CVarInfo import CVarInfo
 
+if TYPE_CHECKING:
+    from chc.app.CFileGlobals import CGCompTag, CGType, CGVarDef
+    from chc.app.CCompInfo import CCompInfo
+    from chc.app.CFieldInfo import CFieldInfo
+    from chc.app.CInitInfo import (
+        CSingleInitInfo, CCompoundInitInfo, COffsetInitInfo)
+    from chc.app.CLocation import CLocation
+    from chc.app.CTypeInfo import CTypeInfo
+
 
 class CVisitor(ABC):
 
     def __init__(self) -> None:
         pass
 
+    @abstractmethod
+    def visit_location(self, loc: "CLocation") -> None:
+        ...
+
+    @abstractmethod
+    def visit_cgtype(self, cgtype: "CGType") -> None:
+        ...
+
+    @abstractmethod
+    def visit_cgcomptag(self, cgcomptag: "CGCompTag") -> None:
+        ...
+
+    @abstractmethod
+    def visit_cgvardef(self, cgvardef: "CGVarDef") -> None:
+        ...
+
+    @abstractmethod
+    def visit_typeinfo(self, typeinfo: "CTypeInfo") -> None:
+        ...
+
+    @abstractmethod
+    def visit_compinfo(self, compinfo: "CCompInfo") -> None:
+        ...
+
+    @abstractmethod
+    def visit_fieldinfo(self, fieldinfo: "CFieldInfo") -> None:
+        ...
+
+    @abstractmethod
+    def visit_single_initinfo(self, initinfo: "CSingleInitInfo") -> None:
+        ...
+
+    @abstractmethod
+    def visit_compound_initinfo(self, initinfo: "CCompoundInitInfo") -> None:
+        ...
+
+    @abstractmethod
+    def visit_offset_initinfo(self, initinfo: "COffsetInitInfo") -> None:
+        ...
+
+    @abstractmethod
+    def visit_block(self, cblock: CS.CBlock) -> None:
+        ...
+
+    @abstractmethod
+    def visit_function_body(self, cbody: CS.CFunctionBody) -> None:
+        ...
+
+    @abstractmethod
+    def visit_if_stmt(self, ifstmt: CS.CIfStmt) -> None:
+        ...
+
+    @abstractmethod
+    def visit_loop_stmt(self, loopstmt: CS.CLoopStmt) -> None:
+        ...
+
+    @abstractmethod
+    def visit_switch_stmt(self, switchstmt: CS.CSwitchStmt) -> None:
+        ...
+
+    @abstractmethod
+    def visit_break_stmt(self, breakstmt: CS.CBreakStmt) -> None:
+        ...
+
+    @abstractmethod
+    def visit_continue_stmt(self, continuestmt: CS.CContinueStmt) -> None:
+        ...
+
+    @abstractmethod
+    def visit_goto_stmt(self, gotostmt: CS.CGotoStmt) -> None:
+        ...
+
+    @abstractmethod
+    def visit_return_stmt(self, returnstmt: CS.CReturnStmt) -> None:
+        ...
+
+    @abstractmethod
+    def visit_instrs_stmt(self, instrsstmt: CS.CInstrsStmt) -> None:
+        ...
+
+    @abstractmethod
+    def visit_assign_instr(self, assigninstr: CI.CAssignInstr) -> None:
+        ...
+
+    @abstractmethod
+    def visit_call_instr(self, callinstr: CI.CCallInstr) -> None:
+        ...
+
+    @abstractmethod
+    def visit_asm_instr(self, asminstr: CI.CAsmInstr) -> None:
+        ...
+
+    @abstractmethod
+    def visit_asm_output(self, asmoutput: CI.CAsmOutput) -> None:
+        ...
+
+    @abstractmethod
+    def visit_asm_input(self, asminput: CI.CAsmInput) -> None:
+        ...
+
     @abstractmethod
     def visit_voidtyp(self, ctyp: CT.CTypVoid) -> None:
         ...
@@ -87,10 +203,162 @@ def visit_funarg(self, ctyp: CT.CFunArg) -> None:
     def visit_funargs(self, ctyp: CT.CFunArgs) -> None:
         ...
 
+    @abstractmethod
+    def visit_lval(self, lval: CL.CLval) -> None:
+        ...
+
+    @abstractmethod
+    def visit_lhostvar(self, lhostvar: CH.CLHostVar) -> None:
+        ...
+
+    @abstractmethod
+    def visit_lhostmem(self, lhostmem: CH.CLHostMem) -> None:
+        ...
+
+    @abstractmethod
+    def visit_nooffset(self, nooffset: CO.CNoOffset) -> None:
+        ...
+
+    @abstractmethod
+    def visit_fieldoffset(self, fieldoffset: CO.CFieldOffset) -> None:
+        ...
+
+    @abstractmethod
+    def visit_indexoffset(self, indexoffset: CO.CIndexOffset) -> None:
+        ...
+
+    @abstractmethod
+    def visit_constexp(self, c: CE.CExpConst) -> None:
+        ...
+
+    @abstractmethod
+    def visit_explval(self, lval: CE.CExpLval) -> None:
+        ...
+
+    @abstractmethod
+    def visit_sizeof(self, sizeof: CE.CExpSizeOf) -> None:
+        ...
+
+    @abstractmethod
+    def visit_sizeofe(self, sizeofe: CE.CExpSizeOfE) -> None:
+        ...
+
+    @abstractmethod
+    def visit_size_of_str(self, sizeofstr: CE.CExpSizeOfStr) -> None:
+        ...
+
+    @abstractmethod
+    def visit_alignof(self, alignof: CE.CExpAlignOf) -> None:
+        ...
+
+    @abstractmethod
+    def visit_alignofe(self, alignofe: CE.CExpAlignOfE) -> None:
+        ...
+
+    @abstractmethod
+    def visit_unop(self, unop: CE.CExpUnOp) -> None:
+        ...
+
+    @abstractmethod
+    def visit_binop(self, binop: CE.CExpBinOp) -> None:
+        ...
+
+    @abstractmethod
+    def visit_question(self, question: CE.CExpQuestion) -> None:
+        ...
+
+    @abstractmethod
+    def visit_cast(self, ecast: CE.CExpCastE) -> None:
+        ...
+
+    @abstractmethod
+    def visit_addrof(self, addrof: CE.CExpAddrOf) -> None:
+        ...
+
+    @abstractmethod
+    def visit_addr_of_label(self, addroflabel: CE.CExpAddrOfLabel) -> None:
+        ...
+
+    @abstractmethod
+    def visit_startof(self, startof: CE.CExpStartOf) -> None:
+        ...
+
+    @abstractmethod
+    def visit_fn_app(self, fnapp: CE.CExpFnApp) -> None:
+        ...
+
+    @abstractmethod
+    def visit_cn_app(self, cnapp: CE.CExpCnApp) -> None:
+        ...
+
     @abstractmethod
     def visit_attributes(self, a: CA.CAttributes) -> None:
         ...
 
     @abstractmethod
-    def visit_constexp(self, a: CE.CExpConst) -> None:
+    def visit_attribute(self, a: CA.CAttribute) -> None:
+        ...
+
+    @abstractmethod
+    def visit_attr_int(self, a: CA.CAttrInt) -> None:
+        ...
+
+    @abstractmethod
+    def visit_attr_str(self, a: CA.CAttrStr) -> None:
+        ...
+
+    @abstractmethod
+    def visit_attr_cons(self, a: CA.CAttrCons) -> None:
+        ...
+
+    @abstractmethod
+    def visit_attr_sizeof(self, a: CA.CAttrSizeOf) -> None:
+        ...
+
+    @abstractmethod
+    def visit_attr_sizeofe(self, a: CA.CAttrSizeOfE) -> None:
+        ...
+
+    @abstractmethod
+    def visit_attr_sizeofs(self, a: CA.CAttrSizeOfS) -> None:
+        ...
+
+    @abstractmethod
+    def visit_attr_alignof(self, a: CA.CAttrAlignOf) -> None:
+        ...
+
+    @abstractmethod
+    def visit_attr_alignofe(self, a: CA.CAttrAlignOfE) -> None:
+        ...
+
+    @abstractmethod
+    def visit_attr_alignofs(self, a: CA.CAttrAlignOfS) -> None:
+        ...
+
+    @abstractmethod
+    def visit_attr_unop(self, a: CA.CAttrUnOp) -> None:
+        ...
+
+    @abstractmethod
+    def visit_attr_binop(self, a: CA.CAttrBinOp) -> None:
+        ...
+
+    @abstractmethod
+    def visit_attr_dot(self, a: CA.CAttrDot) -> None:
+        ...
+
+    @abstractmethod
+    def visit_attr_star(self, a: CA.CAttrStar) -> None:
+        ...
+
+    @abstractmethod
+    def visit_attr_addrof(self, a: CA.CAttrAddrOf) -> None:
+        ...
+
+    @abstractmethod
+    def visit_attr_index(self, a: CA.CAttrIndex) -> None:
+        ...
+
+    @abstractmethod
+    def visit_attr_question(self, a: CA.CAttrQuestion) -> None:
         ...
diff --git a/chc/cmdline/AnalysisManager.py b/chc/cmdline/AnalysisManager.py
index 7cc56a2..c681259 100644
--- a/chc/cmdline/AnalysisManager.py
+++ b/chc/cmdline/AnalysisManager.py
@@ -32,6 +32,7 @@
 import subprocess
 import os
 import shutil
+import sys
 
 from typing import List, Optional, Tuple, TYPE_CHECKING
 
@@ -45,17 +46,23 @@
     from chc.app.CFile import CFile
 
 
+def print_status(m: str) -> None:
+    sys.stderr.write(m + "\n")
+
+
 class AnalysisManager:
     """Provide the interface to the codehawk (ocaml) analyzer."""
 
     def __init__(
-        self,
-        capp: "CApplication",
-        wordsize: int = 0,
-        unreachability: bool = False,
-        thirdpartysummaries: List[str] = [],
-        nofilter: bool = True,
-        verbose: bool = False,
+            self,
+            capp: "CApplication",
+            wordsize: int = 0,
+            unreachability: bool = False,
+            thirdpartysummaries: List[str] = [],
+            keep_system_includes: bool = False,
+            verbose: bool = False,
+            disable_timing: bool = False,
+            collectdiagnostics: bool = False
     ) -> None:
         """Initialize the analyzer location and target file location.
 
@@ -72,22 +79,27 @@ def __init__(
         """
 
         self._capp = capp
-        # self.contractpath = capp.contractpath
         self._config = Config()
-        # self.chsummaries = self.config.summaries
-        # self.path = self.capp.path
-        # self.canalyzer = self.config.canalyzer
-        # self.gui = self.config.chc_gui
-        self.nofilter = nofilter
+        self._keep_system_includes = keep_system_includes
         self.wordsize = wordsize
         self.thirdpartysummaries = thirdpartysummaries
         self.unreachability = unreachability
         self.verbose = verbose
+        self.disable_timing = disable_timing
+        self._collectdiagnostics = collectdiagnostics
 
     @property
     def capp(self) -> "CApplication":
         return self._capp
 
+    @property
+    def keep_system_includes(self) -> bool:
+        return self._keep_system_includes
+
+    @property
+    def collect_diagnostics(self) -> bool:
+        return self._collectdiagnostics
+
     @property
     def contractpath(self) -> Optional[str]:
         return self.capp.contractpath
@@ -171,7 +183,7 @@ def reset_tables(self, cfile: "CFile") -> None:
 
     def _execute_cmd(self, CMD: List[str]) -> None:
         try:
-            print(CMD)
+            print_status(", ".join(CMD))
             result = subprocess.check_output(CMD)
             print(result.decode("utf-8"))
         except subprocess.CalledProcessError as args:
@@ -179,9 +191,11 @@ def _execute_cmd(self, CMD: List[str]) -> None:
             print(args)
             exit(1)
 
-    def _create_file_primary_proofobligations_cmd_partial(self) -> List[str]:
+    def _create_file_primary_proofobligations_cmd_partial(
+            self, po_cmd="undefined-behavior-primary"
+    ) -> List[str]:
         cmd: List[str] = [
-            self.canalyzer, "-summaries", self.chsummaries, "-command", "primary"]
+            self.canalyzer, "-summaries", self.chsummaries, "-command", po_cmd]
         if not (self.thirdpartysummaries is None):
             for s in self.thirdpartysummaries:
                 cmd.extend(["-summaries", s])
@@ -189,30 +203,37 @@ def _create_file_primary_proofobligations_cmd_partial(self) -> List[str]:
             cmd.extend(["-contractpath", self.contractpath])
         cmd.extend(["-projectname", self.capp.projectname])
 
-        if self.nofilter:
-            cmd.append("-nofilter")
+        if self.keep_system_includes:
+            cmd.append("-keep_system_includes")
         if self.wordsize > 0:
             cmd.extend(["-wordsize", str(self.wordsize)])
+        if self.collect_diagnostics:
+            cmd.append("-diagnostics")
         cmd.append(self.targetpath)
         cmd.append("-cfilename")
         return cmd
 
     def create_file_primary_proofobligations(
-            self, cfilename: str, cfilepath: Optional[str] = None) -> None:
+            self,
+            cfilename: str,
+            cfilepath: Optional[str] = None,
+            po_cmd: str = "undefined-behavior-primary"
+    ) -> None:
         """Call analyzer to create primary proof obligations for a single file."""
 
         chklogger.logger.info(
             "Create primiary proof obligations for file %s with path %s",
             cfilename, ("none" if cfilepath is None else cfilepath))
         try:
-            cmd = self._create_file_primary_proofobligations_cmd_partial()
+            cmd = self._create_file_primary_proofobligations_cmd_partial(
+                po_cmd=po_cmd)
             cmd.append(cfilename)
             if cfilepath is not None:
                 cmd.extend(["-cfilepath", cfilepath])
             chklogger.logger.info(
                 "Ocaml analyzer is called with %s", str(cmd))
             if self.verbose:
-                print(str(cmd))
+                print_status(str(cmd))
                 result = subprocess.call(
                     cmd, cwd=self.targetpath, stderr=subprocess.STDOUT)
                 print("\nResult: " + str(result))
@@ -238,13 +259,17 @@ def create_file_primary_proofobligations(
             print(args)
             exit(1)
 
-    def create_app_primary_proofobligations(self, processes: int = 1) -> None:
+    def create_app_primary_proofobligations(
+            self,
+            po_cmd: str = "undefined-behavior-primary",
+            processes: int = 1) -> None:
         """Call analyzer to create ppo's for all application files."""
 
         if processes > 1:
 
             def f(cfile: "CFile") -> None:
-                cmd = self._create_file_primary_proofobligations_cmd_partial()
+                cmd = self._create_file_primary_proofobligations_cmd_partial(
+                    po_cmd=po_cmd)
                 cmd.append(cfile.cfilename)
                 if cfile.cfilepath is not None:
                     cmd.extend(["-cfilepath", cfile.cfilepath])
@@ -262,7 +287,7 @@ def f(cfile: "CFile") -> None:
 
             def f(cfile: "CFile") -> None:
                 self.create_file_primary_proofobligations(
-                    cfile.cfilename, cfile.cfilepath)
+                    cfile.cfilename, cfile.cfilepath, po_cmd=po_cmd)
 
             self.capp.iter_files(f)
 
@@ -283,14 +308,18 @@ def _generate_and_check_file_cmd_partial(
         if not (self.contractpath is None):
             cmd.extend(["-contractpath", self.contractpath])
         cmd.extend(["-projectname", self.capp.projectname])
-        if self.nofilter:
-            cmd.append("-nofilter")
+        if self.keep_system_includes:
+            cmd.append("-keep_system_includes")
         if self.wordsize > 0:
             cmd.extend(["-wordsize", str(self.wordsize)])
         if self.unreachability:
             cmd.append("-unreachability")
         if self.verbose:
             cmd.append("-verbose")
+        if self.disable_timing:
+            cmd.append("-disable_timing")
+        if self.collect_diagnostics:
+            cmd.append("-diagnostics")
         cmd.append(self.targetpath)
         if cfilepath is not None:
             cmd.extend(["-cfilepath", cfilepath])
@@ -321,6 +350,7 @@ def generate_and_check_file(
                     stdout=open(os.devnull, "w"),
                     stderr=subprocess.STDOUT,
                 )
+                print("\nResult: " + str(result))
             if result != 0:
                 chklogger.logger.error(
                     "Error in generating invariants for %s", cfilename)
diff --git a/chc/cmdline/ParseManager.py b/chc/cmdline/ParseManager.py
index f41df19..80e3c5b 100644
--- a/chc/cmdline/ParseManager.py
+++ b/chc/cmdline/ParseManager.py
@@ -72,7 +72,7 @@ def __init__(
             projectpath: str,
             projectname: str,
             targetpath: str,
-            filter: bool = False,
+            keep_system_includes: bool = False,
             posix: bool = False,
             verbose: bool = True,
             keepUnused: bool = False,
@@ -96,7 +96,7 @@ def __init__(
             self._targetpath, self._projectname)
         self._analysisresultspath = UF.get_analysisresults_path(
             self._targetpath, self._projectname)
-        self._filter = filter
+        self._keep_system_includes = keep_system_includes
         self._posix = posix
         self._keepUnused = keepUnused
         self._verbose = verbose
@@ -160,8 +160,8 @@ def tgtplatform(self) -> str:
         return self._tgtplatform
 
     @property
-    def filter(self) -> bool:
-        return self._filter
+    def keep_system_includes(self) -> bool:
+        return self._keep_system_includes
 
     @property
     def posix(self) -> bool:
@@ -419,9 +419,11 @@ def preprocess(
     def parse_with_ccommands(
             self,
             compilecommands: List[Dict[str, Any]],
-            copyfiles: bool = True) -> None:
+            copyfiles: bool = True) -> int:
         """Preprocess and call C parser to produce xml semantics files."""
 
+        exitcode = 0
+
         cfiles: Dict[str, int] = {}
         targetfiles = TargetFiles()
         for c in compilecommands:
@@ -439,8 +441,8 @@ def parse_with_ccommands(
                 "-targetdirectory",
                 self.analysisresultspath
             ]
-            if not self.filter:
-                command.append("-nofilter")
+            if self.keep_system_includes:
+                command.append("-keep_system_includes")
             if self.keepUnused:
                 command.append("-keepUnused")
             command.append(ifilename)
@@ -459,6 +461,7 @@ def parse_with_ccommands(
                 print("\n" + ("*" * 80))
                 print("Parsing error in " + cfilename)
                 print("*" * 80)
+                exitcode = 1
                 break
 
         if self.verbose:
@@ -481,6 +484,7 @@ def parse_with_ccommands(
             )
         os.chdir(self.projectpath)
         shutil.copy("compile_commands.json", self.savedsourcepath)
+        return exitcode
 
     def parse_ifiles(self, copyfiles: bool = True) -> None:
         """Run the CodeHawk C parser on all .i files in the directory."""
@@ -533,8 +537,8 @@ def parse_ifile(self, ifilename: str) -> int:
             "-targetdirectory",
             self.analysisresultspath,
         ]
-        if not self.filter:
-            cmd.append("-nofilter")
+        if not self.keep_system_includes:
+            cmd.append("-keep_system_includes")
         if self.keepUnused:
             cmd.append("-keepUnused")
         cmd.append(ifilename)
diff --git a/chc/cmdline/c_file/cfileutil.py b/chc/cmdline/c_file/cfileutil.py
index b598584..40d3815 100644
--- a/chc/cmdline/c_file/cfileutil.py
+++ b/chc/cmdline/c_file/cfileutil.py
@@ -76,6 +76,7 @@
 if TYPE_CHECKING:
     from chc.invariants.CInvariantFact import CInvariantNRVFact
     from chc.app.CAttributes import CAttributes
+    from chc.app.CInstr import CCallInstr
     from chc.app.CTyp import (
         CTypComp, CTypFloat, CTypFun, CTypInt, CTypPtr)
     from chc.proof.CFunctionPO import CFunctionPO
@@ -119,6 +120,7 @@ def cfile_parse_file(args: argparse.Namespace) -> NoReturn:
     # arguments
     pcfilename: str = os.path.abspath(args.filename)
     opttgtpath: Optional[str] = args.tgtpath
+    keep_system_includes: bool = args.keep_system_includes
     loglevel: str = args.loglevel
     logfilename: Optional[str] = args.logfilename
     logfilemode: str = args.logfilemode
@@ -156,7 +158,8 @@ def cfile_parse_file(args: argparse.Namespace) -> NoReturn:
 
     chklogger.logger.info("Target path: %s", targetpath)
 
-    parsemanager = ParseManager(projectpath, projectname, targetpath)
+    parsemanager = ParseManager(
+        projectpath, projectname, targetpath, keep_system_includes=keep_system_includes)
     parsemanager.remove_semantics()
     parsemanager.initialize_paths()
 
@@ -398,6 +401,75 @@ def cfile_mk_headerfile(args: argparse.Namespace) -> NoReturn:
     exit(0)
 
 
+def cfile_cil_source(args: argparse.Namespace) -> NoReturn:
+    """Outputs a textual representation of the CIL AST. """
+
+    # 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()
+
+    fcilsource = cfile.cil_source()
+
+    if xoutput is not None:
+        outputfilename = xoutput + ".cil.c"
+        with open(outputfilename, "w") as fp:
+            fp.write(fcilsource)
+        print("Cil source code written to " + outputfilename)
+
+    else:
+        print(fcilsource)
+
+    exit(0)
+
+
 def cfile_analyze_file(args: argparse.Namespace) -> NoReturn:
     """Analyzes a single c-file and saves the results in the .cch directory.
 
@@ -420,7 +492,11 @@ def cfile_analyze_file(args: argparse.Namespace) -> NoReturn:
     xcfilename: str = args.filename
     opttgtpath: Optional[str] = args.tgtpath
     wordsize: int = args.wordsize
+    keep_system_includes: bool = args.keep_system_includes
+    analysis: str = args.analysis
     verbose: bool = args.verbose
+    analysisdomains: str = args.analysis_domains
+    collectdiagnostics: bool = args.collect_diagnostics
     loglevel: str = args.loglevel
     logfilename: Optional[str] = args.logfilename
     logfilemode: str = args.logfilemode
@@ -432,6 +508,8 @@ def cfile_analyze_file(args: argparse.Namespace) -> NoReturn:
     cfilename = cfilename_ext[:-2]
     projectname = cfilename
 
+    po_cmd = analysis + "-primary"
+
     set_logging(
         loglevel,
         targetpath,
@@ -470,24 +548,34 @@ def cfile_analyze_file(args: argparse.Namespace) -> NoReturn:
     contractpath = os.path.join(targetpath, "chc_contracts")
 
     capp = CApplication(
-        projectpath, projectname, targetpath, contractpath, singlefile=True)
+        projectpath,
+        projectname,
+        targetpath,
+        contractpath,
+        singlefile=True,
+        keep_system_includes=keep_system_includes)
 
     capp.initialize_single_file(cfilename)
     cfile = capp.get_cfile()
 
-    am = AnalysisManager(capp, verbose=verbose, wordsize=wordsize)
+    am = AnalysisManager(
+        capp,
+        verbose=verbose,
+        collectdiagnostics=collectdiagnostics,
+        wordsize=wordsize,
+        keep_system_includes=keep_system_includes)
 
-    am.create_file_primary_proofobligations(cfilename)
+    am.create_file_primary_proofobligations(cfilename, po_cmd=po_cmd)
     am.reset_tables(cfile)
     capp.collect_post_assumes()
 
-    am.generate_and_check_file(cfilename, None, "llrvisp")
+    am.generate_and_check_file(cfilename, None, analysisdomains)
     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, analysisdomains)
         am.reset_tables(cfile)
 
     chklogger.logger.info("cfile analyze completed")
@@ -508,6 +596,7 @@ def cfile_report_file(args: argparse.Namespace) -> NoReturn:
     # arguments
     xcfilename: str = args.filename
     opttgtpath: Optional[str] = args.tgtpath
+    canalysis: str = args.analysis
     cshowcode: bool = args.showcode
     cshowinvariants: bool = args.showinvariants
     cfunctions: Optional[List[str]] = args.functions
@@ -563,6 +652,19 @@ def pofilter(po: "CFunctionPO") -> bool:
                 cfile, pofilter=pofilter, showinvs=cshowinvariants))
 
         print(RP.file_proofobligation_stats_tostring(cfile))
+
+        def callsite_str(instr: "CCallInstr") -> str:
+            return (
+                instr.parent.cfile.name + ".c:"
+                + instr.parent.cfun.name + ":"
+                + str(instr.location.line)
+            )
+
+        if canalysis == "outputparameters":
+            for cfun in cfile.functions.values():
+                print("\nFunction: " + cfun.name)
+                print(str(cfun.analysis_digests))
+
         exit(0)
 
     for fnname in cfunctions:
@@ -580,6 +682,10 @@ def cfile_run_file(args: argparse.Namespace) -> NoReturn:
     # arguments
     pcfilename: str = os.path.abspath(args.filename)
     opttgtpath: Optional[str] = args.tgtpath
+    keep_system_includes: bool = args.keep_system_includes
+    analysis: str = args.analysis
+    analysisdomains: str = args.analysis_domains
+    collectdiagnostics: bool = args.collect_diagnostics
     cshowcode: bool = args.showcode
     copen: bool = args.open
     cshowinvariants: bool = args.showinvariants
@@ -611,6 +717,8 @@ def cfile_run_file(args: argparse.Namespace) -> NoReturn:
     cfilename = cfilename_c[:-2]
     projectname = cfilename
 
+    po_cmd = analysis + "-primary"
+
     if not os.path.isdir(targetpath):
         print_error("Target directory: " + targetpath + " does not exist")
         exit(1)
@@ -624,7 +732,8 @@ def cfile_run_file(args: argparse.Namespace) -> NoReturn:
 
     chklogger.logger.info("Target path: %s", targetpath)
 
-    parsemanager = ParseManager(projectpath, projectname, targetpath)
+    parsemanager = ParseManager(
+        projectpath, projectname, targetpath, keep_system_includes=keep_system_includes)
     parsemanager.remove_semantics()
     parsemanager.initialize_paths()
 
@@ -674,30 +783,44 @@ def cfile_run_file(args: argparse.Namespace) -> NoReturn:
     contractpath = os.path.join(targetpath, "chc_contracts")
 
     capp = CApplication(
-        projectpath, projectname, targetpath, contractpath, singlefile=True)
+        projectpath,
+        projectname,
+        targetpath,
+        contractpath,
+        singlefile=True,
+        keep_system_includes=keep_system_includes)
 
     capp.initialize_single_file(cfilename)
     cfile = capp.get_cfile()
 
-    am = AnalysisManager(capp, verbose=verbose)
+    am = AnalysisManager(
+        capp,
+        verbose=verbose,
+        collectdiagnostics=collectdiagnostics,
+        keep_system_includes=keep_system_includes)
 
-    am.create_file_primary_proofobligations(cfilename)
+    am.create_file_primary_proofobligations(cfilename, po_cmd=po_cmd)
     am.reset_tables(cfile)
     capp.collect_post_assumes()
 
-    am.generate_and_check_file(cfilename, None, "llrvisp")
+    am.generate_and_check_file(cfilename, None, analysisdomains)
     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, analysisdomains)
         am.reset_tables(cfile)
 
     chklogger.logger.info("cfile analyze completed")
 
     capp = CApplication(
-        projectpath, projectname, targetpath, contractpath, singlefile=True)
+        projectpath,
+        projectname,
+        targetpath,
+        contractpath,
+        singlefile=True,
+        keep_system_includes=keep_system_includes)
     capp.initialize_single_file(cfilename)
     cfile = capp.get_cfile()
 
@@ -723,6 +846,12 @@ def pofilter(po: "CFunctionPO") -> bool:
             cfile, pofilter=pofilter, showinvs=cshowinvariants))
 
     print(RP.file_proofobligation_stats_tostring(cfile))
+
+    if analysis == "outputparameters":
+        for cfun in cfile.functions.values():
+            print("\nFunction: " + cfun.name)
+            print(str(cfun.analysis_digests))
+
     exit(0)
 
 
diff --git a/chc/cmdline/c_project/cprojectutil.py b/chc/cmdline/c_project/cprojectutil.py
index 14dbd17..865247c 100644
--- a/chc/cmdline/c_project/cprojectutil.py
+++ b/chc/cmdline/c_project/cprojectutil.py
@@ -59,7 +59,7 @@
     from chc.app.CAttributes import CAttributes
     from chc.app.CFile import CFile
     from chc.app.CFunction import CFunction
-    from chc.app.CInstr import CInstr
+    from chc.app.CInstr import CInstr, CCallInstr
     from chc.app.CStmt import CInstrsStmt, CStmt
     from chc.invariants.CInvariantFact import CInvariantNRVFact
     from chc.app.CTyp import (
@@ -69,10 +69,14 @@
 
 def print_error(m: str) -> None:
     sys.stderr.write(("*" * 80) + "\n")
-    sys.stderr.write(m + "\n")
+    sys.stderr.write("F:" + m + "\n")
     sys.stderr.write(("*" * 80) + "\n")
 
 
+def print_status_update(m: str) -> None:
+    sys.stderr.write("[chkc] " + m + "\n")
+
+
 def set_logging(
         level: str,
         path: str,
@@ -111,6 +115,7 @@ def cproject_parse_project(args: argparse.Namespace) -> NoReturn:
     projectpath: str = args.path
     projectname: str = args.projectname
     opttgtpath: Optional[str] = args.tgtpath
+    keep_system_includes: bool = args.keep_system_includes
     loglevel: str = args.loglevel
     logfilename: Optional[str] = args.logfilename
     logfilemode: str = args.logfilemode
@@ -157,13 +162,19 @@ def cproject_parse_project(args: argparse.Namespace) -> NoReturn:
         print_error("The compile_commands.json file was found empty")
         exit(1)
 
-    parsemanager = ParseManager(projectpath, projectname, targetpath)
+    parsemanager = ParseManager(
+        projectpath,
+        projectname,
+        targetpath,
+        keep_system_includes=keep_system_includes)
     parsemanager.remove_semantics()
     parsemanager.initialize_paths()
-    parsemanager.parse_with_ccommands(compilecommands, copyfiles=True)
-    parsemanager.save_semantics()
+    exitcode = parsemanager.parse_with_ccommands(compilecommands, copyfiles=True)
+    if exitcode == 0:
+        parsemanager.save_semantics()
 
-    exit(0)
+    print_status_update("exitcode: " + str(exitcode))
+    exit(exitcode)
 
 
 def cproject_scan_op(args: argparse.Namespace) -> NoReturn:
@@ -419,12 +430,67 @@ def is_included(path: Optional[str]) -> bool:
     exit(0)
 
 
+def cproject_cil_source(args: argparse.Namespace) -> NoReturn:
+    """Outputs a textual representation of the CIL AST."""
+
+    # arguments
+
+    tgtpath: str = args.tgtpath
+    projectname: str = args.projectname
+    filename: str = args.filename
+    loglevel: str = args.loglevel
+    logfilename: Optional[str] = args.logfilename
+    logfilemode: str = args.logfilemode
+
+    targetpath = os.path.abspath(tgtpath)
+    projectpath = targetpath
+    cfilename_c = os.path.basename(filename)
+    cfilename = cfilename_c[:-2]
+    cfilepath = os.path.dirname(filename)
+
+    set_logging(
+        loglevel,
+        targetpath,
+        logfilename=logfilename,
+        mode=logfilemode,
+        msg="Command cfile mk-headerfile was invoked")
+
+    if not UF.has_analysisresults_path(targetpath, projectname):
+        print_error(
+            f"No analysis results found for {projectname} in {targetpath}")
+        exit(1)
+
+    contractpath = os.path.join(targetpath, "chc_contracts")
+    capp = CApplication(
+        projectpath, projectname, targetpath, contractpath)
+
+    if capp.has_file(filename[:-2]):
+        cfile = capp.get_file(filename[:-2])
+    else:
+        print_error(f"File {filename} not found")
+        exit(1)
+
+    fcilsource = cfile.cil_source()
+
+    outputfilename = cfile.cfilename + ".cil.c"
+    with open(outputfilename, "w") as fp:
+        fp.write(fcilsource)
+    print("Cil source code written to " + outputfilename)
+
+    exit(0)
+
+
 def cproject_analyze_project(args: argparse.Namespace) -> NoReturn:
 
     # arguments
     tgtpath: str = args.tgtpath
     projectname: str = args.projectname
+    keep_system_includes: bool = args.keep_system_includes
+    analysis: str = args.analysis
+    analysisdomains: str = args.analysis_domains
+    collectdiagnostics: bool = args.collect_diagnostics
     maxprocesses: int = args.maxprocesses
+    verbose: bool = args.verbose
     loglevel: str = args.loglevel
     logfilename: Optional[str] = args.logfilename
     logfilemode: str = args.logfilemode
@@ -433,6 +499,8 @@ def cproject_analyze_project(args: argparse.Namespace) -> NoReturn:
     if excludefiles is None:
         excludefiles = []
 
+    po_cmd = analysis + "-primary"
+
     if not os.path.isdir(tgtpath):
         print_error(f"Target directory {tgtpath} not found")
         exit(1)
@@ -459,6 +527,7 @@ def cproject_analyze_project(args: argparse.Namespace) -> NoReturn:
         projectname,
         targetpath,
         contractpath,
+        keep_system_includes=keep_system_includes,
         excludefiles=excludefiles)
 
     def save_xrefs(f: "CFile") -> None:
@@ -476,29 +545,74 @@ def save_xrefs(f: "CFile") -> None:
         projectname,
         targetpath,
         contractpath,
+        keep_system_includes=keep_system_includes,
         excludefiles=excludefiles)
 
-    am = AnalysisManager(capp, verbose=True)
+    am = AnalysisManager(
+        capp,
+        verbose=verbose,
+        collectdiagnostics=collectdiagnostics,
+        keep_system_includes=keep_system_includes)
+
+    exitcode = 0
+
+    def check_continuation() -> int:
+        if analysis == "outputparameters":
+            if not capp.check_digests():
+                return 166
+        return 0
 
     with timing("analysis"):
 
         try:
-            am.create_app_primary_proofobligations(processes=maxprocesses)
+            am.create_app_primary_proofobligations(
+                po_cmd=po_cmd, processes=maxprocesses)
             capp.reinitialize_tables()
             capp.collect_post_assumes()
         except UF.CHError as e:
             print(str(e.wrap()))
             exit(1)
 
-        for i in range(1):
-            am.generate_and_check_app("llrvisp", processes=maxprocesses)
-            capp.reinitialize_tables()
-            capp.update_spos()
-
-        for i in range(5):
-            capp.update_spos()
-            am.generate_and_check_app("llrvisp", processes=maxprocesses)
-            capp.reinitialize_tables()
+        exitcode = check_continuation()
+
+        if exitcode == 0:
+            for i in range(1):
+                am.generate_and_check_app(analysisdomains, processes=maxprocesses)
+                capp.reinitialize_tables()
+                capp.update_spos()
+
+            exitcode = check_continuation()
+
+        if exitcode == 0:
+            for i in range(5):
+                capp.update_spos()
+                am.generate_and_check_app(analysisdomains, processes=maxprocesses)
+                capp.reinitialize_tables()
+
+                exitcode = check_continuation()
+                if exitcode > 0:
+                    break
+
+    if analysis == "outputparameters":
+        presult = capp.outputparameters()
+        vresult = capp.viable_outputparameters()
+        mresult = capp.maybe_outputparameters()
+        viable = sum(len(f) for f in vresult.values())
+        maybe = sum(len(f) for f in mresult.values())
+        opp = sum(len(f) for f in presult.values())
+        print("Functions analyzed     : " + str(len(vresult)))
+        print("Outputparameters       : " + str(opp))
+        print("Maybe outputparameters : " + str(maybe))
+        print("Viable outputparameters: " + str(viable))
+        for (fname, pl) in vresult.items():
+            if len(pl) > 0:
+                print("  function: " + fname)
+                for p in pl:
+                    print("    " + str(p.parameter))
+        if viable > 0:
+            exitcode = 0
+        elif maybe > 0:
+            exitcode = 167
 
     timestamp = os.stat(UF.get_cchpath(targetpath, projectname)).st_ctime
 
@@ -508,7 +622,8 @@ def save_xrefs(f: "CFile") -> None:
     UF.save_project_summary_results(targetpath, projectname, result)
     UF.save_project_summary_results_as_xml(targetpath, projectname, result)
 
-    exit(0)
+    print_status_update("exitcode: " + str(exitcode))
+    exit(exitcode)
 
 
 def cproject_report(args: argparse.Namespace) -> NoReturn:
@@ -517,38 +632,73 @@ def cproject_report(args: argparse.Namespace) -> NoReturn:
     # arguments
     tgtpath: str = args.tgtpath
     projectname: str = args.projectname
+    canalysis: str = args.analysis
+    verbose: bool = args.verbose
+    loglevel: str = args.loglevel
+    logfilename: Optional[str] = args.logfilename
+    logfilemode: str = args.logfilemode
 
     targetpath = os.path.abspath(tgtpath)
     projectpath = targetpath
 
-    result = UF.read_project_summary_results(targetpath, projectname)
-    if result is not None:
-        print(RP.project_proofobligation_stats_dict_to_string(result))
-        exit(0)
+    set_logging(
+        loglevel,
+        targetpath,
+        logfilename=logfilename,
+        mode=logfilemode,
+        msg="c-project report invoked")
 
-    if not UF.has_analysisresults_path(targetpath, projectname):
-        print_error(
-            f"No analysis results found for {projectname} in {targetpath}")
-        exit(1)
+    if canalysis == "undefined-behavior":
+        statsresult = UF.read_project_summary_results(targetpath, projectname)
+        if statsresult is not None:
+            print(RP.project_proofobligation_stats_dict_to_string(statsresult))
+            exit(0)
+
+        if not UF.has_analysisresults_path(targetpath, projectname):
+            print_error(
+                f"No analysis results found for {projectname} in {targetpath}")
+            exit(1)
+
+        contractpath = os.path.join(targetpath, "chc_contracts")
+        capp = CApplication(
+            projectpath, projectname, targetpath, contractpath)
+
+        timestamp = os.stat(UF.get_cchpath(targetpath, projectname)).st_ctime
+        fresult = RP.project_proofobligation_stats_to_dict(capp)
+        fresult["timestamp"] = timestamp
+        fresult["project"] = projectpath
+        UF.save_project_summary_results(targetpath, projectname, fresult)
+        UF.save_project_summary_results_as_xml(targetpath, projectname, fresult)
+        exit(0)
 
     contractpath = os.path.join(targetpath, "chc_contracts")
     capp = CApplication(
         projectpath, projectname, targetpath, contractpath)
 
-    timestamp = os.stat(UF.get_cchpath(targetpath, projectname)).st_ctime
-    fresult = RP.project_proofobligation_stats_to_dict(capp)
-    fresult["timestamp"] = timestamp
-    fresult["project"] = projectpath
-    UF.save_project_summary_results(targetpath, projectname, fresult)
-    UF.save_project_summary_results_as_xml(targetpath, projectname, fresult)
-
-    result = UF.read_project_summary_results(targetpath, projectname)
-    if result is not None:
-        print(RP.project_proofobligation_stats_dict_to_string(result))
+    statsresult = UF.read_project_summary_results(targetpath, projectname)
+    if statsresult is not None:
+        print(RP.project_proofobligation_stats_dict_to_string(statsresult))
     else:
         print_error("Results were not readable")
         exit(1)
 
+    if canalysis == "outputparameters":
+
+        print("\n\nOutput-parameter analysis results")
+        for cfile in capp.files.values():
+            print("\nFile: " + cfile.name)
+            for cfun in cfile.functions.values():
+                '''
+                if len(cfun.analysis_digests.digests) == 0:
+                    print(
+                        "\nFunction: "
+                        + cfun.name
+                        + ": No candidate output parameters")
+                else:
+                '''
+                print("\nFunction: " + cfun.name)
+                print(str(cfun.analysis_digests))
+
     exit(0)
 
 
@@ -559,6 +709,7 @@ def cproject_report_file(args: argparse.Namespace) -> NoReturn:
     tgtpath: str = args.tgtpath
     projectname: str = args.projectname
     filename: str = args.filename
+    canalysis: str = args.analysis
     showcode: bool = args.showcode
     showopen: bool = args.open
     showinvariants: bool = args.showinvariants
@@ -596,6 +747,76 @@ def pofilter(po: "CFunctionPO") -> bool:
 
     print(RP.file_proofobligation_stats_tostring(cfile))
 
+    def callsite_str(instr: "CCallInstr") -> str:
+        return (
+            instr.parent.cfile.name + ".c:"
+            + instr.parent.cfun.name + ":"
+            + str(instr.location.line)
+        )
+
+    if canalysis == "outputparameters":
+        for cfun in cfile.functions.values():
+            print("\nFunction: " + cfun.name)
+            print(str(cfun.analysis_digests))
+
+    exit(0)
+
+
+def cproject_investigate(args: argparse.Namespace) -> NoReturn:
+
+    # arguments
+    tgtpath: str = args.tgtpath
+    projectname: str = args.projectname
+    predicates: Optional[List[str]] = args.predicates
+
+    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)
+
+    def pofilter(po: "CFunctionPO") -> bool:
+        if predicates is not None:
+            return po.predicate_name in predicates
+        else:
+            return True
+
+    def header(s: str) -> str:
+        return (s + ":\n" + ("=" * 80))
+
+    lines: List[str] = []
+
+    for cfile in capp.cfiles:
+        openppos = cfile.get_open_ppos()
+        violations = cfile.get_ppos_violated()
+        delegated = cfile.get_ppos_delegated()
+
+        if len(openppos) + len(violations) + len(delegated) > 0:
+            lines.append("=" * 80)
+            lines.append(cfile.name)
+            lines.append("=" * 80)
+
+        if len(openppos) > 0:
+            lines.append(header("Open primary proof obligations obligations"))
+            lines.append(RP.tag_file_function_pos_tostring(openppos, pofilter=pofilter))
+
+        if len(violations) > 0:
+            lines.append(header("Primary proof obligations violated"))
+            lines.append(RP.tag_file_function_pos_tostring(
+                violations, pofilter=pofilter))
+
+        if len(delegated) > 0:
+            lines.append(header("Primary proof obligations delegated"))
+            lines.append(RP.tag_file_function_pos_tostring(delegated, pofilter=pofilter))
+
+    print("\n".join(lines))
+
     exit(0)
 
 
diff --git a/chc/cmdline/chkc b/chc/cmdline/chkc
index b104086..bb36e96 100755
--- a/chc/cmdline/chkc
+++ b/chc/cmdline/chkc
@@ -634,6 +634,10 @@ def parse() -> argparse.Namespace:
         "--tgtpath",
         help=("directory in which to store the analysis artifacts "
               + "(default: <cpath>)"))
+    cfileparse.add_argument(
+        "--keep-system-includes",
+        action="store_true",
+        help="do not filter out functions from files with absolute file names")
     cfileparse.add_argument(
         "--loglevel", "-log",
         choices=UL.LogLevel.options(),
@@ -706,6 +710,34 @@ def parse() -> argparse.Namespace:
         help="file mode for log file: append (a, default), or write (w)")
     cfilemkheader.set_defaults(func=C.cfile_mk_headerfile)
 
+    # --- cil-source
+    cfilecilsource = cfileparsers.add_parser("cil-source")
+    cfilecilsource.add_argument(
+        "filename",
+        help="name of file to be printed as cil-source text")
+    cfilecilsource.add_argument(
+        "--tgtpath",
+        help="directory in which to store the analysis artifacts "
+        + "(default: <cpath>)")
+    cfilecilsource.add_argument(
+        "--output", "-o",
+        help=("basename of file to save output "
+              + "(without extension): a file with extension .cil.c will be created"))
+    cfilecilsource.add_argument(
+        "--loglevel", "-log",
+        choices=UL.LogLevel.options(),
+        default="NONE",
+        help="activate logging with given level (default to stderr)")
+    cfilecilsource.add_argument(
+        "--logfilename",
+        help="name of file to write log messages")
+    cfilecilsource.add_argument(
+        "--logfilemode",
+        choices=["a", "w"],
+        default="a",
+        help="file mode for log file: append (a, default), or write (w)")
+    cfilecilsource.set_defaults(func=C.cfile_cil_source)
+
     # --- analyze
     cfileanalyze = cfileparsers.add_parser("analyze")
     cfileanalyze.add_argument(
@@ -720,6 +752,25 @@ def parse() -> argparse.Namespace:
         type=int,
         default=32,
         help="architecture wordsize in bits (16, 32, or 64)")
+    cfileanalyze.add_argument(
+        "--keep-system-includes",
+        action="store_true",
+        help="do not filter out functions from files with absolute file names")
+    cfileanalyze.add_argument(
+        "--analysis",
+        default="undefined-behavior",
+        choices=["undefined-behavior", "outputparameters"],
+        help="choose analysis for creating primary proof obligations")
+    cfileanalyze.add_argument(
+        "--collect-diagnostics",
+        action="store_true",
+        help="save diagnostics in a separate diagnostics log file")
+    cfileanalyze.add_argument(
+        "--analysis-domains",
+        default="llrvisp",
+        help=("choose analysis domains to be used (l: linear equalities"
+              ", r: pepr, v: value sets, i: intervals, s: symbolic sets"
+              ", p: pointer sets)"))
     cfileanalyze.add_argument(
         "--verbose", "-v",
         action="store_true",
@@ -755,6 +806,11 @@ def parse() -> argparse.Namespace:
         "--functions",
         nargs="*",
         help="restrict output to function names listed (defualt: all)")
+    cfilereport.add_argument(
+        "--analysis",
+        default="undefined-behavior",
+        choices=["undefined-behavior", "outputparameters"],
+        help="choose analysis for reporting results")
     cfilereport.add_argument(
         "--open",
         action="store_true",
@@ -794,6 +850,25 @@ def parse() -> argparse.Namespace:
     cfilerun.add_argument(
         "--tgtpath",
         help="directory to store the analysis results")
+    cfilerun.add_argument(
+        "--keep-system-includes",
+        action="store_true",
+        help="don't filter out functions from files with absolute filenames")
+    cfilerun.add_argument(
+        "--analysis",
+        default="undefined-behavior",
+        choices=["undefined-behavior", "outputparameters"],
+        help="choose analysis for creating primary proof obligations")
+    cfilerun.add_argument(
+        "--collect-diagnostics",
+        action="store_true",
+        help="save diagnostics in a separate diagnostics log file")
+    cfilerun.add_argument(
+        "--analysis-domains",
+        default="llrvisp",
+        help=("choose analysis domains to be used (l: linear equalities"
+              ", r: pepr, v: value sets, i: intervals, s: symbolic sets"
+              ", p: pointer sets)"))
     cfilerun.add_argument(
         "--showcode",
         action="store_true",
@@ -1387,6 +1462,10 @@ def parse() -> argparse.Namespace:
         "projectname", help="name of the project")
     cprojectparse.add_argument(
         "--tgtpath", help="directory to save the results")
+    cprojectparse.add_argument(
+        "--keep-system-includes",
+        action="store_true",
+        help="don't filter out functions from files with absolute filenames")
     cprojectparse.add_argument(
         "--loglevel", "-log",
         choices=UL.LogLevel.options(),
@@ -1469,12 +1548,58 @@ def parse() -> argparse.Namespace:
         help="file mode for log file: append (a, default), or write (w)")
     cprojectmkheader.set_defaults(func=P.cproject_mk_headerfile)
 
+    # --- cil-source
+    cprojectcilsource = cprojectparsers.add_parser("cil-source")
+    cprojectcilsource.add_argument(
+        "tgtpath", help="directory that contains the analysis results")
+    cprojectcilsource.add_argument(
+        "projectname", help="name of the project")
+    cprojectcilsource.add_argument(
+        "filename", help="filename with relative path wrt the project")
+    cprojectcilsource.add_argument(
+        "--loglevel", "-log",
+        choices=UL.LogLevel.options(),
+        default="NONE",
+        help="activate logging with given level (default to stderr)")
+    cprojectcilsource.add_argument(
+        "--logfilename",
+        help="name of file to write log messages")
+    cprojectcilsource.add_argument(
+        "--logfilemode",
+        choices=["a", "w"],
+        default="a",
+        help="file mode for log file: append (a, default), or write (w)")
+    cprojectcilsource.set_defaults(func=P.cproject_cil_source)
+
     # --- analyze
     cprojectanalyze = cprojectparsers.add_parser("analyze")
     cprojectanalyze.add_argument(
         "tgtpath", help="directory that contains the analysis results")
     cprojectanalyze.add_argument(
         "projectname", help="name of the project")
+    cprojectanalyze.add_argument(
+        "--keep-system-includes",
+        action="store_true",
+        help="don't filter out functions from files with absolute filenames")
+    cprojectanalyze.add_argument(
+        "--verbose", "-v",
+        action="store_true",
+        help="print analyzer status updates of invariant generation process")
+    cprojectanalyze.add_argument(
+        "--analysis",
+        default="undefined-behavior",
+        choices=["undefined-behavior", "outputparameters"],
+        help="choose analysis for creating primary proof obligations")
+    cprojectanalyze.add_argument(
+        "--collect-diagnostics",
+        action="store_true",
+        help="save diagnostics in a separate diagnostics log file")
+    cprojectanalyze.add_argument(
+        "--analysis-domains",
+        default="llrvisp",
+        help=("choose analysis domains to be used (l: linear equalities"
+              ", r: pepr, v: value sets, i: intervals, s: symbolic sets"
+              ", p: pointer sets)"))
     cprojectanalyze.add_argument(
         "--maxprocesses",
         help="number of files to process in parallel",
@@ -1507,6 +1632,28 @@ def parse() -> argparse.Namespace:
         "tgtpath", help="directory that contains the analysis results")
     cprojectreport.add_argument(
         "projectname", help="name of the project")
+    cprojectreport.add_argument(
+        "--analysis",
+        default="undefined-behavior",
+        choices=["undefined-behavior", "outputparameters"],
+        help="choose analysis for reporting results")
+    cprojectreport.add_argument(
+        "--verbose", "-v",
+        action="store_true")
+    cprojectreport.add_argument(
+        "--loglevel", "-log",
+        choices=UL.LogLevel.options(),
+        default="NONE",
+        help="activate logging with given level (default to stderr)")
+    cprojectreport.add_argument(
+        "--logfilename",
+        help="name of file to write log messages")
+    cprojectreport.add_argument(
+        "--logfilemode",
+        choices=["a", "w"],
+        default="a",
+        help="file mode for log file: append (a, default), or write (w)")
+
     cprojectreport.set_defaults(func=P.cproject_report)
 
     # --- report-file
@@ -1517,6 +1664,11 @@ def parse() -> argparse.Namespace:
         "projectname", help="name of the project")
     cprojectreportfile.add_argument(
         "filename", help="filename with relative path wrt the project")
+    cprojectreportfile.add_argument(
+        "--analysis",
+        default="undefined-behavior",
+        choices=["undefined-behavior", "outputparameters"],
+        help="choose analysis for reporting results")
     cprojectreportfile.add_argument(
         "--showcode",
         action="store_true",
@@ -1531,6 +1683,17 @@ def parse() -> argparse.Namespace:
         help="show location invariants on the code")
     cprojectreportfile.set_defaults(func=P.cproject_report_file)
 
+    # --- investigate
+    cprojectinvestigate = cprojectparsers.add_parser("investigate")
+    cprojectinvestigate.add_argument(
+        "tgtpath", help="directory that contains the analysis results")
+    cprojectinvestigate.add_argument(
+        "projectname", help="name of the project")
+    cprojectinvestigate.add_argument(
+        "--predicates",
+        nargs="*",
+        help="names of predicates of interest, e.g., not-null (default: all")
+    cprojectinvestigate.set_defaults(func=P.cproject_investigate)
     # --- query
     cprojectquery = cprojectparsers.add_parser("query")
     cprojectqueryparsers = cprojectquery.add_subparsers(title="show options")
diff --git a/chc/cmdline/juliet/JulietTestScoring.py b/chc/cmdline/juliet/JulietTestScoring.py
index 14712e0..6a17c89 100644
--- a/chc/cmdline/juliet/JulietTestScoring.py
+++ b/chc/cmdline/juliet/JulietTestScoring.py
@@ -185,7 +185,7 @@ def f(spo: "CFunctionPO") -> None:
                 if sev is None:
                     sevtxt = "?"
                 else:
-                    sevtxt = spo.get_display_prefix() + "  " + sev
+                    sevtxt = spo.get_display_prefix() + "  " + str(sev)
                 lines.append(
                     "     C:"
                     + str(spo.line).rjust(3)
@@ -213,7 +213,7 @@ def testppo_results_tostring(
                 if ev is None:
                     evstr = "?"
                 else:
-                    evstr = ppo.get_display_prefix() + "  " + ev
+                    evstr = ppo.get_display_prefix() + "  " + str(ev)
                 lines.append(
                     "    "
                     + str(ppo.line).rjust(3)
diff --git a/chc/cmdline/kendra/TestManager.py b/chc/cmdline/kendra/TestManager.py
index d42ef3e..b898641 100644
--- a/chc/cmdline/kendra/TestManager.py
+++ b/chc/cmdline/kendra/TestManager.py
@@ -345,7 +345,8 @@ def test_ppos(self) -> None:
                 )
                 cfilename = creffilename_c[:-2]
                 capp.initialize_single_file(cfilename)
-                am = AnalysisManager(capp, verbose=self.verbose)
+                am = AnalysisManager(
+                    capp, verbose=self.verbose, disable_timing=True)
                 am.create_file_primary_proofobligations(cfilename)
                 cfile = capp.get_cfile()
                 capp.collect_post_assumes()
@@ -588,7 +589,8 @@ def test_ppo_proofs(self, delaytest: bool = False) -> None:
             # only generate invariants if required
             if creffile.has_domains():
                 for d in creffile.domains:
-                    am = AnalysisManager(capp, verbose=self.verbose)
+                    am = AnalysisManager(
+                        capp, verbose=self.verbose, disable_timing=True)
                     am.generate_and_check_file(cfilename, None, d)
             cfile.reinitialize_tables()
             ppos = cfile.get_ppos()
@@ -668,7 +670,8 @@ def test_spo_proofs(self, delaytest: bool = False) -> None:
             cappfile = capp.get_cfile()
             if creffile.has_domains():
                 for d in creffile.domains:
-                    am = AnalysisManager(capp, verbose=self.verbose)
+                    am = AnalysisManager(
+                        capp, verbose=self.verbose, disable_timing=True)
                     am.generate_and_check_file(cfilename, None, d)
             cappfile.reinitialize_tables()
             spos = cappfile.get_spos()
diff --git a/chc/proof/CFilePredicateDictionary.py b/chc/proof/CFilePredicateDictionary.py
index 75368c5..141b7d2 100644
--- a/chc/proof/CFilePredicateDictionary.py
+++ b/chc/proof/CFilePredicateDictionary.py
@@ -194,6 +194,10 @@ def f(index: int, tags: List[str], args: List[int]) -> PO.CPOPredicate:
             p = cast(PO.CPOInitialized, p)
             args = [self.dictionary.index_lval(p.lval, subst=subst)]
 
+        elif p.is_locally_initialized:
+            p = cast(PO.CPOLocallyInitialized, p)
+            args = [self.dictionary.index_lval(p.lval, subst=subst)]
+
         elif p.is_initialized_range:
             p = cast(PO.CPOInitializedRange, p)
             args = [
diff --git a/chc/proof/CFilePredicateRecord.py b/chc/proof/CFilePredicateRecord.py
index 05e37d9..1e7e9f9 100644
--- a/chc/proof/CFilePredicateRecord.py
+++ b/chc/proof/CFilePredicateRecord.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
@@ -37,6 +37,7 @@
 if TYPE_CHECKING:
     from chc.app.CDictionary import CDictionary
     from chc.app.CFile import CFile
+    from chc.app.CFileDeclarations import CFileDeclarations
     from chc.proof.CFilePredicateDictionary import CFilePredicateDictionary
 
 
@@ -59,6 +60,10 @@ def pd(self) -> "CFilePredicateDictionary":
     def cd(self) -> "CDictionary":
         return self.pd.dictionary
 
+    @property
+    def cdeclarations(self) -> "CFileDeclarations":
+        return self.cfile.declarations
+
     @property
     def cfile(self) -> "CFile":
         return self.pd.cfile
diff --git a/chc/proof/CFunPODictionary.py b/chc/proof/CFunPODictionary.py
index 3fbb5a8..63ce515 100644
--- a/chc/proof/CFunPODictionary.py
+++ b/chc/proof/CFunPODictionary.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
@@ -36,6 +36,8 @@
 from typing import Callable, Dict, List, Mapping, TYPE_CHECKING
 
 from chc.proof.AssumptionType import AssumptionType
+from chc.proof.OutputParameterRejectionReason import OutputParameterRejectionReason
+from chc.proof.OutputParameterStatus import OutputParameterStatus
 from chc.proof.CFunPODictionaryRecord import podregistry
 from chc.proof.PPOType import PPOType
 from chc.proof.SPOType import SPOType
@@ -66,10 +68,16 @@ def __init__(
             cfun: "CFunction",
             xnode: ET.Element) -> None:
         self._cfun = cfun
+        self.output_parameter_rejection_reason_table = IndexedTable(
+            "output-parameter-rejection-reason-table")
+        self.output_parameter_status_table = IndexedTable(
+            "output-parameter-status-table")
         self.assumption_type_table = IndexedTable("assumption-table")
         self.ppo_type_table = IndexedTable("ppo-type-table")
         self.spo_type_table = IndexedTable("spo-type-table")
         self.tables = [
+            self.output_parameter_rejection_reason_table,
+            self.output_parameter_status_table,
             self.assumption_type_table,
             self.ppo_type_table,
             self.spo_type_table]
@@ -102,6 +110,19 @@ def interfacedictionary(self) -> "InterfaceDictionary":
 
     # ------------------------ Retrieve items from dictionary ----------------
 
+    def get_output_parameter_rejection_reason(
+            self, ix: int) -> OutputParameterRejectionReason:
+        return podregistry.mk_instance(
+            self,
+            self.output_parameter_rejection_reason_table.retrieve(ix),
+            OutputParameterRejectionReason)
+
+    def get_output_parameter_status(self, ix: int) -> OutputParameterStatus:
+        return podregistry.mk_instance(
+            self,
+            self.output_parameter_status_table.retrieve(ix),
+            OutputParameterStatus)
+
     def get_assumption_type(self, ix: int) -> AssumptionType:
         return podregistry.mk_instance(
             self, self.assumption_type_table.retrieve(ix), AssumptionType)
@@ -125,6 +146,14 @@ def get_spo_type_map(self) -> Dict[int, IndexedTableValue]:
 
     # ------------------------- Provide read/write xml service ---------------
 
+    def read_xml_output_parameter_status(
+            self, txnode: ET.Element, tag: str = "icops") -> OutputParameterStatus:
+        optix = txnode.get(tag)
+        if optix is not None:
+            return self.get_output_parameter_status(int(optix))
+        else:
+            raise UF.CHCError("Error in reading output-parameter-status")
+
     def read_xml_assumption_type(
             self, txnode: ET.Element, tag: str = "iast") -> AssumptionType:
         optix = txnode.get(tag)
diff --git a/chc/proof/CFunPODictionaryRecord.py b/chc/proof/CFunPODictionaryRecord.py
index fd9c8dc..b673819 100644
--- a/chc/proof/CFunPODictionaryRecord.py
+++ b/chc/proof/CFunPODictionaryRecord.py
@@ -36,6 +36,7 @@
     from chc.app.CApplication import CApplication
     from chc.app.CContext import ProgramContext
     from chc.app.CContextDictionary import CContextDictionary
+    from chc.app.CDictionary import CDictionary
     from chc.app.CFile import CFile
     from chc.app.CFileDeclarations import CFileDeclarations
     from chc.app.CFunction import CFunction
@@ -75,6 +76,10 @@ def cfile(self) -> "CFile":
     def cdecls(self) -> "CFileDeclarations":
         return self.cfile.declarations
 
+    @property
+    def cdictionary(self) -> "CDictionary":
+        return self.cfile.dictionary
+
     @property
     def cxd(self) -> "CContextDictionary":
         return self.cfile.contextdictionary
diff --git a/chc/proof/CFunctionAnalysisDigest.py b/chc/proof/CFunctionAnalysisDigest.py
new file mode 100644
index 0000000..a10b28f
--- /dev/null
+++ b/chc/proof/CFunctionAnalysisDigest.py
@@ -0,0 +1,226 @@
+# ------------------------------------------------------------------------------
+# 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.
+# ------------------------------------------------------------------------------
+
+import xml.etree.ElementTree as ET
+
+from typing import cast, List, Optional, TYPE_CHECKING
+
+from chc.proof.CandidateOutputParameter import CandidateOutputParameter
+from chc.proof.OutputParameterCalleeCallsite import OutputParameterCalleeCallsite
+
+from chc.util.loggingutil import chklogger
+
+if TYPE_CHECKING:
+    from chc.app.CApplication import CApplication
+    from chc.app.CFile import CFile
+    from chc.app.CFileDeclarations import CFileDeclarations
+    from chc.app.CFunction import CFunction
+    from chc.app.CVarInfo import CVarInfo
+    from chc.proof.CFunPODictionary import CFunPODictionary
+    from chc.proof.OutputParameterStatus import OutputParameterStatusRejected
+
+
+class CFunctionAnalysisDigest:
+
+    def __init__(self, cfun: "CFunction", xnode: ET.Element) -> None:
+        self.xnode = xnode   # analysis-digest node in adg file
+        self._cfun = cfun
+
+    @property
+    def cfun(self) -> "CFunction":
+        return self._cfun
+
+    @property
+    def cfile(self) -> "CFile":
+        return self.cfun.cfile
+
+    @property
+    def is_active(self) -> bool:
+        return True
+
+    @property
+    def capp(self) -> "CApplication":
+        return self.cfile.capp
+
+    def viable_parameters(self) -> List[CandidateOutputParameter]:
+        return []
+
+    def outputparameters(self) -> List[CandidateOutputParameter]:
+        return []
+
+    def maybe_parameters(self) -> List[CandidateOutputParameter]:
+        return []
+
+
+class CFunctionOutputParameterAnalysisDigest(CFunctionAnalysisDigest):
+
+    def __init__(self, cfun: "CFunction", xnode: ET.Element) -> None:
+        CFunctionAnalysisDigest.__init__(self, cfun, xnode)
+        self._candidate_parameters: Optional[List[CandidateOutputParameter]] = None
+        self._callee_callsites: Optional[List[OutputParameterCalleeCallsite]] = None
+        self._caller_callsites: Optional[List[OutputParameterCalleeCallsite]] = None
+
+    @property
+    def parameters(self) -> List[CandidateOutputParameter]:
+        if self._candidate_parameters is None:
+            self._candidate_parameters = []
+            xparams = self.xnode.find("candidate-parameters")
+            if xparams is not None:
+                for xparam in xparams.findall("param"):
+                    cparam = CandidateOutputParameter(self, xparam)
+                    self._candidate_parameters.append(cparam)
+        return self._candidate_parameters
+
+    def has_parameters(self) -> bool:
+        return len(self.parameters) > 0
+
+    @property
+    def callee_callsites(self) -> List[OutputParameterCalleeCallsite]:
+        if self._callee_callsites is None:
+            self._callee_callsites = []
+            xsites = self.xnode.find("callee-callsites")
+            if xsites is not None:
+                for xsite in xsites.findall("ccs"):
+                    ccsite = OutputParameterCalleeCallsite(self, xsite)
+                    self._callee_callsites.append(ccsite)
+        return self._callee_callsites
+
+    @property
+    def caller_callsites(self) -> List[OutputParameterCalleeCallsite]:
+        if self._caller_callsites is None:
+            self._caller_callsites = []
+            callinstrs = self.capp.get_callinstrs()
+            for callinstr in callinstrs:
+                if str(callinstr.callee) == self.cfun.name:
+                    caller = callinstr.cfun
+                    cfunadgs = caller.analysis_digests
+                    if len(cfunadgs.digests) == 1:
+                        cfunadg = cfunadgs.digests[0]
+                        cfunadg = cast(
+                            "CFunctionOutputParameterAnalysisDigest", cfunadg)
+                        callsites = cfunadg.callee_callsites
+                        callsites = [
+                            callsite for callsite in callsites
+                            if str(callsite.callee) == self.cfun.name]
+                        self._caller_callsites = callsites
+        return self._caller_callsites
+
+    @property
+    def is_active(self) -> bool:
+        if self.has_parameters():
+            if all(p.status.is_rejected for p in self.parameters):
+                return False
+            else:
+                return True
+        else:
+            return False
+
+    def outputparameters(self) -> List[CandidateOutputParameter]:
+        return self.parameters
+
+    def viable_parameters(self) -> List[CandidateOutputParameter]:
+        return [p for p in self.parameters if p.is_viable()]
+
+    def maybe_parameters(self) -> List[CandidateOutputParameter]:
+        return [p for p in self.parameters if not (p.status.is_rejected or p.is_viable())]
+
+    def __str__(self) -> str:
+        lines: List[str] = []
+        for p in self.parameters:
+            if p.status.is_rejected:
+                pstatus = cast("OutputParameterStatusRejected", p.status)
+                lines.append(
+                    " X " + str(p.parameter_index) + " " + str(p.parameter))
+                lines.append(
+                    "Reasons: " + "\n".join(str(r) for r in pstatus.reasons))
+            elif p.is_viable():
+                lines.append(" v " + str(p.parameter_index) + " " + str(p))
+            else:
+                lines.append(" ? " + str(p.parameter_index) + " " + str(p))
+        if any(p.is_viable() for p in self.parameters):
+            if len(self.caller_callsites) > 0:
+                lines.append("\nCaller-callsites:")
+                for ccs in self.caller_callsites:
+                    lines.append("  " + str(ccs))
+        return "\n".join(lines)
+
+
+class CFunctionAnalysisDigests:
+
+    def __init__(self, cfun: "CFunction", xnode: Optional[ET.Element]) -> None:
+        self._cfun = cfun
+        self.xnode = xnode    # analysis-digests node
+        self._digests: Optional[List[CFunctionAnalysisDigest]] = None
+
+    @property
+    def cfun(self) -> "CFunction":
+        return self._cfun
+
+    @property
+    def digests(self) -> List[CFunctionAnalysisDigest]:
+        if self._digests is None:
+            self._digests = []
+            if self.xnode is not None:
+                for xdigest in self.xnode.findall("analysis-digest"):
+                    digestkind = xdigest.get("name", "none")
+                    if digestkind == "output parameters":
+                        digest = CFunctionOutputParameterAnalysisDigest(
+                            self.cfun, xdigest)
+                        self._digests.append(digest)
+            else:
+                chklogger.logger.warning("Adg xnode is None")
+        return self._digests
+
+    def outputparameters(self) -> List[CandidateOutputParameter]:
+        result: List[CandidateOutputParameter] = []
+        for d in self.digests:
+            result.extend(d.outputparameters())
+        return result
+
+    def viable_outputparameters(self) -> List[CandidateOutputParameter]:
+        result: List[CandidateOutputParameter] = []
+        for d in self.digests:
+            result.extend(d.viable_parameters())
+        return result
+
+    def maybe_outputparameters(self) -> List[CandidateOutputParameter]:
+        result: List[CandidateOutputParameter] = []
+        for d in self.digests:
+            result.extend(d.maybe_parameters())
+        return result
+
+    @property
+    def is_active(self) -> bool:
+        if len(self.digests) == 1:
+            return self.digests[0].is_active
+        return False
+
+    def __str__(self) -> str:
+        lines: List[str] = []
+        for digest in self.digests:
+            lines.append(str(digest))
+        return "\n".join(lines)
diff --git a/chc/proof/CFunctionCallsiteSPO.py b/chc/proof/CFunctionCallsiteSPO.py
index 0216e74..d3fa442 100644
--- a/chc/proof/CFunctionCallsiteSPO.py
+++ b/chc/proof/CFunctionCallsiteSPO.py
@@ -39,7 +39,7 @@
     from chc.proof.CFunPODictionaryRecord import CFunPOType
     from chc.proof.CFunctionProofs import CFunctionProofs
     from chc.proof.CProofDependencies import CProofDependencies
-    from chc.proof.CProofDiagnostic import CProofDiagnostic
+    from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg
     from chc.proof.SPOType import CallsiteSPOType
 
 
@@ -52,7 +52,7 @@ def __init__(
             potype: "CFunPOType",
             status: str = "open",
             deps: Optional["CProofDependencies"] = None,
-            expl: Optional[str] = None,
+            expl: Optional["SituatedMsg"] = None,
             diag: Optional["CProofDiagnostic"] = None) -> None:
         CFunctionPO.__init__(self, cproofs, potype, status, deps, expl, diag)
 
diff --git a/chc/proof/CFunctionCallsiteSPOs.py b/chc/proof/CFunctionCallsiteSPOs.py
index 99697bf..bf90da5 100644
--- a/chc/proof/CFunctionCallsiteSPOs.py
+++ b/chc/proof/CFunctionCallsiteSPOs.py
@@ -43,7 +43,7 @@
 from chc.proof.CFunctionCallsiteSPO import CFunctionCallsiteSPO
 from chc.proof.CFunctionPO import po_status
 from chc.proof.CProofDependencies import CProofDependencies
-from chc.proof.CProofDiagnostic import CProofDiagnostic
+from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg
 
 import chc.util.fileutil as UF
 from chc.util.loggingutil import chklogger
@@ -233,8 +233,10 @@ def spos(self) -> Dict[int, List[CFunctionCallsiteSPO]]:
                             deps = CProofDependencies(self.cproofs, xpo)
                             status = po_status[xpo.get("s", "o")]
                             xexpl = xpo.find("e")
-                            expl = None if xexpl is None else xexpl.get("txt")
-                            diagnostic = CProofDiagnostic(xpo.find("d"))
+                            expl = (
+                                None if xexpl is None
+                                else SituatedMsg(self.cfun.cdictionary, xexpl))
+                            diagnostic = CProofDiagnostic(self.cproofs, xpo.find("d"))
                             self._spos[int(xapid)].append(
                                 CFunctionCallsiteSPO(
                                     self.cproofs,
diff --git a/chc/proof/CFunctionLocalSPO.py b/chc/proof/CFunctionLocalSPO.py
index 91f1fe5..6b6930e 100644
--- a/chc/proof/CFunctionLocalSPO.py
+++ b/chc/proof/CFunctionLocalSPO.py
@@ -38,7 +38,7 @@
     from chc.proof.CFunctionProofs import CFunctionProofs
     from chc.proof.CFunPODictionaryRecord import CFunPOType
     from chc.proof.CProofDependencies import CProofDependencies
-    from chc.proof.CProofDiagnostic import CProofDiagnostic
+    from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg
 
 
 class CFunctionLocalSPO(CFunctionPO):
@@ -49,7 +49,7 @@ def __init__(
             potype: "CFunPOType",
             status: str = "open",
             deps: Optional["CProofDependencies"] = None,
-            expl: Optional[str] = None,
+            expl: Optional["SituatedMsg"] = None,
             diag: Optional["CProofDiagnostic"] = None) -> None:
         CFunctionPO.__init__(self, cproofs, potype, status, deps, expl, diag)
 
diff --git a/chc/proof/CFunctionPO.py b/chc/proof/CFunctionPO.py
index 05f5af2..e0f5be3 100644
--- a/chc/proof/CFunctionPO.py
+++ b/chc/proof/CFunctionPO.py
@@ -47,7 +47,7 @@
     from chc.proof.CFunPODictionary import CFunPODictionary
     from chc.proof.CPOPredicate import CPOPredicate
     from chc.proof.CProofDependencies import CProofDependencies
-    from chc.proof.CProofDiagnostic import CProofDiagnostic
+    from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg
     from chc.proof.SPOType import SPOType
 
 
@@ -72,7 +72,7 @@ def __init__(
             potype: CFunPOType,
             status: str = "open",
             deps: Optional["CProofDependencies"] = None,
-            expl: Optional[str] = None,
+            expl: Optional["SituatedMsg"] = None,
             diag: Optional["CProofDiagnostic"] = None) -> None:
         self._cproofs = cproofs
         self._potype = potype
@@ -182,7 +182,7 @@ def has_dependencies(self) -> bool:
         return self._dependencies is not None
 
     @property
-    def explanation(self) -> Optional[str]:
+    def explanation(self) -> Optional["SituatedMsg"]:
         return self._explanation
 
     def has_explanation(self) -> bool:
@@ -364,7 +364,7 @@ def write_xml(self, cnode: ET.Element) -> None:
             self.dependencies.write_xml(cnode)
         if self.explanation is not None:
             enode = ET.Element("e")
-            enode.set("txt", self.explanation)
+            enode.set("txt", self.explanation.msg)
             cnode.append(enode)
         if self.has_diagnostic():
             dnode = ET.Element("d")
diff --git a/chc/proof/CFunctionPPO.py b/chc/proof/CFunctionPPO.py
index 9f87298..f2f4735 100644
--- a/chc/proof/CFunctionPPO.py
+++ b/chc/proof/CFunctionPPO.py
@@ -38,7 +38,7 @@
     from chc.proof.CFunctionProofs import CFunctionProofs
     from chc.proof.CFunPODictionaryRecord import CFunPOType
     from chc.proof.CProofDependencies import CProofDependencies
-    from chc.proof.CProofDiagnostic import CProofDiagnostic
+    from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg
 
 
 class CFunctionPPO(CFunctionPO):
@@ -50,7 +50,7 @@ def __init__(
             ppotype: "CFunPOType",
             status: str = "open",
             deps: Optional["CProofDependencies"] = None,
-            expl: Optional[str] = None,
+            expl: Optional["SituatedMsg"] = None,
             diag: Optional["CProofDiagnostic"] = None) -> None:
         CFunctionPO.__init__(self, cproofs, ppotype, status, deps, expl, diag)
 
diff --git a/chc/proof/CFunctionPPOs.py b/chc/proof/CFunctionPPOs.py
index 0145b12..d7e3e8c 100644
--- a/chc/proof/CFunctionPPOs.py
+++ b/chc/proof/CFunctionPPOs.py
@@ -34,7 +34,7 @@
 
 from chc.proof.CFunctionPPO import CFunctionPPO
 from chc.proof.CProofDependencies import CProofDependencies
-from chc.proof.CProofDiagnostic import CProofDiagnostic
+from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg
 
 import chc.util.fileutil as UF
 
@@ -90,12 +90,13 @@ def ppos(self) -> Dict[int, CFunctionPPO]:
                 id = ppotype.index
                 status = po_status[xp.get("s", "o")]
                 deps = CProofDependencies(self.cproofs, xp)
-                diagnostic = CProofDiagnostic(xp.find("d"))
+                diagnostic = CProofDiagnostic(self.cproofs, xp.find("d"))
 
                 # get explanation
                 enode = xp.find("e")
                 if enode is not None:
-                    expl: Optional[str] = enode.get("txt", "")
+                    expl: Optional[SituatedMsg] = SituatedMsg(
+                        self.cfun.cdictionary, enode)
                 else:
                     expl = None
 
diff --git a/chc/proof/CFunctionProofs.py b/chc/proof/CFunctionProofs.py
index c4e0187..91ce44c 100644
--- a/chc/proof/CFunctionProofs.py
+++ b/chc/proof/CFunctionProofs.py
@@ -30,7 +30,7 @@
 
 import xml.etree.ElementTree as ET
 
-from typing import Callable, List, Optional, TYPE_CHECKING
+from typing import Callable, cast, List, Optional, TYPE_CHECKING
 
 from chc.proof.CFunctionCallsiteSPOs import CFunctionCallsiteSPOs
 from chc.proof.CFunctionPO import CFunctionPO
@@ -44,6 +44,10 @@
     from chc.app.CApplication import CApplication
     from chc.app.CFile import CFile
     from chc.app.CFunction import CFunction
+    from chc.proof.CPOPredicate import (
+        CPOLocallyInitialized,
+        CPOOutputParameterInitialized,
+        CPOOutputParameterUnaltered)
 
 
 class CFunctionProofs:
@@ -240,6 +244,23 @@ def _get_spos(self, force=False):
                     + self.cfile.name
                 )
 
+    def get_output_parameter_ppos(self, vname: str) -> List[CFunctionPO]:
+        result: List[CFunctionPO] = []
+        for ppo in self.ppolist:
+            if ppo.predicate.is_locally_initialized:
+                vinfo = cast("CPOLocallyInitialized", ppo.predicate).varinfo
+                if vinfo.vname == vname:
+                    result.append(ppo)
+            elif ppo.predicate.is_output_parameter_initialized:
+                vinfo = cast("CPOOutputParameterInitialized", ppo.predicate).varinfo
+                if vinfo.vname == vname:
+                    result.append(ppo)
+            elif ppo.predicate.is_output_parameter_unaltered:
+                vinfo = cast("CPOOutputParameterUnaltered", ppo.predicate).varinfo
+                if vinfo.vname == vname:
+                    result.append(ppo)
+        return result
+
     def _save_spos(self, cnode: ET.Element) -> None:
         UF.save_spo_file(
             self.targetpath,
diff --git a/chc/proof/CFunctionReturnsiteSPO.py b/chc/proof/CFunctionReturnsiteSPO.py
index a77fd30..e17579b 100644
--- a/chc/proof/CFunctionReturnsiteSPO.py
+++ b/chc/proof/CFunctionReturnsiteSPO.py
@@ -38,7 +38,7 @@
     from chc.proof.CFunctionReturnsiteSPOs import CFunctionReturnsiteSPOs
     from chc.proof.CFunPODictionaryRecord import CFunPOType
     from chc.proof.CProofDependencies import CProofDependencies
-    from chc.proof.CProofDiagnostic import CProofDiagnostic
+    from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg
     from chc.proof.SPOType import SPOType
 
 
@@ -51,7 +51,7 @@ def __init__(
             potype: "CFunPOType",
             status: str = "open",
             deps: Optional["CProofDependencies"] = None,
-            expl: Optional[str] = None,
+            expl: Optional["SituatedMsg"] = None,
             diag: Optional["CProofDiagnostic"] = None) -> None:
         CFunctionPO.__init__(
             self, crspos.cproofs, potype, status, deps, expl, diag)
diff --git a/chc/proof/CFunctionReturnsiteSPOs.py b/chc/proof/CFunctionReturnsiteSPOs.py
index d407948..2268909 100644
--- a/chc/proof/CFunctionReturnsiteSPOs.py
+++ b/chc/proof/CFunctionReturnsiteSPOs.py
@@ -39,7 +39,7 @@
 
 from chc.proof.CFunctionReturnsiteSPO import CFunctionReturnsiteSPO
 from chc.proof.CProofDependencies import CProofDependencies
-from chc.proof.CProofDiagnostic import CProofDiagnostic
+from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg
 
 import chc.util.fileutil as UF
 
@@ -107,8 +107,10 @@ def spos(self) -> Dict[int, List[CFunctionReturnsiteSPO]]:
                         deps = CProofDependencies(self.cproofs, xpo)
                         status = po_status[xpo.get("s", "o")]
                         xexpl = xpo.find("e")
-                        expl = None if xexpl is None else xexpl.get("txt")
-                        diagnostic = CProofDiagnostic(xpo.find("d"))
+                        expl = (
+                            None if xexpl is None
+                            else SituatedMsg(self.cfun.cdictionary, xexpl))
+                        diagnostic = CProofDiagnostic(self.cproofs, xpo.find("d"))
                         self._spos[ipc].append(
                             CFunctionReturnsiteSPO(
                                 self, spotype, status, deps, expl, diagnostic))
diff --git a/chc/proof/CFunctionSPOs.py b/chc/proof/CFunctionSPOs.py
index fbebd26..5527013 100644
--- a/chc/proof/CFunctionSPOs.py
+++ b/chc/proof/CFunctionSPOs.py
@@ -40,7 +40,7 @@
 from chc.proof.CFunctionPO import CFunctionPO
 from chc.proof.CFunctionPO import po_status
 from chc.proof.CProofDependencies import CProofDependencies
-from chc.proof.CProofDiagnostic import CProofDiagnostic
+from chc.proof.CProofDiagnostic import CProofDiagnostic, SituatedMsg
 
 from chc.util.loggingutil import chklogger
 
@@ -103,9 +103,11 @@ def local_spos(self) -> Dict[int, CFunctionLocalSPO]:
                 for xpo in xlspos.findall("po"):
                     spotype = self.podictionary.read_xml_spo_type(xpo)
                     xexpl = xpo.find("e")
-                    expl = None if xexpl is None else xexpl.get("txt")
+                    expl = (
+                        None if xexpl is None
+                        else SituatedMsg(self.cfun.cdictionary, xexpl))
                     deps = CProofDependencies(self.cproofs, xpo)
-                    diagnostic = CProofDiagnostic(xpo.find("d"))
+                    diagnostic = CProofDiagnostic(self.cproofs, xpo.find("d"))
                     status = po_status[xpo.get("s", "o")]
                     self._localspos[spotype.po_index] = CFunctionLocalSPO(
                         self.cproofs, spotype, status, deps, expl, diagnostic)
diff --git a/chc/proof/CPOPredicate.py b/chc/proof/CPOPredicate.py
index bc2335e..2003f4c 100644
--- a/chc/proof/CPOPredicate.py
+++ b/chc/proof/CPOPredicate.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,7 +40,9 @@
     from chc.app.CExp import CExp, CExpLval
     from chc.app.CLHost import CLHostVar
     from chc.app.CLval import CLval
+    from chc.app.COffset import COffset
     from chc.app.CTyp import CTyp
+    from chc.app.CVarInfo import CVarInfo
     from chc.proof.CFilePredicateDictionary import CFilePredicateDictionary
 
 
@@ -71,12 +73,18 @@
     'iu': 'int-underflow',
     'iub': 'index-upper-bound',
     'lb': 'lower-bound',
+    'li': 'locally-initialized',
     'nm': 'new-memory',
     'nn': 'not-null',
     'nneg': 'non-negative',
     'no': 'no-overlap',
     'nt': 'null-terminated',
     'null': 'null',
+    "opa": "output_parameter-argument",
+    'opi': 'output_parameter-initialized',
+    "opne": "output_parameter-no-escape",
+    "ops": "output_parameter-scalar",
+    'opu': 'output_parameter-unaltered',
     'pc': 'pointer-cast',
     'plb': 'ptr-lower-bound',
     'pre': 'precondition',
@@ -89,6 +97,7 @@
     'ub': 'upper-bound',
     'uio': 'uint-overflow',
     'uiu': 'uint-underflow',
+    'up': 'unique-pointer',
     'va': 'var-args',
     'vc': 'value-constraint',
     'vm': 'valid-mem',
@@ -180,6 +189,10 @@ def is_index_upper_bound(self) -> bool:
     def is_initialized(self) -> bool:
         return False
 
+    @property
+    def is_locally_initialized(self) -> bool:
+        return False
+
     @property
     def is_initialized_range(self) -> bool:
         return False
@@ -224,6 +237,14 @@ def is_null(self) -> bool:
     def is_null_terminated(self) -> bool:
         return False
 
+    @property
+    def is_output_parameter_initialized(self) -> bool:
+        return False
+
+    @property
+    def is_output_parameter_unaltered(self) -> bool:
+        return False
+
     @property
     def is_pointer_cast(self) -> bool:
         return False
@@ -280,6 +301,10 @@ def is_stack_address_escape(self) -> bool:
     def is_type_at_offset(self) -> bool:
         return False
 
+    @property
+    def is_unique_pointer(self) -> bool:
+        return False
+
     @property
     def is_upper_bound(self) -> bool:
         return False
@@ -962,6 +987,48 @@ def __str__(self) -> str:
         return "initialized(" + str(self.lval) + ")"
 
 
+@pdregistry.register_tag("li", CPOPredicate)
+class CPOLocallyInitialized(CPOPredicate):
+    """locally initialized(lval): location initialized within the function.
+
+    - args[0]: index of lval in cdictionary
+    """
+
+    def __init__(
+            self, pd: "CFilePredicateDictionary", ixval: IT.IndexedTableValue
+            ) -> None:
+        CPOPredicate.__init__(self, pd, ixval)
+
+    @property
+    def varinfo(self) -> "CVarInfo":
+        return self.cdeclarations.get_varinfo(self.args[0])
+
+    @property
+    def lval(self) -> "CLval":
+        return self.cd.get_lval(self.args[1])
+
+    @property
+    def is_locally_initialized(self) -> bool:
+        return True
+
+    def has_variable(self, vid: int) -> bool:
+        return self.lval.has_variable(vid)
+
+    def has_variable_deref(self, vid: int) -> bool:
+        return self.lval.has_variable_deref(vid)
+
+    def has_ref_type(self) -> bool:
+        return self.lval.has_ref_type()
+
+    def __str__(self) -> str:
+        return (
+            "locally-initialized("
+            + str(self.varinfo.vname)
+            + ", "
+            + str(self.lval)
+            + ")")
+
+
 @pdregistry.register_tag("ir", CPOPredicate)
 class CPOInitializedRange(CPOPredicate):
     """initialized-range(exp, size): the memory range starting at the address
@@ -2123,6 +2190,29 @@ def __str__(self) -> str:
         return "value-constraint(" + str(self.exp) + ")"
 
 
+@pdregistry.register_tag("up", CPOPredicate)
+class CPOUniquePointer(CPOPredicate):
+
+    def __init__(
+            self, pd: "CFilePredicateDictionary", ixval: IT.IndexedTableValue
+    ) -> None:
+        CPOPredicate.__init__(self, pd, ixval)
+
+    @property
+    def exp(self) -> "CExp":
+        return self.cd.get_exp(self.args[0])
+
+    @property
+    def is_unique_pointer(self) -> bool:
+        return True
+
+    def has_variable(self, vid: int) -> bool:
+        return self.exp.has_variable(vid)
+
+    def __str__(self) -> str:
+        return "unique-pointer(" + str(self.exp) + ")"
+
+
 @pdregistry.register_tag("prm", CPOPredicate)
 class CPOPreservedAllMemory(CPOPredicate):
     """preserves-all-memory(): true of a function that does not free any memory.
@@ -2162,3 +2252,135 @@ def has_variable(self, vid: int) -> bool:
 
     def __str__(self) -> str:
         return "preserves-value(" + str(self.exp) + ")"
+
+
+@pdregistry.register_tag("opi", CPOPredicate)
+class CPOOutputParameterInitialized(CPOPredicate):
+    """
+
+    - args[0]: index of varinfo in cdecls
+    """
+    def __init__(
+            self, pd: "CFilePredicateDictionary", ixval: IT.IndexedTableValue
+    ) -> None:
+        CPOPredicate.__init__(self, pd, ixval)
+
+    @property
+    def varinfo(self) -> "CVarInfo":
+        return self.cdeclarations.get_varinfo(self.args[0])
+
+    @property
+    def offset(self) -> "COffset":
+        return self.cd.get_offset(self.args[1])
+
+    @property
+    def is_output_parameter_initialized(self) -> bool:
+        return True
+
+    def has_variable(self, vid: int) -> bool:
+        return self.varinfo.vid == vid
+
+    def __str__(self) -> str:
+        return (
+            "output_parameter-initialized("
+            + str(self.varinfo.vname)
+            + ", "
+            + str(self.offset)
+            + ")")
+
+
+@pdregistry.register_tag("opu", CPOPredicate)
+class CPOOutputParameterUnaltered(CPOPredicate):
+    """
+
+    - args[0]: index of varinfo in cdecls
+    """
+    def __init__(
+            self, pd: "CFilePredicateDictionary", ixval: IT.IndexedTableValue
+    ) -> None:
+        CPOPredicate.__init__(self, pd, ixval)
+
+    @property
+    def varinfo(self) -> "CVarInfo":
+        return self.cdeclarations.get_varinfo(self.args[0])
+
+    @property
+    def offset(self) -> "COffset":
+        return self.cd.get_offset(self.args[1])
+
+    @property
+    def is_output_parameter_unaltered(self) -> bool:
+        return True
+
+    def has_variable(self, vid: int) -> bool:
+        return self.varinfo.vid == vid
+
+    def __str__(self) -> str:
+        return (
+            "output_parameter-unaltered("
+            + str(self.varinfo.vname)
+            + ", "
+            + str(self.offset)
+            + ")")
+
+
+@pdregistry.register_tag("opa", CPOPredicate)
+class CPOOutputParameterArgument(CPOPredicate):
+
+    def __init__(
+            self, pd: "CFilePredicateDictionary", ixval: IT.IndexedTableValue
+    ) -> None:
+        CPOPredicate.__init__(self, pd, ixval)
+
+    @property
+    def exp(self) -> "CExp":
+        return self.cd.get_exp(self.args[0])
+
+    def __str__(self) -> str:
+        return "output-parameter-argument(" + str(self.exp) + ")"
+
+
+@pdregistry.register_tag("ops", CPOPredicate)
+class CPOOutputParameterScalar(CPOPredicate):
+
+    def __init__(
+            self, pd: "CFilePredicateDictionary", ixval: IT.IndexedTableValue
+    ) -> None:
+        CPOPredicate.__init__(self, pd, ixval)
+
+    @property
+    def varinfo(self) -> "CVarInfo":
+        return self.cdeclarations.get_varinfo(self.args[0])
+
+    @property
+    def exp(self) -> "CExp":
+        return self.cd.get_exp(self.args[1])
+
+    def __str__(self) -> str:
+        return (
+            "output-parameter-scalar("
+            + str(self.varinfo) + ", "
+            + str(self.exp) + ")")
+
+
+@pdregistry.register_tag("opne", CPOPredicate)
+class CPOOutputParameterNoEscape(CPOPredicate):
+
+    def __init__(
+            self, pd: "CFilePredicateDictionary", ixval: IT.IndexedTableValue
+    ) -> None:
+        CPOPredicate.__init__(self, pd, ixval)
+
+    @property
+    def varinfo(self) -> "CVarInfo":
+        return self.cdeclarations.get_varinfo(self.args[0])
+
+    @property
+    def exp(self) -> "CExp":
+        return self.cd.get_exp(self.args[1])
+
+    def __str__(self) -> str:
+        return (
+            "output-parameter-no-escape("
+            + str(self.varinfo) + ", "
+            + str(self.exp) + ")")
diff --git a/chc/proof/CProofDiagnostic.py b/chc/proof/CProofDiagnostic.py
index a5a504b..5f6a50f 100644
--- a/chc/proof/CProofDiagnostic.py
+++ b/chc/proof/CProofDiagnostic.py
@@ -32,15 +32,88 @@
 
 from typing import Dict, List, Optional, TYPE_CHECKING
 
+if TYPE_CHECKING:
+    from chc.app.CDictionary import CDictionary
+    from chc.app.CFunction import CFunction
+    from chc.proof.CFunctionProofs import CFunctionProofs
+
+
+class SituatedMsg:
+
+    def __init__(self, cd: "CDictionary", xnode: ET.Element) -> None:
+        self._cd = cd
+        self._xnode = xnode
+
+    @property
+    def cd(self) -> "CDictionary":
+        return self._cd
+
+    @property
+    def msg(self) -> str:
+        result = self._xnode.get("t")
+        if result is None:
+            return self._xnode.get("txt", "?")
+        else:
+            return result
+
+    @property
+    def file(self) -> Optional[str]:
+        xfile = self._xnode.get("file")
+        if xfile is not None:
+            return self.cd.get_string(int(xfile))
+        return None
+
+    @property
+    def line(self) -> Optional[int]:
+        xline = self._xnode.get("line")
+        if xline is not None:
+            return int(xline)
+        return None
+
+    @property
+    def detail(self) -> Optional[str]:
+        xdetail = self._xnode.get("detail")
+        if xdetail is not None:
+            return self.cd.get_string(int(xdetail))
+        return None
+
+    @property
+    def is_situated(self) -> bool:
+        return (
+            self.file is not None
+            and self.line is not None
+            and self.detail is not None)
+
+    def __str__(self) -> str:
+        if self.is_situated:
+            return self.msg + " (" + str(self.line) + ": " + str(self.detail) + ")"
+        else:
+            return self.msg
+
 
 class CProofDiagnostic:
 
-    def __init__(self, xnode: Optional[ET.Element]) -> None:
+    def __init__(
+            self, cproofs: "CFunctionProofs", xnode: Optional[ET.Element]
+    ) -> None:
+        self._cproofs = cproofs
         self._xnode = xnode
         self._invsmap: Optional[Dict[int, List[int]]] = None
-        self._amsgs: Optional[Dict[int, List[str]]] = None
+        self._amsgs: Optional[Dict[int, List[SituatedMsg]]] = None
         self._kmsgs: Optional[Dict[str, List[str]]] = None
-        self._msgs: Optional[List[str]] = None
+        self._msgs: Optional[List[SituatedMsg]] = None
+
+    @property
+    def cproofs(self) -> "CFunctionProofs":
+        return self._cproofs
+
+    @property
+    def cfun(self) -> "CFunction":
+        return self.cproofs.cfun
+
+    @property
+    def cd(self) -> "CDictionary":
+        return self.cfun.cdictionary
 
     @property
     def invsmap(self) -> Dict[int, List[int]]:
@@ -63,7 +136,7 @@ def invsmap(self) -> Dict[int, List[int]]:
         return self._invsmap
 
     @property
-    def msgs(self) -> List[str]:
+    def msgs(self) -> List[SituatedMsg]:
         """Returns general diagnostics pertaining to the proof obligation."""
 
         if self._msgs is None:
@@ -71,11 +144,12 @@ def msgs(self) -> List[str]:
             if self._xnode is not None:
                 mnode = self._xnode.find("msgs")
                 if mnode is not None:
-                    self._msgs = [x.get("t", "") for x in mnode.findall("msg")]
+                    self._msgs = [
+                        SituatedMsg(self.cd, x) for x in mnode.findall("msg")]
         return self._msgs
 
     @property
-    def argument_msgs(self) -> Dict[int, List[str]]:
+    def argument_msgs(self) -> Dict[int, List[SituatedMsg]]:
         """Returns argument-specific diagnostic messages.
 
         Note: argument index starts at 1.
@@ -89,7 +163,8 @@ def argument_msgs(self) -> Dict[int, List[str]]:
                     for n in anode.findall("arg"):
                         xargindex = n.get("a")
                         if xargindex is not None:
-                            msgs = [x.get("t", "") for x in n.findall("msg")]
+                            msgs = [
+                                SituatedMsg(self.cd, x) for x in n.findall("msg")]
                             self._amsgs[int(xargindex)] = msgs
         return self._amsgs
 
@@ -132,9 +207,9 @@ def write_xml(self, dnode: ET.Element) -> None:
         for arg in self.argument_msgs:
             anode = ET.Element("arg")
             anode.set("a", str(arg))
-            for t in self.argument_msgs[arg]:
+            for msg in self.argument_msgs[arg]:
                 tnode = ET.Element("msg")
-                tnode.set("t", t)
+                tnode.set("t", msg.msg)
                 anode.append(tnode)
             aanode.append(anode)
         for key in self.keyword_msgs:
@@ -145,13 +220,13 @@ def write_xml(self, dnode: ET.Element) -> None:
                 tnode.set("t", t)
                 knode.append(tnode)
             kknode.append(knode)
-        for t in self.msgs:
+        for msg in self.msgs:
             mnode = ET.Element("msg")
-            mnode.set("t", t)
+            mnode.set("t", msg.msg)
             mmnode.append(mnode)
         dnode.extend([inode, mmnode, aanode, kknode])
 
     def __str__(self) -> str:
         if len(self.msgs) == 0:
             return "no diagnostic messages"
-        return "\n".join(self.msgs)
+        return "\n".join(str(m) for m in self.msgs)
diff --git a/chc/proof/CandidateOutputParameter.py b/chc/proof/CandidateOutputParameter.py
new file mode 100644
index 0000000..96ea9ec
--- /dev/null
+++ b/chc/proof/CandidateOutputParameter.py
@@ -0,0 +1,173 @@
+# ------------------------------------------------------------------------------
+# 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.
+# ------------------------------------------------------------------------------
+
+import xml.etree.ElementTree as ET
+
+from typing import List, Optional, TYPE_CHECKING
+
+if TYPE_CHECKING:
+    from chc.app.CFile import CFile
+    from chc.app.CFileDeclarations import CFileDeclarations
+    from chc.app.CFunction import CFunction
+    from chc.app.CLocation import CLocation
+    from chc.app.CVarInfo import CVarInfo
+    from chc.proof.CFunPODictionary import CFunPODictionary
+    from chc.proof.CFunctionAnalysisDigest import (
+        CFunctionOutputParameterAnalysisDigest)
+    from chc.proof.OutputParameterCalleeCallsite import (
+        OutputParameterCalleeCallsiteArg,
+        OutputParameterCalleeCallsite)
+    from chc.proof.OutputParameterStatus import OutputParameterStatus
+
+
+class COpParamReturnsite:
+
+    def __init__(self, cop: "CandidateOutputParameter", xnode: ET.Element) -> None:
+        self._cop = cop
+        self.xnode = xnode
+
+    @property
+    def cop(self) -> "CandidateOutputParameter":
+        return self._cop
+
+    @property
+    def cfun(self) -> "CFunction":
+        return self.cop.cfun
+
+    @property
+    def cfile(self) -> "CFile":
+        return self.cop.cfile
+
+    @property
+    def fdecls(self) -> "CFileDeclarations":
+        return self.cfile.declarations
+
+    @property
+    def podictionary(self) -> "CFunPODictionary":
+        return self.cfun.podictionary
+
+    @property
+    def location(self) -> "CLocation":
+        return self.fdecls.read_xml_location(self.xnode)
+
+    @property
+    def status(self) -> "OutputParameterStatus":
+        return self.podictionary.read_xml_output_parameter_status(self.xnode)
+
+    def is_viable(self) -> bool:
+        return self.status.is_written or self.status.is_unaltered
+
+    def __str__(self) -> str:
+        return str(self.location.line) + ": " + str(self.status)
+
+
+class CandidateOutputParameter:
+
+    def __init__(
+            self, adg: "CFunctionOutputParameterAnalysisDigest", xnode: ET.Element
+    ) -> None:
+        self._adg = adg
+        self.xnode = xnode    # param node
+        self._returnsites: Optional[List[COpParamReturnsite]] = None
+        self._caller_callsite_args: Optional[List["OutputParameterCalleeCallsiteArg"]] = None
+        # self._calldeps: Optional[List[CopParamCallDependency]] = None
+
+    @property
+    def adg(self) -> "CFunctionOutputParameterAnalysisDigest":
+        return self._adg
+
+    @property
+    def cfun(self) -> "CFunction":
+        return self.adg.cfun
+
+    @property
+    def cfile(self) -> "CFile":
+        return self.adg.cfile
+
+    @property
+    def podictionary(self) -> "CFunPODictionary":
+        return self.cfun.podictionary
+
+    @property
+    def fdecls(self) -> "CFileDeclarations":
+        return self.cfile.declarations
+
+    @property
+    def parameter(self) -> "CVarInfo":
+        return self.fdecls.read_xml_varinfo(self.xnode)
+
+    @property
+    def parameter_index(self) -> int:
+        """1-based index."""
+        return int(self.xnode.get("paramindex", -1))
+
+    @property
+    def status(self) -> "OutputParameterStatus":
+        return self.podictionary.read_xml_output_parameter_status(self.xnode)
+
+    @property
+    def returnsites(self) -> List[COpParamReturnsite]:
+        if self._returnsites is None:
+            self._returnsites = []
+            xreturns = self.xnode.find("returnsites")
+            if xreturns is not None:
+                for xreturn in xreturns.findall("rs"):
+                    returnsite = COpParamReturnsite(self, xreturn)
+                    self._returnsites.append(returnsite)
+        return self._returnsites
+
+    @property
+    def caller_callsite_args(self) -> List["OutputParameterCalleeCallsiteArg"]:
+        if self._caller_callsite_args is None:
+            self._caller_callsite_args = []
+            callsites = self.adg.caller_callsites
+            for callsite in callsites:
+                for callarg in callsite.callargs:
+                    if callarg.arg_index == self.parameter_index:
+                        self._caller_callsite_args.append(callarg)
+        return self._caller_callsite_args
+
+    def is_viable(self) -> bool:
+        if self.status.is_rejected:
+            return False
+        returns_viable = (
+            all(returnsite.is_viable() for returnsite in self.returnsites))
+        callers_viable = (
+            all(callarg.status.is_viable for callarg in self.caller_callsite_args))
+        return returns_viable and callers_viable
+
+    def __str__(self) -> str:
+        lines: List[str] = []
+        lines.append(str(self.parameter) + ": " + str(self.status))
+        if not self.status.is_rejected:
+            lines.append("   Return sites")
+            for returnsite in self.returnsites:
+                lines.append("       " + str(returnsite))
+            lines.append("   Call arguments")
+            for callsite_arg in self.caller_callsite_args:
+                lines.append("       " + str(callsite_arg))
+        return "\n".join(lines)
diff --git a/chc/proof/OutputParameterCalleeCallsite.py b/chc/proof/OutputParameterCalleeCallsite.py
new file mode 100644
index 0000000..3c45ffa
--- /dev/null
+++ b/chc/proof/OutputParameterCalleeCallsite.py
@@ -0,0 +1,181 @@
+# ------------------------------------------------------------------------------
+# 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.
+# ------------------------------------------------------------------------------
+
+import xml.etree.ElementTree as ET
+
+from typing import List, Optional, TYPE_CHECKING
+
+if TYPE_CHECKING:
+    from chc.app.CContext import ProgramContext
+    from chc.app.CContextDictionary import CContextDictionary
+    from chc.app.CExp import CExp
+    from chc.app.CFile import CFile
+    from chc.app.CFileDictionary import CFileDictionary
+    from chc.app.CFileDeclarations import CFileDeclarations
+    from chc.app.CFunction import CFunction
+    from chc.app.CLocation import CLocation
+    from chc.app.CVarInfo import CVarInfo
+    from chc.proof.CFunctionAnalysisDigest import (
+        CFunctionOutputParameterAnalysisDigest)
+    from chc.proof.CFunPODictionary import CFunPODictionary
+    from chc.proof.OutputParameterStatus import OutputParameterStatus
+
+
+class OutputParameterCalleeCallsiteArg:
+
+    def __init__(
+            self, opcallsite: "OutputParameterCalleeCallsite", xnode: ET.Element
+    ) -> None:
+        self._opcallsite = opcallsite
+        self.xnode = xnode
+
+    @property
+    def opcallsite(self) -> "OutputParameterCalleeCallsite":
+        return self._opcallsite
+
+    @property
+    def adg(self) -> "CFunctionOutputParameterAnalysisDigest":
+        return self.opcallsite.adg
+
+    @property
+    def cfun(self) -> "CFunction":
+        return self.adg.cfun
+
+    @property
+    def cfile(self) -> "CFile":
+        return self.adg.cfile
+
+    @property
+    def cdictionary(self) -> "CFileDictionary":
+        return self.cfile.dictionary
+
+    @property
+    def podictionary(self) -> "CFunPODictionary":
+        return self.cfun.podictionary
+
+    @property
+    def contextdictionary(self) -> "CContextDictionary":
+        return self.cfile.contextdictionary
+
+    @property
+    def fdecls(self) -> "CFileDeclarations":
+        return self.cfile.declarations
+
+    @property
+    def status(self) -> "OutputParameterStatus":
+        return self.podictionary.read_xml_output_parameter_status(self.xnode)
+
+    @property
+    def argument(self) -> "CExp":
+        return self.cdictionary.read_xml_exp(self.xnode)
+
+    @property
+    def context(self) -> "ProgramContext":
+        return self.contextdictionary.read_xml_context(self.xnode)
+
+    @property
+    def arg_index(self) -> int:
+        expctxt = self.context.exp_context
+        lastnode = expctxt.nodes[-1]
+        if str(lastnode).startswith("arg:"):
+            index = int(str(lastnode)[4:])
+            return index
+        else:
+            return -1
+
+    def __str__(self) -> str:
+        return (
+            str(self.status)
+            + " " + str(self.argument) + " (argindex: " + str(self.arg_index))
+
+
+class OutputParameterCalleeCallsite:
+
+    def __init__(
+            self, adg: "CFunctionOutputParameterAnalysisDigest", xnode: ET.Element
+    ) -> None:
+        self._adg = adg
+        self.xnode = xnode
+        self._callargs: Optional[List[OutputParameterCalleeCallsiteArg]] = None
+
+    @property
+    def adg(self) -> "CFunctionOutputParameterAnalysisDigest":
+        return self._adg
+
+    @property
+    def cfun(self) -> "CFunction":
+        return self.adg.cfun
+
+    @property
+    def cfile(self) -> "CFile":
+        return self.adg.cfile
+
+    @property
+    def cdictionary(self) -> "CFileDictionary":
+        return self.cfile.dictionary
+
+    @property
+    def podictionary(self) -> "CFunPODictionary":
+        return self.cfun.podictionary
+
+    @property
+    def fdecls(self) -> "CFileDeclarations":
+        return self.cfile.declarations
+
+    @property
+    def callargs(self) -> List[OutputParameterCalleeCallsiteArg]:
+        if self._callargs is None:
+            self._callargs = []
+            xcallargs = self.xnode.find("callee-callsite-args")
+            if xcallargs is not None:
+                for xcallarg in xcallargs.findall("callarg"):
+                    callarg = OutputParameterCalleeCallsiteArg(self, xcallarg)
+                    self._callargs.append(callarg)
+        return self._callargs
+
+    @property
+    def status(self) -> "OutputParameterStatus":
+        return self.podictionary.read_xml_output_parameter_status(self.xnode)
+
+    @property
+    def location(self) -> "CLocation":
+        return self.fdecls.read_xml_location(self.xnode)
+
+    @property
+    def callee(self) -> "CExp":
+        return self.cdictionary.read_xml_exp(self.xnode)
+
+    def __str__(self) -> str:
+        lines: List[str] = []
+        lines.append(
+            str(self.location.line)
+            + ": "
+            + "; callee: "
+            + str(self.callee))
+        for callarg in self.callargs:
+            lines.append("    " + str(callarg))
+        return "\n".join(lines)
diff --git a/chc/proof/OutputParameterRejectionReason.py b/chc/proof/OutputParameterRejectionReason.py
new file mode 100644
index 0000000..637ab43
--- /dev/null
+++ b/chc/proof/OutputParameterRejectionReason.py
@@ -0,0 +1,172 @@
+# ------------------------------------------------------------------------------
+# 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 List, TYPE_CHECKING
+
+from chc.proof.CFunPODictionaryRecord import CFunPODictionaryRecord, podregistry
+
+
+from chc.util.IndexedTable import IndexedTableValue
+
+
+if TYPE_CHECKING:
+    from chc.app.CCompInfo import CCompInfo
+    from chc.app.CDictionary import CDictionary
+    from chc.app.CTyp import CTyp
+    from chc.proof.CFunPODictionary import CFunPODictionary
+
+
+class OutputParameterRejectionReason(CFunPODictionaryRecord):
+
+    def __init__(
+            self, pod: "CFunPODictionary", ixval: IndexedTableValue
+    ) -> None:
+        CFunPODictionaryRecord.__init__(self, pod, ixval)
+
+
+@podregistry.register_tag("a", OutputParameterRejectionReason)
+class OutputParameterRejectionReasonArrayStruct(OutputParameterRejectionReason):
+
+    def __init__(
+            self, pod: "CFunPODictionary", ixval: IndexedTableValue
+    ) -> None:
+        OutputParameterRejectionReason.__init__(self, pod, ixval)
+
+    @property
+    def compinfo(self) -> "CCompInfo":
+        return self.cdecls.get_compinfo(self.args[0])
+
+    def __str__(self) -> str:
+        return "Struct with embedded array: " + str(self.compinfo)
+
+
+@podregistry.register_tag("at", OutputParameterRejectionReason)
+class OutputParameterRejectionReasonArrayType(OutputParameterRejectionReason):
+
+    def __init__(
+            self, pod: "CFunPODictionary", ixval: IndexedTableValue
+    ) -> None:
+        OutputParameterRejectionReason.__init__(self, pod, ixval)
+
+    @property
+    def typ(self) -> "CTyp":
+        return self.cdictionary.get_typ(self.args[0])
+
+    def __str__(self) -> str:
+        return "array type: " + str(self.typ)
+
+
+@podregistry.register_tag("c", OutputParameterRejectionReason)
+class OutputParameterRejectionReasonConstQualifier(OutputParameterRejectionReason):
+
+    def __init__(
+            self, pod: "CFunPODictionary", ixval: IndexedTableValue
+    ) -> None:
+        OutputParameterRejectionReason.__init__(self, pod, ixval)
+
+    @property
+    def typ(self) -> "CTyp":
+        return self.cdictionary.get_typ(self.args[0])
+
+    def __str__(self) -> str:
+        return "Const qualifier: " + str(self.typ)
+
+
+@podregistry.register_tag("o", OutputParameterRejectionReason)
+class OutputParameterRejectionReasonOtherReason(OutputParameterRejectionReason):
+
+    def __init__(
+            self, pod: "CFunPODictionary", ixval: IndexedTableValue
+    ) -> None:
+        OutputParameterRejectionReason.__init__(self, pod, ixval)
+
+    @property
+    def reason(self) -> str:
+        return self.cdictionary.get_string(self.args[0])
+
+    def __str__(self) -> str:
+        return "Other: " + str(self.reason)
+
+
+@podregistry.register_tag("p", OutputParameterRejectionReason)
+class OutputParameterRejectionReasonPointerPointer(OutputParameterRejectionReason):
+
+    def __init__(
+            self, pod: "CFunPODictionary", ixval: IndexedTableValue
+    ) -> None:
+        OutputParameterRejectionReason.__init__(self, pod, ixval)
+
+    @property
+    def typ(self) -> "CTyp":
+        return self.cdictionary.get_typ(self.args[0])
+
+    def __str__(self) -> str:
+        return "Pointer to pointer: " + str(self.typ)
+
+
+@podregistry.register_tag("r", OutputParameterRejectionReason)
+class OutputParameterRejectionReasonParameterRead(OutputParameterRejectionReason):
+
+    def __init__(
+            self, pod: "CFunPODictionary", ixval: IndexedTableValue
+    ) -> None:
+        OutputParameterRejectionReason.__init__(self, pod, ixval)
+
+    @property
+    def linenumber(self) -> int:
+        return self.args[0]
+
+    def __str__(self) -> str:
+        return "Parameter is read at line " + str(self.linenumber)
+
+
+@podregistry.register_tag("s", OutputParameterRejectionReason)
+class OutputParameterRejectionReasonSystemStruct(OutputParameterRejectionReason):
+
+    def __init__(
+            self, pod: "CFunPODictionary", ixval: IndexedTableValue
+    ) -> None:
+        OutputParameterRejectionReason.__init__(self, pod, ixval)
+
+    @property
+    def compinfo(self) -> "CCompInfo":
+        return self.cdecls.get_compinfo(self.args[0])
+
+    def __str__(self) -> str:
+        return "Target type is a system struct: " + str(self.compinfo)
+
+
+@podregistry.register_tag("v", OutputParameterRejectionReason)
+class OutputParameterRejectionReasonVoidPointer(OutputParameterRejectionReason):
+
+    def __init__(
+            self, pod: "CFunPODictionary", ixval: IndexedTableValue
+    ) -> None:
+        OutputParameterRejectionReason.__init__(self, pod, ixval)
+
+    def __str__(self) -> str:
+        return "Void pointer"
diff --git a/chc/proof/OutputParameterStatus.py b/chc/proof/OutputParameterStatus.py
new file mode 100644
index 0000000..3d840e4
--- /dev/null
+++ b/chc/proof/OutputParameterStatus.py
@@ -0,0 +1,151 @@
+# ------------------------------------------------------------------------------
+# 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 List, TYPE_CHECKING
+
+from chc.proof.CFunPODictionaryRecord import CFunPODictionaryRecord, podregistry
+
+
+from chc.util.IndexedTable import IndexedTableValue
+
+
+if TYPE_CHECKING:
+    from chc.app.CDictionary import CDictionary
+    from chc.proof.CFunPODictionary import CFunPODictionary
+    from chc.proof.OutputParameterRejectionReason import OutputParameterRejectionReason
+
+
+class OutputParameterStatus(CFunPODictionaryRecord):
+
+    def __init__(
+            self, pod: "CFunPODictionary", ixval: IndexedTableValue
+    ) -> None:
+        CFunPODictionaryRecord.__init__(self, pod, ixval)
+
+    @property
+    def is_unknown(self) -> bool:
+        return False
+
+    @property
+    def is_rejected(self) -> bool:
+        return False
+
+    @property
+    def is_written(self) -> bool:
+        return False
+
+    @property
+    def is_unaltered(self) -> bool:
+        return False
+
+    @property
+    def is_viable(self) -> bool:
+        return False
+
+
+@podregistry.register_tag("u", OutputParameterStatus)
+class OutputParameterStatusUnknown(OutputParameterStatus):
+
+    def __init__(
+            self, pod: "CFunPODictionary", ixval: IndexedTableValue
+    ) -> None:
+        OutputParameterStatus.__init__(self, pod, ixval)
+
+    @property
+    def is_unknown(self) -> bool:
+        return True
+
+    def __str__(self) -> str:
+        return "Unknown"
+
+
+@podregistry.register_tag("v", OutputParameterStatus)
+class OutputParameterStatusViable(OutputParameterStatus):
+
+    def __init__(
+            self, pod: "CFunPODictionary", ixval: IndexedTableValue
+    ) -> None:
+        OutputParameterStatus.__init__(self, pod, ixval)
+
+    @property
+    def is_viable(self) -> bool:
+        return True
+
+    def __str__(self) -> str:
+        return "Viable"
+
+
+@podregistry.register_tag("r", OutputParameterStatus)
+class OutputParameterStatusRejected(OutputParameterStatus):
+
+    def __init__(
+            self, pod: "CFunPODictionary", ixval: IndexedTableValue
+    ) -> None:
+        OutputParameterStatus.__init__(self, pod, ixval)
+
+    @property
+    def is_rejected(self) -> bool:
+        return True
+
+    @property
+    def reasons(self) -> List["OutputParameterRejectionReason"]:
+        return [self.pod.get_output_parameter_rejection_reason(arg) for arg in self.args]
+
+    def __str__(self) -> str:
+        return "Rejected: " + "; ".join(str(reason) for reason in self.reasons)
+
+
+@podregistry.register_tag("w", OutputParameterStatus)
+class OutputParameterStatusWritten(OutputParameterStatus):
+
+    def __init__(
+            self, pod: "CFunPODictionary", ixval: IndexedTableValue
+    ) -> None:
+        OutputParameterStatus.__init__(self, pod, ixval)
+
+    @property
+    def is_written(self) -> bool:
+        return True
+
+    def __str__(self) -> str:
+        return "Written"
+
+
+@podregistry.register_tag("a", OutputParameterStatus)
+class OutputParameterStatusUnaltered(OutputParameterStatus):
+
+    def __init__(
+            self, pod: "CFunPODictionary", ixval: IndexedTableValue
+    ) -> None:
+        OutputParameterStatus.__init__(self, pod, ixval)
+
+    @property
+    def is_unaltered(self) -> bool:
+        return True
+
+    def __str__(self) -> str:
+        return "Unaltered"
diff --git a/chc/reporting/ProofObligations.py b/chc/reporting/ProofObligations.py
index 26e1233..759ea8e 100644
--- a/chc/reporting/ProofObligations.py
+++ b/chc/reporting/ProofObligations.py
@@ -32,6 +32,8 @@
 from typing import (
     Any, Callable, cast, Dict, List, Sequence, Set, Tuple, TYPE_CHECKING)
 
+import chc.util.fileutil as UF
+
 if TYPE_CHECKING:
     from chc.app.CApplication import CApplication
     from chc.app.CFile import CFile
@@ -300,14 +302,19 @@ def pos_no_code_to_string(
                 prefix = po.get_display_prefix()
                 lines.append(prefix + " " + str(po))
                 lines.append((" " * indent) + str(expl))
+                deps = po.dependencies.invs
+                lines.append(
+                    ("\n" + " " * indent).join(
+                        str(self.cfunction.invdictionary.get_invariant_fact(i)
+                            for i in deps)))
             else:
                 lines.append("\n<?> " + str(po))
                 if po.has_diagnostic():
                     amsgs = po.diagnostic.argument_msgs
                     if len(amsgs) > 0:
                         for arg in sorted(amsgs):
-                            for s in sorted(amsgs[arg]):
-                                lines.append((" " * indent) + s)
+                            for amsg in amsgs[arg]:
+                                lines.append((" " * indent) + str(amsg))
                     kmsgs = po.diagnostic.keyword_msgs
                     if len(kmsgs) > 0:
                         for key in sorted(kmsgs):
@@ -316,7 +323,7 @@ def pos_no_code_to_string(
                     msgs = po.diagnostic.msgs
                     if len(msgs) > 0:
                         for m in msgs:
-                            lines.append((" " * indent) + m)
+                            lines.append((" " * indent) + str(m))
                     keys = po.diagnostic.argument_indices
                     for k in sorted(keys):
                         invids = po.diagnostic.get_invariant_ids(k)
@@ -382,6 +389,11 @@ def pos_on_code_tostring(
                 prefix = po.get_display_prefix()
                 lines.append(prefix + " " + str(po))
                 lines.append((" " * indent) + str(expl))
+                deps = po.dependencies.invs
+                lines.append(
+                    ("\n" + " " * indent).join(str(
+                        self.cfunction.invdictionary.get_invariant_fact(i))
+                                               for i in deps))
             else:
                 contexts.add(po.context)
                 lines.append("\n<?> " + str(po))
@@ -389,8 +401,8 @@ def pos_on_code_tostring(
                     amsgs = po.diagnostic.argument_msgs
                     if len(amsgs) > 0:
                         for arg in sorted(amsgs):
-                            for s in sorted(amsgs[arg]):
-                                lines.append((" " * indent) + s)
+                            for amsg in amsgs[arg]:
+                                lines.append((" " * indent) + str(amsg))
                     kmsgs = po.diagnostic.keyword_msgs
                     if len(kmsgs) > 0:
                         for key in sorted(kmsgs):
@@ -399,7 +411,7 @@ def pos_on_code_tostring(
                     msgs = po.diagnostic.msgs
                     if len(msgs) > 0:
                         for m in msgs:
-                            lines.append((" " * indent) + m)
+                            lines.append((" " * indent) + str(m))
                     keys = po.diagnostic.argument_indices
                     for k in sorted(keys):
                         invids = po.diagnostic.get_invariant_ids(k)
@@ -651,16 +663,20 @@ def project_proofobligation_stats_dict_to_string(
     pporesults = stats_dict["fileresults"]["ppos"]
     sporesults = stats_dict["fileresults"]["spos"]
 
-    rhlen = max([len(x) for x in pporesults])
-    lines.append(
-        proofobligation_stats_tostring(
-            pporesults, sporesults, rhlen=rhlen, header1="c files"))
+    if len(pporesults) > 0:
+        rhlen = max([len(x) for x in pporesults])
+        lines.append(
+            proofobligation_stats_tostring(
+                pporesults, sporesults, rhlen=rhlen, header1="c files"))
 
-    lines.append("\n\nProof Obligation Statistics")
+        lines.append("\n\nProof Obligation Statistics")
 
-    tagpporesults = stats_dict["tagresults"]["ppos"]
-    tagsporesults = stats_dict["tagresults"]["spos"]
-    lines.append(proofobligation_stats_tostring(tagpporesults, tagsporesults))
+        tagpporesults = stats_dict["tagresults"]["ppos"]
+        tagsporesults = stats_dict["tagresults"]["spos"]
+        lines.append(proofobligation_stats_tostring(tagpporesults, tagsporesults))
+
+    else:
+        lines.append("Zero primary proof obligations")
 
     return "\n".join(lines)
 
@@ -792,7 +808,6 @@ def tag_file_function_pos_tostring(
             for ff in sorted(fundict[f]):
                 lines.append("    Function: " + ff)
                 for po in sorted(fundict[f][ff], key=lambda po: po.line):
-                    invd = po.cfun.invdictionary
                     lines.append((" " * 6) + str(po))
                     if po.is_closed:
                         lines.append((" " * 14) + str(po.explanation))
@@ -801,27 +816,31 @@ def tag_file_function_pos_tostring(
                         amsgs = po.diagnostic.argument_msgs
                         if len(amsgs) > 0:
                             for arg in sorted(amsgs):
-                                for s in sorted(amsgs[arg]):
-                                    lines.append((" " * 14) + s)
+                                for amsg in amsgs[arg]:
+                                    lines.append((" " * 14) + str(amsg))
                         msgs = po.diagnostic.msgs
                         if len(msgs) > 0:
-                            lines.append((" " * 8) + " ---> " + msgs[0])
-                            for s in msgs[1:]:
-                                lines.append((" " * 14) + s)
+                            lines.append((" " * 8) + " ---> " + str(msgs[0]))
+                            for msg in msgs[1:]:
+                                lines.append((" " * 14) + str(msg))
                             lines.append(" ")
                         keys = po.diagnostic.argument_indices
-                        for k in keys:
-                            invids = po.diagnostic.get_invariant_ids(k)
-                            for id in invids:
-                                inv = invd.get_invariant_fact(id)
-                                if inv.is_nrv_fact:
-                                    inv = cast("CInvariantNRVFact", inv)
-                                    nrv = inv.non_relational_value
-                                    lines.append(
-                                        (" " * 14)
-                                        + str(k)
-                                        + ": "
-                                        + str(nrv))
+                        try:
+                            invd = po.cfun.invdictionary
+                            for k in keys:
+                                invids = po.diagnostic.get_invariant_ids(k)
+                                for id in invids:
+                                    inv = invd.get_invariant_fact(id)
+                                    if inv.is_nrv_fact:
+                                        inv = cast("CInvariantNRVFact", inv)
+                                        nrv = inv.non_relational_value
+                                        lines.append(
+                                            (" " * 14)
+                                            + str(k)
+                                            + ": "
+                                            + str(nrv))
+                        except UF.CHCError:
+                            pass
 
                         lines.append(" ")
 
diff --git a/chc/util/fileutil.py b/chc/util/fileutil.py
index 4815200..48c3d43 100644
--- a/chc/util/fileutil.py
+++ b/chc/util/fileutil.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
@@ -1295,6 +1295,17 @@ def get_ppo_filename(
     return os.path.join(fnpath, filename)
 
 
+def has_ppo_file(
+        targetpath: str,
+        projectname: str,
+        cfilepath: Optional[str],
+        cfilename: str,
+        fnname: str) -> bool:
+    filename = get_ppo_filename(
+        targetpath, projectname, cfilepath, cfilename, fnname)
+    return os.path.isfile(filename)
+
+
 def get_ppo_xnode(
         targetpath: str,
         projectname: str,
@@ -1330,6 +1341,30 @@ def get_spo_xnode(
         filename, "function", "Secondary proof obligations file", show=False)
 
 
+def get_adg_filename(
+        targetpath: str,
+        projectname: str,
+        cfilepath: Optional[str],
+        cfilename: str,
+        fnname: str) -> str:
+    fnpath = get_cfile_fnpath(
+        targetpath, projectname, cfilepath, cfilename, fnname)
+    filename = get_fn_composite(cfilename, fnname, "adg")
+    return os.path.join(fnpath, filename)
+
+
+def get_adg_xnode(
+        targetpath: str,
+        projectname: str,
+        cfilepath: Optional[str],
+        cfilename: str,
+        fnname: str) -> Optional[ET.Element]:
+    filename = get_adg_filename(
+        targetpath, projectname, cfilepath, cfilename, fnname)
+    return get_xnode(
+        filename, "function", "Analysis digests file", show=False)
+
+
 def save_spo_file(
         targetpath: str,
         projectname: str,
@@ -1971,6 +2006,13 @@ def xget_int_attr(p: ET.Element, tag: str, msg: str) -> int:
     return int(xdata)
 
 
+def xget_int_attr_o(node: ET.Element, tag: str) -> Optional[int]:
+    xattrval = node.get(tag)
+    if xattrval is not None:
+        return int(xattrval)
+    return None
+
+
 if __name__ == "__main__":
 
     config = Config()