Bug #7394
closedRestore support for property automata rule specifications
0%
Description
Currently strategies with property automata do not work and should be fixed.
Also most of rule specifications still does not support property automata.
Updated by Evgeny Novikov almost 8 years ago
- Category deleted (
Program fragments generation)
Updated by Vitaly Mordan almost 8 years ago
- Priority changed from Normal to Urgent
This is the last strategy, which still does not work and represent dead code.
It must be restored.
Updated by Evgeny Novikov almost 8 years ago
- Priority changed from Urgent to High
It bears pure experimental sense while there are other really important issues.
Updated by Vitaly Mordan almost 8 years ago
Support of property automata for separated strategies has been restored in branch restore_property_automata.
All tests for 'instrumentation' strategies are passing.
Note, that 'property automata' option requires CPAchecker branch muauto (preferable configuration is ldv-spa).
Updated by Vitaly Mordan almost 8 years ago
Support of multiple property verification (or on-the-fly specification decomposition) has been restored.
Note, that MPV-based strategies require CPAchecker branch muauto (preferable configuration is ldv-mpa).
Updated by Evgeny Novikov almost 8 years ago
- Status changed from New to Closed
- Published in build set to e317c7b
I merged the branch in e317c7b.