Allow Same Local Variable Names at Different Scopes
If a C program contains multiple local variable declarations of the same name at different scopes, the frontend will prompt a name collision error, because currently RefinedC hoists all local variables to the top-level scope, and require their names to be unique. However, using local variable of the same name at different scopes is acceptable by the C compiler. Here is an example: https://github.com/bolt-perf-contracts/bolt/blob/master/nf/router/router_options.c.
In this file, timestamp_flag
is both declared inside and outside the if-statement:
if (timestamp_pointer > opt_length) {
...
uint8_t timestamp_flag = ...;
...
}
...
uint8_t timestamp_flag = ...;
...
To make the frontend accept more C programs in practice, we should allow them. One possible solution could be: the frontend internally rename those local variables to <original name>'<counter>
. For example: timestamp_flag'1
and timestamp_flag'2
. Note that '
is a valid identifier char for Coq, but not for C. So these renamed variables will never conflict with any other C variables. For better readability, one may also use line number (if the developer kindly does not write two statements at the same line; or just use line and column number together) in place of counter.