add xpo-predicate for trusted-os-cmd-fmt-arg-string

Author: sipma

chb/app/CHVersion.py

@@ -1,3 +1,3 @@
-chbversion: str = "0.3.0-20260610"
+chbversion: str = "0.3.0-20260611"
 
-minimum_required_chb_version = "0.6.0_20260610"
+minimum_required_chb_version = "0.6.0_20260611"

chb/app/FnProofObligations.py

@@ -159,6 +159,7 @@ def __str__(self) -> str:
             + str(self.xpo)
             + " ("
             + str(self.status)
+            + m
             + ")")
 
 
@@ -192,7 +193,7 @@ def proofobligations(self) -> Dict[str, List[ProofObligation]]:
                         xstatus = xxpo.find("status")
                         if xstatus is not None:
                             status = POStatus(self.xpod, xstatus)
-                            msg = xxpo.get("m", "none")
+                            msg = xstatus.get("m", "none")
                             po = ProofObligation(iaddr, xpo, status, msg)
                             self._store[iaddr].append(po)
         return self._store

chb/app/XPOPredicate.py

@@ -953,6 +953,37 @@ def __str__(self) -> str:
             + ")")
 
 
+@xporegistry.register_tag("tfa", XPOPredicate)
+class XPOTrustedOsCmdFmtArgString(XPOPredicate):
+    """Expression is trusted as argument for a format string-constructed command.
+
+    args[0]: index of expression in xprdictionary
+    """
+
+    def __init__(
+            self, xpod: "FnXPODictionary", ixval: IndexedTableValue) -> None:
+        XPOPredicate.__init__(self, xpod, ixval)
+
+    @property
+    def is_xpo_trusted_os_cmd_fmt_arg_string(self) -> bool:
+        return True
+
+    @property
+    def expr(self) -> "XXpr":
+        return self.xd.xpr(self.args[0])
+
+    @property
+    def optlen(self) -> Optional["XXpr"]:
+        if self.args[1] == -1:
+            return None
+        return self.xd.xpr(self.args[1])
+
+    def __str__(self) -> str:
+        return (
+            "trusted-os-cmd-fmt-arg-string("
+            + str(self.expr))
+
+
 @xporegistry.register_tag("v", XPOPredicate)
 class XPOValidMem(XPOPredicate):
     """Expression points to valid memory.