Project

General

Profile

Actions

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.

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.

Actions #1

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.

Actions #2

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.

Actions #3

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.

Actions #4

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

Also available in: Atom PDF