Actions
Bug #7342
closedOption cpa.arg.errorPath.exportImmediately=true is broken with valueAnalysis
Status:
Rejected
Priority:
Normal
Assignee:
-
Category:
Addons
Target version:
-
Start date:
06/27/2016
Due date:
% Done:
0%
Estimated time:
Detected in build:
svn
Platform:
Published in build:
Description
The counterexample is exported on the fly in AbstractARGRefiner, but the ValueRefiner does not extend this abstract class. Thus witnesses are not exported neither during refinement stage, nor during statistics printing if the option is enabled.
Updated by Evgeny Novikov almost 8 years ago
- Category set to Tasks generation
- Status changed from New to Open
- Assignee changed from Vitaly Mordan to Evgeny Novikov
- Priority changed from Normal to Urgent
I will work around this by myself since we miss target bug bcb4a75bde38~/drivers/hid/hid.ko/linux:chrdev. The work around is very simple - just get rid of this option until it will be fully supported in CPAchecker.
Updated by Evgeny Novikov almost 8 years ago
- Assignee changed from Evgeny Novikov to Vitaly Mordan
- Priority changed from Urgent to Normal
The work around is in b02d9b1 to master.
Updated by Evgeny Novikov over 7 years ago
- Category changed from Tasks generation to Addons
- Status changed from Open to Feedback
This is a bug in CPAchecker which has another issue tracker. So when it will be reported at the right place or fixed without that, we will reject this issue.
Updated by Evgeny Novikov about 6 years ago
- Status changed from Feedback to Rejected
- Assignee deleted (
Vitaly Mordan)
No progress during a year, so, I reject it.
Actions