https://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692017-09-20T10:38:25ZOpen-Source ProjectsKlever - Bug #8448: Specify proper safety properties specification for generic:memoryhttps://forge.ispras.ru/issues/8448?journal_id=315942017-09-20T10:38:25ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>Update to the recent commit in branch <em>smg_witness_for_ldv</em> (25831) didn't help, so, wait, till Anton will fix CPAchecker SMG.</p> Klever - Bug #8448: Specify proper safety properties specification for generic:memoryhttps://forge.ispras.ru/issues/8448?journal_id=317742017-10-03T17:07:46ZAnton Vasilyevvasilyev@ispras.ru
<ul><li><strong>Assignee</strong> changed from <i>Evgeny Novikov</i> to <i>Anton Vasilyev</i></li></ul> Klever - Bug #8448: Specify proper safety properties specification for generic:memoryhttps://forge.ispras.ru/issues/8448?journal_id=317752017-10-04T07:21:43ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Assignee</strong> changed from <i>Anton Vasilyev</i> to <i>Evgeny Novikov</i></li></ul><p>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.</p> Klever - Bug #8448: Specify proper safety properties specification for generic:memoryhttps://forge.ispras.ru/issues/8448?journal_id=317782017-10-04T12:05:19ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>File</strong> deleted (<del><i>CPAchecker files.zip</i></del>)</li></ul> Klever - Bug #8448: Specify proper safety properties specification for generic:memoryhttps://forge.ispras.ru/issues/8448?journal_id=317792017-10-04T12:05:53ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>File</strong> <a href="/attachments/5343">CPAchecker files.zip</a> <a class="icon-only icon-download" title="Download" href="/attachments/download/5343/CPAchecker%20files.zip">CPAchecker files.zip</a> added</li></ul><p>Upload proper input files for CPAchecker rather than its logs.</p> Klever - Bug #8448: Specify proper safety properties specification for generic:memoryhttps://forge.ispras.ru/issues/8448?journal_id=317802017-10-04T12:10:18ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Status</strong> changed from <i>New</i> to <i>Rejected</i></li><li><strong>Assignee</strong> deleted (<del><i>Evgeny Novikov</i></del>)</li></ul><p>Anton found out that the problem is with incorrect safety properties specification.</p> Klever - Bug #8448: Specify proper safety properties specification for generic:memoryhttps://forge.ispras.ru/issues/8448?journal_id=317812017-10-04T12:11:25ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Subject</strong> changed from <i>Current version of CPAchecker SMG does not find even trivial bug for its only unsafe test case</i> to <i>Specify proper safety properties specification for generic:memory</i></li><li><strong>Description</strong> updated (<a title="View differences" href="/journals/31781/diff?detail_id=36023">diff</a>)</li><li><strong>Category</strong> changed from <i>Addons</i> to <i>Requirement specifications</i></li><li><strong>Status</strong> changed from <i>Rejected</i> to <i>Open</i></li><li><strong>Assignee</strong> set to <i>Evgeny Novikov</i></li><li><strong>Priority</strong> changed from <i>Urgent</i> to <i>Immediate</i></li></ul> Klever - Bug #8448: Specify proper safety properties specification for generic:memoryhttps://forge.ispras.ru/issues/8448?journal_id=317862017-10-06T09:14:04ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Status</strong> changed from <i>Open</i> to <i>Closed</i></li></ul><p>I fixed this issue in master in <a class="changeset" title="Specify safety properties in verifier profiles Also, fix memory safety checking (https://forge.i..." href="https://forge.ispras.ru/projects/klever/repository/331/revisions/7cef633b1f794a108b215696c0eb26bcc6df8568">7cef633b</a>. From now safety properties to be checked should be specified for corresponding verifier profiles since they are yet another verifier option.</p>