`goto-instrument --dump-c` still produces invalid code when parameter name overlaps with local variable name

[vecchiot-aws]

CBMC version: 5.35.0 (cbmc-5.35.0-95-ge6f69702f)
Operating system: macOS Big Sur v11.4

Exact command line resulting in the issue:
Though the example in #6242 was fixed, there are still other examples which don't work. I've created a simpler example attached here:

• Input: test.json
• Command: symtab2gb test.json --out test.goto; goto-instrument --dump-c test.goto > test.c
• Output: test.c

What behaviour did you expect: A valid C program is produced.

What happened instead: The parameter and local variables have the same name, leading to a compilation error:

int main(int x)
{
  unsigned int x;
}

If it helps, this was created from the following Rust file using RMC, with manual edits to simplify:

fn help(x: i32) {
    let x: i64;
}

fn main() {
    help(1);
}

[TGWDB]

Thanks for the update, comments and observations below.

The json file does not have the "expected" information that cbmc (or here goto-instrument) expects for variable names. Typically they would be expected to contain information about their scoping in the form of function::name (or with more details), but the ones in the example here are missing this. This breaks the checking for parameter collisions and hence the example.

I've created an example (attached) where the variables are renamed in the json with the above scope information and this fixes the goto-instrument pass. rename.json.txt

Not related, but you can use goto-instrument --dump-c test.goto test.c (without the redirect) to have the C code written to the .c file without the other output

[vecchiot-aws]

Thanks for your help! Unfortunately, this doesn't quite fix it. If we actually try to use the function parameter within the body of the function, it ends up using a different name than the one used to declare it:

// main
// 
int main(int x)
{
  unsigned int 2_x;
  return 1_x; // <--  This is when we try to return the parameter.
}

Here is a version that demonstrates this issue (all I did was add a return statement to the body, and change the names to have _1_x instead of 1_x):
test.json

Command: symtab2gb test.json -out test.goto; goto-instrument --dump-c test.goto test.c
Result:

// main
// 
int main(int x)
{
  unsigned int _2_x;
  return _1_x;
}