Project

General

Profile

Bug #8448

Specify proper safety properties specification for generic:memory

Added by Evgeny Novikov about 3 years ago. Updated almost 3 years ago.

Status:
Closed
Priority:
Immediate
Category:
Rule 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

CPAchecker files.zip (17.9 KB) CPAchecker files.zip Evgeny Novikov, 10/04/2017 03:05 PM

History

#1

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

#2

Updated by Anton Vasilyev almost 3 years ago

  • Assignee changed from Evgeny Novikov to Anton Vasilyev
#3

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

#4

Updated by Evgeny Novikov almost 3 years ago

  • File deleted (CPAchecker files.zip)
#5

Updated by Evgeny Novikov almost 3 years ago

Upload proper input files for CPAchecker rather than its logs.

#6

Updated by Evgeny Novikov almost 3 years ago

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

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

#7

Updated by Evgeny Novikov almost 3 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 Rule specifications
  • Status changed from Rejected to Open
  • Assignee set to Evgeny Novikov
  • Priority changed from Urgent to Immediate
#8

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

Also available in: Atom PDF