Label-based function pointer restrictions fail for JSON file

[avanhatt]

I'm attempting to use the new label-based function pointer restrictions added here (CC @tautschnig): #6508

That PR adds a test case for the command line based restrictions. I am trying to run the same case (regression/goto-instrument/restrict-function-pointer-by-label/test.c) with --function-pointer-restrictions-file and a JSON file instead of --restrict-function-pointer.

Here is the file:

{
    "use_f.labelled_call":[
       "f"
    ]
}

This fails with:

goto-instrument --function-pointer-restrictions-file restriction.json a.out b.out
Reading GOTO program from 'a.out'
Invalid restriction
Reason: use_f.labelled_call not found in the symbol table

The same restriction passed on the command line works as expected:

goto-instrument --restrict-function-pointer use_f.labelled_call/f a.out b.out
Reading GOTO program from 'a.out'
file test.c line 9 function use_f: replacing function pointer by 1 possible targets
Writing GOTO program to 'b.out'

CBMC version: 5.49.0 (cbmc-5.49.0)
Operating system: macOS 11.5.2
Exact command line resulting in the issue:

goto-instrument --function-pointer-restrictions-file restriction.json a.out b.out

What behaviour did you expect:

The same behavior with JSON as the command line, for f to be passed as a restriction.

What happened instead:

Failure to find symbol.

[tautschnig]

Thank you for the helpful report, and my apologies for failing to address JSON support in the earlier commit in the first place. This will now be fixed once #6610 is merged.