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

[vecchiot-aws]

When two local variables have the same base name, --dump-c automatically uses the unique name for all (except the first) variables in that scope to avoid name conflicts. However, this does not consider function parameter names at the moment.

CBMC version: 5.34.0 (cbmc-5.32.1-183-gc50985444)
Operating system: macOS Big Sur v11.4

Exact command line resulting in the issue: symtab2gb test.json --out test.goto; goto-instrument --dump-c test.goto > test.c
with test.json
produces test.c

What behaviour did you expect: The contents of test.c is valid C code.
What happened instead: The parameter to helper and one of the local variables have overlapping names.

Generated definition of helper:

void helper(unsigned int x) {
  int x;
  int helper$$1$$var_3$$x;
}

[martin-cs]

Good find; thank you for the bug report.

[NlightNFotis]

Hello @vecchiot-aws.

Is it possible to share with us the code that generated .json file? That will make it easier for us to dissect the problem and design a solution.

[vecchiot-aws]

This was produced by running rmc --gen-c test.rs on the following code. Note that I cleaned up the symbol table json a lot in the original post. (Link to RMC on Github.)

fn helper(x: i32) {
    let x: i32;
    let x: i32;
}

fn main() {
    helper(1);
}