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
 #1

Updated by Evgeny Novikov about 7 years ago

I analyzed a corresponding witness (attached) but there are not definitions for these variables. So this is a CPAchecker (BAM?) issue - open this bug within its issues tracker.

Actions
Copy link
 #2

Updated by Alexey Khoroshilov about 7 years ago

  • Status changed from Rejected to Open
  • Assignee set to Ilja Zakharov
  • Priority changed from Urgent to High

The attached witness is in compliance with requirements to the witnesses [1].
So, there is no a valid reason for bug report in CPAchecker project.

If our tools have some additional requirements to the format, we have to prepare description of them and then it will be possible to discuss the proposal with CPAchecker team.
Ilja is working on that, so he has to take into account the problem described in this ticket as well.

[1] https://github.com/sosy-lab/sv-witnesses/

Actions
Copy link
 #3

Updated by Evgeny Novikov about 7 years ago

  • Status changed from Open to Rejected
  • Assignee deleted (Ilja Zakharov)

After all this issue looks completely strange here. There is not even a more important and generic issue that requests for so called additional requirements from our tools. Indeed these requirements are not from our tools - these requirements aim at representation of witnesses for analysis by experts rather than by other verification tools. Thus such issues should be related with verifier communities, most likely with the SV-COMP one which looks to be a dominating one. Open or request somebody to open a corresponding generic issue within the dedicated projects, e.g. within the one you specified yourself. There one can mention this particular requirement although it is just one of many others. Anyway it would be great if Ilja Zakharov and Alexey Polushkin will be mentioned in the SV-COMP related projects.

Actions
Copy link

Also available in: Atom PDF