https://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692022-07-26T13:11:14ZOpen-Source ProjectsKlever - Feature #11782: Update CIFhttps://forge.ispras.ru/issues/11782?journal_id=440062022-07-26T13:11:14ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Status</strong> changed from <i>New</i> to <i>Resolved</i></li></ul><p>I did that in branch <em>update-cif</em>. Let's see on testing results.</p> Klever - Feature #11782: Update CIFhttps://forge.ispras.ru/issues/11782?journal_id=440222022-07-27T07:02:47ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Blocked by</strong> <i><a class="issue tracker-4 status-5 priority-5 priority-high3 closed" href="/issues/11772">Feature #11772</a>: Update CPAchecker</i> added</li></ul> Klever - Feature #11782: Update CIFhttps://forge.ispras.ru/issues/11782?journal_id=440232022-07-27T07:04:21ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Status</strong> changed from <i>Resolved</i> to <i>Open</i></li></ul><p>It turned out that CPAchecker could not spit out error traces containing local static variables (it runs out of heap memory after a long period of time). Thus, it is necessary to fix and update it first (<a class="issue tracker-4 status-5 priority-5 priority-high3 closed" title="Feature: Update CPAchecker (Closed)" href="https://forge.ispras.ru/issues/11772">#11772</a>).</p> Klever - Feature #11782: Update CIFhttps://forge.ispras.ru/issues/11782?journal_id=441692022-08-08T10:13:39ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>Ilya has recently fixed warning from Clang-Tidy (<a class="external" href="https://github.com/ldv-klever/cif/pull/3">https://github.com/ldv-klever/cif/pull/3</a>). This should not affect anything anyhow, so I included the corresponding update into the branch for upcoming testing.</p> Klever - Feature #11782: Update CIFhttps://forge.ispras.ru/issues/11782?journal_id=442522022-08-17T17:23:01ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Blocked by</strong> <i><a class="issue tracker-4 status-5 priority-5 priority-high3 closed" href="/issues/11833">Feature #11833</a>: Update CPAchecker</i> added</li></ul> Klever - Feature #11782: Update CIFhttps://forge.ispras.ru/issues/11782?journal_id=442552022-08-18T07:28:52ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Status</strong> changed from <i>Open</i> to <i>Resolved</i></li></ul><p>I rebased branch <em>update-cif</em> on top of branch <em>update-cpachecker</em> (<a class="issue tracker-4 status-5 priority-5 priority-high3 closed" title="Feature: Update CPAchecker (Closed)" href="https://forge.ispras.ru/issues/11772">#11772</a>, <a class="issue tracker-4 status-5 priority-5 priority-high3 closed" title="Feature: Update CPAchecker (Closed)" href="https://forge.ispras.ru/issues/11833">#11833</a>) and launched CI testing.</p> Klever - Feature #11782: Update CIFhttps://forge.ispras.ru/issues/11782?journal_id=442572022-08-18T13:53:36ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>CI revealed a couple of negative regressions, but they are not crucial. You can see <a class="changeset" title="Specify negative regressions 2 safes became timeouts. Anyway, the corresponding driver is so c..." href="https://forge.ispras.ru/projects/klever/repository/331/revisions/0d03909c333401be3003ee276c9811816b426dbe">0d03909c3</a> for details.</p> Klever - Feature #11782: Update CIFhttps://forge.ispras.ru/issues/11782?journal_id=442622022-08-19T11:14:03ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Status</strong> changed from <i>Resolved</i> to <i>Closed</i></li></ul><p>Verification of a subset of Linux 5.19-rc7 drivers showed a bunch of improvements. The overall CPU time consumed by CPAchecker decreased for ~10%! Correspondingly a lot of timeouts became pretty hard safes and unsafes (some of these unsafes were already revealed early). Thus, a minor fix can result in great improvements. I merged the branch to master in commit:c0d03909c3.</p>