From 86c0c74fbac82b1fa3fa1153d12b6ca557cdd2c4 Mon Sep 17 00:00:00 2001
From: Steven Valdez <dvorak42@aarno-labs.com>
Date: Tue, 11 Aug 2026 15:22:19 -0500
Subject: [PATCH] Set buffersize based on first argument if unknown from proof
 obligation.

---
 chb/cmdline/reportcmds.py | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/chb/cmdline/reportcmds.py b/chb/cmdline/reportcmds.py
index 67084908..fe11ce8a 100644
--- a/chb/cmdline/reportcmds.py
+++ b/chb/cmdline/reportcmds.py
@@ -1873,6 +1873,9 @@ def is_cmd_delegation(po: 'ProofObligation') -> bool:
                 fn_arg["type"] = "pointer"
                 fn_arg["max-length"] = buffersize
                 fn_arg["size-origin"] = sizeorigin
+                # Set the buffersize based on the first passthrough argument if unknown from PO.
+                if not found_fmt_arg and pc_content["buffersize"] == 0:
+                    pc_content["buffersize"] = buffersize
 
             # If we've already found the format string input, treat the remaining arguments
             # up to the number of format string specifiers as inputs.