Project

General

Profile

Actions

Bug #1012

open

BLAST and CPAchecker do not agree on safety of certain drivers

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

Status:
New
Priority:
Normal
Category:
BLAST
Start date:
03/31/2011
Due date:
% Done:

0%

Estimated time:
Detected in build:
v0.2.1
Platform:
Published in build:

Description

After CPAchecker support was restored, I run driver verification on a stable revision v0.2.1. It turned out that CPAchecker, aside from being three times slower, found some errors in the drivers proved safe by BLAST. The results of CPAchecker are attached.


Files

cpa_media_32.pax (22 MB) cpa_media_32.pax CPAchecker run on drivers/media/ Pavel Shved, 03/31/2011 12:20 PM

Related issues 1 (1 open0 closed)

Blocked by Linux Driver Verification - Bug #1019: Our models are not correctly understood by CPAcheckerNewMikhail Mandrykin04/04/2011

Actions
Actions

Also available in: Atom PDF