Feature request: labels for function pointer restrictions

[avanhatt]

RMC is starting to use CBMC function pointer restrictions.

We have found CBMC's naming convention for identifying specific function pointer calls (indexed based on static placement, documented here) to be difficult to use without introducing wrapper functions. It would be helpful if we could specify call sites using C labels instead:

That is, we would like to be able to use "call_f" : [...], "call_g": [...] instead of "surrounding_fn.function_pointer_call.1" : [...], "surrounding_fn.function_pointer_call.2": [...] for this example:

void surrounding_fn(..) {
    call_f: (*f)(x);
    call_g: (*g)(y);
}

[danielsn]

This would also be useful for having meaningful and stable names for unwindsets

[danielsn]

I suspect the name would actually be surrounding_fn::call_f to ensure uniqueness

[tautschnig]

We first need to add a uniqueness check in the C front-end, which happily accepts the following at the moment:

int main()
{
  int x;
label: x=1;
  goto label;
label: x=2;
}

[jimgrundy]

I'd love to be able to refer to loops by label rather than number when specifying unwindings. Is that feasible to add?

[tautschnig]

I'd love to be able to refer to loops by label rather than number when specifying unwindings. Is that feasible to add?

#6508 (still in draft mode) now adds support for both loops and function pointers to be referred to by label.