https://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692019-03-15T10:14:21ZOpen-Source ProjectsDeductive Verification Tools for Linux Kernel - Bug #9546: Frama-C (CIL) for GCC does not behave like GCC when casting ternary operatorshttps://forge.ispras.ru/issues/9546?journal_id=358032019-03-15T10:14:21ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Blocks</strong> <i><a class="issue tracker-1 status-5 priority-4 priority-default closed parent" href="/issues/6629">Bug #6629</a>: Used CIL is outdated</i> added</li></ul> Deductive Verification Tools for Linux Kernel - Bug #9546: Frama-C (CIL) for GCC does not behave like GCC when casting ternary operatorshttps://forge.ispras.ru/issues/9546?journal_id=358062019-03-15T10:14:41ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Related to</strong> <i><a class="issue tracker-1 status-6 priority-6 priority-high2 closed" href="/issues/9534">Bug #9534</a>: Incorrect printing of Linux BUILD_BUG_ON</i> added</li></ul> Deductive Verification Tools for Linux Kernel - Bug #9546: Frama-C (CIL) for GCC does not behave like GCC when casting ternary operatorshttps://forge.ispras.ru/issues/9546?journal_id=358102019-03-15T11:54:05ZMikhail Mandrykinmandrykin@ispras.ru
<ul></ul><p>This is actually an old bug that was already fixed in Silicon (v14.0), but was somehow lost during the merge in <a href="https://forge.ispras.ru/projects/astraver/repository/framac/revisions/b8012367250cdac12296f988e2ac37b88c9339fd" class="external">b8012367</a>. Fixed in <a href="https://forge.ispras.ru/projects/astraver/repository/framac/revisions/f2445d34ea27c21d020a1fb59e297c3d61d38c15" class="external">f2445d34</a></p> Deductive Verification Tools for Linux Kernel - Bug #9546: Frama-C (CIL) for GCC does not behave like GCC when casting ternary operatorshttps://forge.ispras.ru/issues/9546?journal_id=358172019-03-17T08:26:53ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>The fix works well! Merges do can bring strange issues, so, there is nothing surprising. Please, close the issue.</p> Deductive Verification Tools for Linux Kernel - Bug #9546: Frama-C (CIL) for GCC does not behave like GCC when casting ternary operatorshttps://forge.ispras.ru/issues/9546?journal_id=358332019-03-18T10:05:43ZMikhail Mandrykinmandrykin@ispras.ru
<ul><li><strong>Status</strong> changed from <i>New</i> to <i>Closed</i></li></ul>