Preconditions

chb/api/XXPredicate.py

@@ -141,6 +141,10 @@ def is_xp_null_terminated(self) -> bool:
     def is_xp_output_formatstring(self) -> bool:
         return False
 
+    @property
+    def is_xp_restricted_output_formatstring(self) -> bool:
+        return False
+
     @property
     def is_xp_positive(self) -> bool:
         return False
@@ -777,6 +781,42 @@ def __str__(self) -> str:
         return "output-formatstring(" + str(self.pointer) + ")"
 
 
+@apiregistry.register_tag("rofs", XXPredicate)
+class XXPRestrictedOutFormatString(XXPredicate):
+    """Term points to a restricted format string for output (printf)
+
+    A restricted output format string is a format string with a specific sequence of
+    format specifiers.
+
+    args[0]: index of pointer in interfacedictionary
+    """
+
+    def __init__(
+            self, ixd: "InterfaceDictionary", ixval: IndexedTableValue) -> None:
+        XXPredicate.__init__(self, ixd, ixval)
+
+    @property
+    def is_xp_restricted_output_formatstring(self) -> bool:
+        return True
+
+    @property
+    def pointer(self) -> "BTerm":
+        return self.id.bterm(self.args[0])
+
+    @property
+    def specifiers(self) -> List[str]:
+        return [self.bd.string(i) for i in self.args[1:]]
+
+    def __str__(self) -> str:
+        return (
+            "restricted-output-formatstring("
+            + str(self.pointer)
+            + ", "
+            + ", ".join(self.specifiers)
+            + ")"
+        )
+
+
 @apiregistry.register_tag("pos", XXPredicate)
 class XXPPositive(XXPredicate):
     """Term is positive.
@@ -1008,7 +1048,7 @@ def optlen(self) -> Optional["BTerm"]:
 
     def __str__(self) -> str:
         return (
-            "trusted-os-cmd-fmt-string("
+            "trusted-os-cmd-fmt-arg-string("
             + str(self.fmt)
             + ", "
             + self.quotes

chb/app/CHVersion.py

@@ -1,3 +1,3 @@
-chbversion: str = "0.3.0-20260619"
+chbversion: str = "0.3.0-20260625"
 
 minimum_required_chb_version = "0.6.0_20260617"

chb/app/XPOPredicate.py

@@ -1004,6 +1004,10 @@ def is_xpo_trusted_os_cmd_fmt_arg_string(self) -> bool:
     def expr(self) -> "XXpr":
         return self.xd.xpr(self.args[0])
 
+    @property
+    def quotes(self) -> str:
+        return self.tags[1]
+
     @property
     def optlen(self) -> Optional["XXpr"]:
         if self.args[1] == -1:
@@ -1013,7 +1017,12 @@ def optlen(self) -> Optional["XXpr"]:
     def __str__(self) -> str:
         return (
             "trusted-os-cmd-fmt-arg-string("
-            + str(self.expr))
+            + str(self.expr)
+            + ", "
+            + str(self.quotes)
+            + ", "
+            + str(self.optlen)
+            + ")")
 
 
 @xporegistry.register_tag("v", XPOPredicate)

chb/invariants/VConstantValueVariable.py

@@ -6,7 +6,7 @@
 #
 # Copyright (c) 2016-2020 Kestrel Technology LLC
 # Copyright (c) 2020      Henny Sipma
-# Copyright (c) 2021-2025 Aarno Labs LLC
+# Copyright (c) 2021-2026 Aarno Labs LLC
 #
 # Permission is hereby granted, free of charge, to any person obtaining a copy
 # of this software and associated documentation files (the "Software"), to deal
@@ -139,6 +139,10 @@ def is_function_return_value(self) -> bool:
     def is_typecast_value(self) -> bool:
         return False
 
+    @property
+    def is_frozen_value(self) -> bool:
+        return False
+
     @property
     def is_symbolic_value(self) -> bool:
         return False
@@ -479,6 +483,37 @@ def __str__(self) -> str:
                 + '_@_' + str(self.jump_addr))
 
 
+@varregistry.register_tag("frv", VConstantValueVariable)
+class VFrozenValue(VConstantValueVariable):
+    """Value of a test at an earlier instruction.
+
+    tags[1]: address of test instruction
+    tags[2]: address of conditional jump instruction
+    args[0]: index of variable in xprdictionary
+    """
+
+    def __init__(
+            self,
+            vd: "FnVarDictionary",
+            ixval: IndexedTableValue) -> None:
+        VConstantValueVariable.__init__(self, vd, ixval)
+
+    @property
+    def is_frozen_value(self) -> bool:
+        return True
+
+    @property
+    def variable(self) -> "XVariable":
+        return self.xd.variable(self.args[0])
+
+    @property
+    def iaddr(self) -> str:
+        return self.tags[1]
+
+    def __str__(self) -> str:
+        return (str(self.variable) + '_@val_' + str(self.iaddr))
+
+
 @varregistry.register_tag("bv", VConstantValueVariable)
 class VBridgeVariable(VConstantValueVariable):
     """Variable that represents a call argument.

