Project

General

Profile

Actions

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
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 open0 closed)

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

Actions
Actions

Also available in: Atom PDF