Actions
Bug #8448
closedSpecify proper safety properties specification for generic:memory
Status:
Closed
Priority:
Immediate
Assignee:
Category:
Requirement specifications
Target version:
Start date:
09/20/2017
Due date:
% Done:
0%
Estimated time:
Detected in build:
svn
Platform:
Published in build:
Description
I attached input verifier files for third-party testing.
Files
Updated by Evgeny Novikov over 6 years ago
Update to the recent commit in branch smg_witness_for_ldv (25831) didn't help, so, wait, till Anton will fix CPAchecker SMG.
Updated by Anton Vasilyev over 6 years ago
- Assignee changed from Evgeny Novikov to Anton Vasilyev
Updated by Evgeny Novikov over 6 years ago
- 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.
Updated by Evgeny Novikov over 6 years ago
- File CPAchecker files.zip CPAchecker files.zip added
Upload proper input files for CPAchecker rather than its logs.
Updated by Evgeny Novikov over 6 years ago
- Status changed from New to Rejected
- Assignee deleted (
Evgeny Novikov)
Anton found out that the problem is with incorrect safety properties specification.
Updated by Evgeny Novikov over 6 years ago
- 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
Updated by Evgeny Novikov over 6 years ago
- 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.
Actions