chb/invariants/XVariable.py

@@ -134,6 +134,13 @@ def is_typecast_value(self) -> bool:
             and self.denotation.is_auxiliary_variable
             and self.denotation.auxvar.is_typecast_value)
 
+    @property
+    def is_frozen_value(self) -> bool:
+        return (
+            self.has_denotation()
+            and self.denotation.is_auxiliary_variable
+            and self.denotation.auxvar.is_frozen_value)
+
     @property
     def is_symbolic_expr_value(self) -> bool:
         return (

chb/invariants/XXprUtil.py

@@ -113,7 +113,7 @@
         VMemoryVariable, VAuxiliaryVariable, VRegisterVariable)
     from chb.invariants.VConstantValueVariable import (
         VInitialRegisterValue, VInitialMemoryValue, VFunctionReturnValue,
-        VTypeCastValue, SideEffectValue, SymbolicValue)
+        VFrozenValue, VTypeCastValue, SideEffectValue, SymbolicValue)
     from chb.invariants.VMemoryBase import (
         VMemoryBase,
         VMemoryBaseBaseVar,
@@ -1053,6 +1053,25 @@ def xvariable_to_ast_def_lval_expression(
                 str(tcvar), iaddr)
         return astree.mk_temp_lval_expression()
 
+    if xvar.is_frozen_value:
+        frvar = cast("VFrozenValue", xvar.denotation.auxvar)
+        variaddr = frvar.iaddr
+        frvarreg = frvar.variable
+        if variaddr in astree.ssa_intros and str(frvarreg) in astree.ssa_intros[variaddr]:
+            vinfo = astree.ssa_intros[variaddr][str(frvarreg)]
+            ssavalue = astree.get_ssa_value(vinfo.vname)
+            if ssavalue is not None:
+                return ssavalue
+            else:
+                return astree.mk_vinfo_lval_expression(
+                    vinfo, anonymous=anonymous)
+        if not anonymous:
+            chklogger.logger.error(
+                "AST def conversion of frozen value %s to lval at address %s "
+                + "not yet supported",
+                str(frvar), iaddr)
+        return astree.mk_temp_lval_expression()
+
     if xvar.is_sideeffect_value:
         sevar = cast("SideEffectValue", xvar.denotation.auxvar)
         argloc = sevar.argument_location

chb/userdata/UserHints.py

@@ -486,6 +486,10 @@ def typename(self) -> Optional[str]:
     def ispointerto(self) -> bool:
         return "ptrto" in self.mods
 
+    @property
+    def isfreeze(self) -> bool:
+        return "freeze" in self.mods
+
     @property
     def mods(self) -> List[str]:
         return cast(List[str], self.varintro.get("mods", []))
@@ -504,6 +508,8 @@ def to_xml(self, node: ET.Element) -> None:
             xvintro.set("ptrto", "yes")
         if self.has_cast():
             xvintro.set("cast", "yes")
+        if self.isfreeze:
+            xvintro.set("freeze", "yes")
 
     def __str__(self) -> str:
         return (