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.