Description
CBMC version: 5.30.1 (cbmc-5.30.1)
Operating system: Ubuntu 20.04.2
Exact command line resulting in the issue:
goto-instrument --function-pointer-restrictions-file restrictions (within the context of the RMC tool).
What behaviour did you expect:
CBMC to restrict function pointer branch analysis to the cases specified, as described in the documentation for function pointer descriptions here.
What happened instead:
I am running into two related problems with the --function-pointer-restrictions-file flag.
(1) Casting
The functions I would like to restrict are a different type than the call site due to a cast in the source code to a function that takes a void pointer. The source code looks roughly like this:
// function pointer creation
.field=(int (*)(void *))_Animal_noise // struct field
// function pointer use
var_5.vtable->field(var_1);
However, if I try to pass _Animal_noise as a restriction, I get this error:
Reason: type mismatch: `main.function_pointer_call.1' points to `int (void *)', but restriction `_Animal_noise' has type `int (struct _10007873221718841048 *self)'
However, if I try and include the cast in the restrictions file, it fails to parse:
Invalid restriction
Reason: symbol not found: (int (*)(void *))_Animal_noise
The pointer itself does not have a symbol name to my understanding, because it is a struct field.
(2) . in function name wrong error, see below
In a different example, some of my restricted function have .. in the name, and fail to parse:
Example:
"_ZN80_$LT$devices..virtio..mmio..MmioTransport$u20$as$u20$devices..bus..BusDevice$GT$5write17h533d97e6e2ca6db0E.function_pointer_call.1": [
"_ZN7devices6virtio6device12VirtioDevice20ack_features_by_page17hbff58082681c1a52E_wrapper",
"_ZN7devices6virtio6device12VirtioDevice20ack_features_by_page17h2c20fca1a3ee805eE_wrapper",
"_ZN7devices6virtio6device12VirtioDevice20ack_features_by_page17h1668e8cac23d16f1E_wrapper"
],
Error:
Reading GOTO program from 'parse_harness1/a.out'
file restrictions: syntax error
failed to read function pointer restrictions from restrictions
This is despite CBMC analyzing the file with these names fine without restrictions.