-
Notifications
You must be signed in to change notification settings - Fork 84
Description
SV-COMP prerun reveals that we now get lots of crashes in ConcurrencySafety:
Fatal error: exception SetDomain.Unsupported("elements on `Top")
This happens when thread IDs sets are used inside partitioned arrays, for example:
./regtest.sh 28 02 --set ana.activated[+] thread --enable exp.partition-arrays.enabledIt happens because the array is initialized to contain unknown integer abstractions, but setting it to a singlethread thread ID set causes a join inside partitioned arrays, which results in a top ValueDomain variant, not a thread ID set.
There is a workaround for thread ID sets overwriting integers for initializing globals and it also gets invoked recursively for updating the array element, but partitioned arrays do some joining nevertheless.
A possible hack to work around this is to implement join of Int and Thread in ValueDomain to yield a Thread (and ignore the Int). Previously we wanted to avoid this since those things can be problematic (#185), but it seems inevitable now, unless someone has a better idea.