Open-Source Projects: Issueshttps://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692023-04-04T11:53:25ZOpen-Source Projects
Redmine Runtime Verification - [FEATURE] #12323 (Open): Разработка аниматора Event-Bhttps://forge.ispras.ru/issues/123232023-04-04T11:53:25ZEugene Kornykhinkornevgen@ispras.ru
<p>( ) Знакомство с интерфейсом replay <-> ProB и его реализацией в java-библиотеках<br />( ) Нулевая версия: все параметры всех событий есть в модельной трассе<br />( ) Отладка нулевой версии<br />( ) Первая версия: недостающие параметры событий вычисляются, поддерживаются некоторые шаблоны охранных условий<br />( ) Отладка первой версии<br />( ) Вторая версия: исследование потенциальных охранных условий, из которых можно эффективно автоматически восстанавливать отсутствующие параметры<br />( ) Отладка второй версии</p> Deductive Verification Tools for Linux Kernel - Bug #8031 (New): Why3IDE не запускается из-за нев...https://forge.ispras.ru/issues/80312017-03-15T21:22:17ZEugene Kornykhinkornevgen@ispras.ru
<p><code><br />[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)<br />[kernel] Parsing ../../../../olga/a.c (with preprocessing)<br />[Jessie2] Starting Jessie translation<br />[Jessie2] warning: \separated is not supported by Jessie. This predicate will be ignored<br />[Jessie2] Producing Jessie files in subdir /home/student/olga/a.jessie<br />[Jessie2] File /home/student/olga/a.jessie/a.jc written.<br />[Jessie2] File /home/student/olga/a.jessie/a.cloc written.<br />[Jessie2] Calling Jessie tool in subdir /home/student/olga/a.jessie<br />[Jessie2] Calling VCs generator.<br />why3 ide --extra-config /home/student/.opam/4.03.0/lib/jessie/why3/why3.conf a.mlw<br />[Config] reading extra configuration file /home/student/.opam/4.03.0/lib/jessie/why3/why3.conf<br />Fatal error: exception Glib.GError("\208\157\208\181 \209\131\208\180\208\176\208\187\208\190\209\129\209\140 \208\190\209\130\208\186\209\128\209\139\209\130\209\140 \209\132\208\176\208\185\208\187 \194\171/home/student/.opam/4.03.0/share/why3/images/boomy/delete.png\194\187: \208\157\208\181\209\130 \209\130\208\176\208\186\208\190\208\179\208\190 \209\132\208\176\208\185\208\187\208\176 \208\184\208\187\208\184 \208\186\208\176\209\130\208\176\208\187\208\190\208\179\208\176")<br />a.makefile:15: ошибка выполнения рецепта для цели «why3ide»<br />make: *** [why3ide] Ошибка 2<br />[Jessie2] user error: Jessie subprocess failed: make -f a.makefile why3ide<br />[kernel] Plug-in Jessie2 aborted: invalid user input.<br /></code></p>
<p>Имеется тема fatcow, но нет темы boomy. В инструкции по установке не описана подобная ситуация и не написано, как изменить тему.</p> JavaTESK - Bug #228 (New): Плагин JavaTESK не работает вместе с плагином CTESKhttps://forge.ispras.ru/issues/2282010-05-28T15:12:31ZEugene Kornykhinkornevgen@ispras.ru
<p>вываливается exception "java.lang.NoSuchFieldError: OUTLINE" - все подробности у Андрея Максимова</p> JavaTESK - Bug #199 (Resolved): Checker: Неправильный тип элемента массива в циклахhttps://forge.ispras.ru/issues/1992010-05-11T07:06:56ZEugene Kornykhinkornevgen@ispras.ru
<p>На примере<br /><pre>
void f(String[][] oldmap)
{
for (String[] pair : oldmap) {
}
}
</pre><br />выдается сообщение, что pair должен быть типа String. Такое поведение checker'а является ошибочным.</p> JavaTESK - Bug #195 (Resolved): Checker: не проходит проверка соответствия класса и raw-параметри...https://forge.ispras.ru/issues/1952010-05-06T11:50:34ZEugene Kornykhinkornevgen@ispras.ru
<p>На примере<br /><pre>
class aa<Z> {}
public class a
{
public <T extends aa> void f2(T o)
{
Class<? extends aa> c = o.getClass();
}
}
</pre></p>
<p>выдается ошибка о несоответствующих типах в присваивании. А зря, тут ошибки нет.</p> JavaTESK - Bug #192 (Resolved): Checker: неправильный возвращаемый тип метода getClasshttps://forge.ispras.ru/issues/1922010-04-29T12:13:54ZEugene Kornykhinkornevgen@ispras.ru
<p>Как оказалось, наш JavaTESK не знает про такую вещь относительно метода getClass() :</p>
<p>The java.lang.Class object that represents the runtime class of the object. The result is of type Class<? extends X> where X is the erasure of the static type of the expression on which getClass is called.<br />/ <a class="external" href="http://java.sun.com/j2se/1.5.0/docs/api/java/lang/Object.html#getClass()">http://java.sun.com/j2se/1.5.0/docs/api/java/lang/Object.html#getClass()</a></p>
<p>Надо реализовать это правило.</p>