Project

General

Profile

Actions
Copy link

Bug #8013

closed

Problems with error traces - undefined __CPAchecker_TMP_X

Added by Alexey Khoroshilov about 7 years ago. Updated about 7 years ago.

Status:
Rejected
Priority:
High
Assignee:
-
Category:
-
Target version:
-
Start date:
03/07/2017
Due date:
% Done:

0%

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

Description

For example, error trace for
drivers/usb/core/usbcore.ko
linux:usb:dev
2.6.33.20

contains fragment:

690              assume(__CPAchecker_TMP_1 != ((unsigned long)((struct dentry *)0)));
690              assume(__CPAchecker_TMP_2 != ((unsigned long)inode));
694              dev = (struct usb_device *)0;
697              assume(((unsigned long)dev) != ((unsigned long)((struct usb_device *)0)));
697              assume(__CPAchecker_TMP_3 == 0U);

where there are many __CPAchecker_TMP_X variables used in assumes, but there is no definition of these variables.

Files

witness.24.graphml.zip (22.7 KB) witness.24.graphml.zip Evgeny Novikov, 03/07/2017 01:53 PM
Actions
Copy link

Also available in: Atom PDF