Bug #8448
closed
Specify proper safety properties specification for generic:memory
Added by Evgeny Novikov almost 7 years ago.
Updated over 6 years ago.
Category:
Requirement specifications
Description
I attached input verifier files for third-party testing.
Files
Update to the recent commit in branch smg_witness_for_ldv (25831) didn't help, so, wait, till Anton will fix CPAchecker SMG.
- Assignee changed from Evgeny Novikov to Anton Vasilyev
- Assignee changed from Anton Vasilyev to Evgeny Novikov
I realized why I have assigned this issue to me. It is intended just for updating references to CPAchecker SMG within Klever configuration files. Actual fixes in CPAchecker SMG are beyond of it.
- File deleted (
CPAchecker files.zip)
Upload proper input files for CPAchecker rather than its logs.
- Status changed from New to Rejected
- Assignee deleted (
Evgeny Novikov)
Anton found out that the problem is with incorrect safety properties specification.
- Subject changed from Current version of CPAchecker SMG does not find even trivial bug for its only unsafe test case to Specify proper safety properties specification for generic:memory
- Description updated (diff)
- Category changed from Addons to Requirement specifications
- Status changed from Rejected to Open
- Assignee set to Evgeny Novikov
- Priority changed from Urgent to Immediate
- Status changed from Open to Closed
I fixed this issue in master in 7cef633b. From now safety properties to be checked should be specified for corresponding verifier profiles since they are yet another verifier option.
Also available in: Atom
PDF