Bug #7342
closed
Option cpa.arg.errorPath.exportImmediately=true is broken with valueAnalysis
Added by Pavel Andrianov almost 8 years ago.
Updated about 6 years ago.
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.
- 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.
- Assignee changed from Evgeny Novikov to Vitaly Mordan
- Priority changed from Urgent to Normal
The work around is in b02d9b1 to master.
- 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.
- Status changed from Feedback to Rejected
- Assignee deleted (
Vitaly Mordan)
No progress during a year, so, I reject it.
Also available in: Atom
PDF