Bug #7394
closed
Restore support for property automata rule specifications
Added by Vitaly Mordan over 8 years ago.
Updated over 8 years ago.
Published in build:
e317c7b
Description
Currently strategies with property automata do not work and should be fixed.
Also most of rule specifications still does not support property automata.
- Category deleted (
Program fragments generation)
- Priority changed from Normal to Urgent
This is the last strategy, which still does not work and represent dead code.
It must be restored.
- Priority changed from Urgent to High
It bears pure experimental sense while there are other really important issues.
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).
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).
- Status changed from New to Closed
- Published in build set to e317c7b
Also available in: Atom
PDF