Project

General

Profile

Actions
Copy link

Bug #2699

open

BLAST doesn't find an error in a rather simple example with division

Added by Evgeny Novikov over 12 years ago. Updated over 12 years ago.

Status:
New
Priority:
Normal
Assignee:
-
Category:
-
Target version:
-
Start date:
04/04/2012
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

Description

CPAchecker finds it. The example with description in attachment.
In fact the example is a minimal test case (I guess) for a real driver that is also attached. On that driver BLAST quickly fails with the same error, while CPAchecker is killed because of time out of 15 minutes.

Files

Download all files
test.c (330 Bytes) test.c Example with division that fails BLAST Evgeny Novikov, 04/04/2012 03:04 PM
drivers-usb-class-cdc-acm.o.general.i (1.54 MB) drivers-usb-class-cdc-acm.o.general.i Real driver that has the same problem Evgeny Novikov, 04/04/2012 03:04 PM
Actions
Copy link

Also available in: Atom PDF