Project

General

Profile

Actions
Copy link

Bug #1019

open

Our models are not correctly understood by CPAchecker

Added by Pavel Shved over 13 years ago. Updated over 11 years ago.

Status:
New
Priority:
Normal
Assignee:
Mikhail Mandrykin
Category:
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

cpa_bug.tgz (66.6 KB) cpa_bug.tgz Pavel Shved, 04/04/2011 01:16 PM

Related issues 1 (1 open — 0 closed)

Blocks Linux Driver Verification - Bug #1012: BLAST and CPAchecker do not agree on safety of certain driversNewMikhail Mandrykin03/31/2011

Actions
Actions
Copy link
 #1

Updated by Pavel Shved over 13 years ago

To reproduce this bug on a larger scale (the assignee will need it to test if the fixes do solve the problem), you may use this line:

RCV_VERIFIER=cpachecker ldv-manager tag=current envs=linux-2.6.31.6.tar.bz2 drivers=drivers/media/dvb/dvb-usb/dvb-usb-cxusb.ko kernel_driver=1 rule_models=32_1

Make sure that cpa.sh from scripts/ folder is in your PATH.

Actions
Copy link
 #2

Updated by Evgeny Novikov over 11 years ago

  • Assignee changed from Vadim Mutilin to Mikhail Mandrykin
Actions
Copy link

Also available in: Atom PDF