File tree Expand file tree Collapse file tree 1 file changed +2
-2
lines changed
regression/cbmc/restrict-function-pointer-by-name Expand file tree Collapse file tree 1 file changed +2
-2
lines changed Original file line number Diff line number Diff line change 3
3
--restrict-function-pointer-by-name main::1::fptr/f --restrict-function-pointer-by-name use_f::fptr/g --restrict-function-pointer-by-name g_fptr/f,h
4
4
\[use_f.assertion.2\] line \d+ assertion fptr\(\) == 2: SUCCESS
5
5
\[use_f.assertion.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be g: SUCCESS
6
- \[main.assertion.1\] line \d+ dereferenced function pointer at main.function_pointer_call.1 must be one of \[h, f \]: SUCCESS
7
- \[main.assertion.2\] line \d+ assertion res == 1 | | res == 3: SUCCESS
6
+ \[main.assertion.1\] line \d+ dereferenced function pointer at main.function_pointer_call.1 must be one of \[(h|f), (h|f) \]: SUCCESS
7
+ \[main.assertion.2\] line \d+ assertion res == 1 \|\ | res == 3: SUCCESS
8
8
\[main.assertion.3\] line \d+ dereferenced function pointer at main.function_pointer_call.2 must be f: SUCCESS
9
9
\[main.assertion.4\] line \d+ assertion fptr\(\) == 1: SUCCESS
10
10
^EXIT=0$
You can’t perform that action at this time.
0 commit comments