Draft: Define concurrency tasks on un-preprocessed .c sources where available
Pre-processed concurrency tasks defined using Ubuntu 18.04's pthread types are not portable. Type definitions incompatible with the system modelling the pthread library lead to wrong assumptions by solvers in the best case, and to crashes in the worst case.
The pthread API defined by POSIX does not specify the concrete underlying definitions for the types pthread_t, pthread_mutex_t, and so on, which it declares. Therefore it is unreasonable to expect solvers to adhere to one specific and old implementation (glibc-2.27 for Ubuntu 18.04) of the pthread API, which is precisely why <pthread.h> exists: enable implementations of the same functions with different underlying system-specific types but the same semantics.
Script used for this modification:
for f in `sed 's/#.*//' ConcurrencySafety-Main.set`; do
p=$(sed -rn "s,input_files: '(.*)\.i',`dirname $f`/\1.c,p" $f)
if [ "x$p" != x -a -f "$p" ]; then
sed -ri "s,(input_files: '.*)\.i',\1.c'," $f
fi
done
The only concurrency-safety task not modified is c/ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i
as the corresponding .c
source is unavailable.
I am aware that discussions about .c vs. .i are ongoing. However, the issue solved by this MR is known to affect ESBMC's model of pthreads.