Actions
Bug #1019
openOur models are not correctly understood by CPAchecker
Start date:
04/04/2011
Due date:
% Done:
0%
Estimated time:
Detected in build:
svn
Platform:
Published in build:
Description
During the checking of kernel with the latest CPAchecker it found more unsafes than BLAST (see bug #1012). I analyzed one of them, and it is totally spurious. CPAchecker could not find mutex_lock_interruptible function, while it was there in the preprocessed and cillify-ed sources.
To reproduce the problem, unpack the archive attached and run
cpa.sh cilled-source.c -config cpa.cfg -entryfunction ldv_main0_plain_sorted_withcheck
In the output you'll notice the following line
Line 7954: Assuming external function to be a pure function: mutex_lock_interruptible (CtoFormulaConverter.makeExternalFunctionCall, INFO)
And in the error trace we see the call to mutex_lock_interruptible not unrolled, leading to a false positive.
Files
Actions