Klever

Is there a branch with test fixes?

No, the fixes were in CPAchecker itself.

Before all sync:race tests passed while function pointers weren't enabled like now, so, I guess that FunctionPointerTest was wrong.

By default function pointers are enabled. My statement about them was only like a note, because I often disable them manually for debugging, and then I will be surprised, why the test does not pass.
Anyway, your question helps to found a bug in CPAchecker. I found, that the error trace, which was shown, should be found even when the function pointers are disabled. Finally, the bug is fixed and the test pass always.
Return to your question: seems yes, the test is now incorrect.
I am going to fix it, or even better to add one more, because this test is also useful. Is it the same issue?

What is the branch in the CPAchecker repository?

CPALockator-combat-mode

Pavel Andrianov wrote:

Before all sync:race tests passed while function pointers weren't enabled like now, so, I guess that FunctionPointerTest was wrong.

By default function pointers are enabled. My statement about them was only like a note, because I often disable them manually for debugging, and then I will be surprised, why the test does not pass.
Anyway, your question helps to found a bug in CPAchecker. I found, that the error trace, which was shown, should be found even when the function pointers are disabled. Finally, the bug is fixed and the test pass always.
Return to your question: seems yes, the test is now incorrect.
I am going to fix it, or even better to add one more, because this test is also useful. Is it the same issue?

Test fixes and improvements are always welcome! It is great when tests are changed together with stuffs for which they are intended.

This is not a bug, vice versa, the change fixes an existed bug. The identifier is based on variable definition: int var -> int_var. However, int the first option there may be a such situation: struct one_struct_nested var1 -> struct_one_struct_nested_var1 and struct one_struct nested_var1 -> struct_one_struct_nested_var1. So, two different variables are mapped to the same identifier. This bug was fixed by changing the identifier construction (adding one more underscore between type and name of variable).

Pavel Andrianov wrote:

This is not a bug, vice versa, the change fixes an existed bug. The identifier is based on variable definition: int var -> int_var. However, int the first option there may be a such situation: struct one_struct_nested var1 -> struct_one_struct_nested_var1 and struct one_struct nested_var1 -> struct_one_struct_nested_var1. So, two different variables are mapped to the same identifier. This bug was fixed by changing the identifier construction (adding one more underscore between type and name of variable).

Okay. But "struct a__b c" and "struct a b__c" will be mapped to the same name again. Indeed you don't need to map space to any identifier symbol. Are you going to fix that one more time? Perhaps you will also need to fix something within Core.

Update CPALockator to 28911 (in branch new_tests_for_races). Attributes, including identifier name are printed into witness.

As a proper decision of issues with witness attributes we at last switch to translation of witness attributes to error trace ones. So, there are not attributes encoded within witness file names anymore and everybody is welcome to specify specific attributes within witnesses!

I implemented this in branch new_tests_for_races that I renamed to new-CPALockator. Now wait from Pavel more pretty names and values for new attributes.

Tests revealed that there are numerous problems with preset marks for sync:race. I fixed them all and started another testing round.