Readable printing of inferred loop assigns contract

[rod-chapman]

CBMC version: 6.4.0
Operating system: macOS

CBMC 6.4.0's "Loop assign contract inference" feature is very useful. When it finds a loop without an explicit CPROVER_assigns contract, it infers one. An information message reports this to the user. For example:

No assigns clause provided for loop PQCP_MLKEM_NATIVE_MLKEM1024_poly_tomont_wrapped_for_contract_checking.0 at file /Users/rodchap/Desktop/rod/projects/crypto/pqcp/pqcp/mlkem/poly.c line 416 function PQCP_MLKEM_NATIVE_MLKEM1024_poly_tomont. The inferred set {side_effect statement="function_call"(__CPROVER_object_whole, arguments(address_of(*PQCP_MLKEM_NATIVE_MLKEM1024_poly_tomont::r.coeffs[cast(PQCP_MLKEM_NATIVE_MLKEM1024_poly_tomont::1::i, signedbv[64])]))), PQCP_MLKEM_NATIVE_MLKEM1024_poly_tomont::1::i} might be incomplete or imprecise, please provide an assigns clause if the analysis fails.

This is basically unreadable for a beginner. Could you construct a pretty-printer that prints the inferred contract in the correct syntax that could be cut-and-pasted directly into the source? For example, I'd like to see the example above reported as:

No assigns clause provided for loop PQCP_MLKEM_NATIVE_MLKEM1024_poly_tomont_wrapped_for_contract_checking.0 at file /Users/rodchap/Desktop/rod/projects/crypto/pqcp/pqcp/mlkem/poly.c line 416 function PQCP_MLKEM_NATIVE_MLKEM1024_poly_tomont.

The inferred set

__CPROVER_assigns(i, __CPROVER_object_whole(r->coeffs))

might be incomplete or imprecise, please provide an assigns clause if the analysis fails.