Pretty print __CPROVER_havoc_object in --show-goto-functions

[SaswatPadhi]

CBMC version: 5.30
Operating system: 10.15.7

Test case:

int main() {
  int a[64];
  __CPROVER_havoc_object(a);
}

Exact command line resulting in the issue:

$ goto-cc test.c -o test.gb && goto-instrument --show-goto-functions test.gb | tail
        signed int a[64l];
        // 1 file /Users/saspadhi/test.c line 3 function main
        irep("(\"code\" \"\" (\"typecast\" \"\" (\"address_of\" \"\" (\"index\" \"\" (\"symbol\" \"type\" (\"array\" \"\" (\"signedbv\" \"width\" (\"32\") \"#c_type\" (\"signed_int\")) \"#source_location\" (\"\" \"file\" (\"/Users/saspadhi/test.c\") \"line\" (\"2\") \"function\" (\"main\") \"working_directory\" (\"/Users/saspadhi/Repos/cbmc-wip\")) \"size\" (\"constant\" \"type\" (\"signedbv\" \"width\" (\"64\") \"#c_type\" (\"signed_long_int\")) \"value\" (\"40\"))) \"#source_location\" (\"\" \"file\" (\"/Users/saspadhi/test.c\") \"line\" (\"3\") \"function\" (\"main\") \"working_directory\" (\"/Users/saspadhi/Repos/cbmc-wip\")) \"identifier\" (\"main::1::a\") \"#lvalue\" (\"1\")) \"\" (\"constant\" \"type\" (\"signedbv\" \"width\" (\"64\") \"#c_type\" (\"signed_long_int\")) \"value\" (\"0\")) \"type\" (\"signedbv\" \"width\" (\"32\") \"#c_type\" (\"signed_int\"))) \"type\" (\"pointer\" \"\" (\"signedbv\" \"width\" (\"32\") \"#c_type\" (\"signed_int\")) \"width\" (\"64\"))) \"type\" (\"pointer\" \"\" (\"empty\" \"#source_location\" (\"\" \"file\" (\"<builtin-architecture-strings>\") \"line\" (\"20\") \"working_directory\" (\"/Users/saspadhi/Repos/cbmc-wip\"))) \"#source_location\" (\"\" \"file\" (\"<builtin-architecture-strings>\") \"line\" (\"20\") \"working_directory\" (\"/Users/saspadhi/Repos/cbmc-wip\")) \"width\" (\"64\"))) \"type\" (\"empty\") \"#source_location\" (\"\" \"file\" (\"/Users/saspadhi/test.c\") \"line\" (\"3\") \"function\" (\"main\") \"working_directory\" (\"/Users/saspadhi/Repos/cbmc-wip\")) \"statement\" (\"havoc_object\"))")
        // 2 file /Users/saspadhi/test.c line 4 function main
        dead a;
        // 3 file /Users/saspadhi/test.c line 4 function main
        return NONDET(signed int);
        // 4 file /Users/saspadhi/test.c line 4 function main
        END_FUNCTION

What behaviour did you expect:
Some readable expression for the __CPROVER_havoc_object call.

What happened instead:
An overly verbose debug output for the irep is printed.

Additional context:
We generate calls to __CPROVER_havoc_object when enforcing loop contracts (may be function contracts too, @feliperodri?). So the --show-goto-functions output for programs that use contracts often end up with unreadable blobs like this.