https://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692019-03-13T12:25:47ZOpen-Source ProjectsKlever - Feature #9532: Update CPAcheckerhttps://forge.ispras.ru/issues/9532?journal_id=357642019-03-13T12:25:47ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Status</strong> changed from <i>New</i> to <i>Resolved</i></li></ul><p>I switched CPAchecker to trunk:30732 in branch <em>frama-c-cil</em>. It seems that the new version takes a bit more resources but sometimes it works better, e.g. there are not some parsing failures and timeouts.</p>
<p>Anyway we will have to switch to the latest version of CPAchecker to get extended witnesses from it.</p> Klever - Feature #9532: Update CPAcheckerhttps://forge.ispras.ru/issues/9532?journal_id=357942019-03-15T06:18:46ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>One our test case failed due to <a class="external" href="https://gitlab.com/sosy-lab/software/cpachecker/issues/570">https://gitlab.com/sosy-lab/software/cpachecker/issues/570</a>. It would be better to update CPAchecker one more time rather than to add one more bad preset unknown mark. But I do not know when CPAchecker will be fixed.</p> Klever - Feature #9532: Update CPAcheckerhttps://forge.ispras.ru/issues/9532?journal_id=358302019-03-17T12:29:13ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>Another one bug in CPAchecker is <a class="external" href="https://gitlab.com/sosy-lab/software/cpachecker/issues/348">https://gitlab.com/sosy-lab/software/cpachecker/issues/348</a>. One of our validation test case fails due to it. BTW, old CIL replaces enumerators with their values when they are used, so there were not such the bug.</p>
<p>Unfortunately, again we can't rely that somebody will fix this bug in CPAchecker soon.</p> Klever - Feature #9532: Update CPAcheckerhttps://forge.ispras.ru/issues/9532?journal_id=358722019-03-25T13:09:00ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Status</strong> changed from <i>Resolved</i> to <i>Closed</i></li></ul><p>I merged the branch to master in <a class="changeset" title="Increase time limit since one test case exceeded the previous one from time to time https://forg..." href="https://forge.ispras.ru/projects/klever/repository/331/revisions/c082518076482dacb70c6e55c98814e7e2ea8da5">c082518</a>. Let's wait for CPAchecker fixes separately as it is not known when they will be.</p>