Project

General

Profile

Actions
Copy link

Bug #8448

closed

Specify proper safety properties specification for generic:memory

Added by Evgeny Novikov over 7 years ago. Updated about 7 years ago.

Status:
Closed
Priority:
Immediate
Assignee:
Evgeny Novikov
Category:
Requirement specifications
Target version:
0.2
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

CPAchecker files.zip (17.9 KB) CPAchecker files.zip Evgeny Novikov, 10/04/2017 03:05 PM
Actions
Copy link
 #1

Updated by Evgeny Novikov over 7 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.

Actions
Copy link
 #2

Updated by Anton Vasilyev about 7 years ago

  • Assignee changed from Evgeny Novikov to Anton Vasilyev
Actions
Copy link
 #3

Updated by Evgeny Novikov about 7 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.

Actions
Copy link
 #4

Updated by Evgeny Novikov about 7 years ago

  • File deleted (CPAchecker files.zip)
Actions
Copy link
 #5

Updated by Evgeny Novikov about 7 years ago

Upload proper input files for CPAchecker rather than its logs.

Actions
Copy link
 #6

Updated by Evgeny Novikov about 7 years ago

  • Status changed from New to Rejected
  • Assignee deleted (Evgeny Novikov)

Anton found out that the problem is with incorrect safety properties specification.

Actions
Copy link
 #7

Updated by Evgeny Novikov about 7 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
Actions
Copy link
 #8

Updated by Evgeny Novikov about 7 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
Copy link

Also available in: Atom PDF