Open-Source Projects: Issueshttps://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692020-09-11T11:03:19ZOpen-Source Projects
Redmine Fortress - Task #10494 (Closed): check Windows build of Boolector on project testshttps://forge.ispras.ru/issues/104942020-09-11T11:03:19ZSergey Smolovsmolov@ispras.ru
<p>Переключиться на ветку <strong>boolector-solver-integrating</strong> и в файле <strong>build.gradle</strong> для SMT-решателя boolector вместо подгрузки его извне (там сейчас подтягивается неработоспособная Windows-сборка) прописать полученную локальную сборку. Затем запустить все jUnit-тесты проекта и убедиться в том, что: а) в тестах участвует Boolector (возможно, не во всех, см. переменную <strong>isSuitableForBoolector</strong> в классе <strong>GenericSolverTestBase</strong> ); б) тесты, в которых задействуется Boolector, проходят.</p> Fortress - Task #10492 (Closed): use CVC4 1.8 in testinghttps://forge.ispras.ru/issues/104922020-09-09T16:10:30ZSergey Smolovsmolov@ispras.ruFortress - Bug #10370 (Closed): class ru.ispras.fortress.solver.constraint.Formulas cannot be ca...https://forge.ispras.ru/issues/103702020-06-08T13:56:16ZSergey Smolovsmolov@ispras.ru
<p>68 test cases fall with the stack trace:<br /><pre>
java.lang.ClassCastException: class ru.ispras.fortress.solver.constraint.Formulas cannot be cast to class ru.ispras.fortress.solver.constraint.Sat4jFormula (ru.ispras.fortress.solver.constraint.Formulas and ru.ispras.fortress.solver.constraint.Sat4jFormula are in unnamed module of loader 'app')
at ru.ispras.fortress.solver.engine.sat.Sat4jSolver.solve(Sat4jSolver.java:74)
at ru.ispras.fortress.solver.constraint.GenericSolverTestBase.solveAndCheckResult(GenericSolverTestBase.java:167)
at ru.ispras.fortress.solver.constraint.GenericSolverTestBase.runSolverTests(GenericSolverTestBase.java:115)
</pre></p> Fortress - Task #10002 (Closed): get Boolector solver from server as dependencyhttps://forge.ispras.ru/issues/100022019-12-20T12:44:32ZSergey Smolovsmolov@ispras.ruFortress - Task #10001 (Rejected): SMT-LIBv2 benchmarkshttps://forge.ispras.ru/issues/100012019-12-20T12:41:49ZSergey Smolovsmolov@ispras.ru
<p>Collection of SMT-LIBv2 constraints that were generated by formal verification tools (Retrascope, MicroTESK) + JUnit test cases that solve them.</p> Castle - Task #9999 (Closed): ChangeLog -> ChangeLog.mdhttps://forge.ispras.ru/issues/99992019-12-20T11:57:43ZSergey Smolovsmolov@ispras.ru
<p>Rewrite ChangeLog file to Markdown format.</p> Castle - Task #9998 (Closed): README -> README.mdhttps://forge.ispras.ru/issues/99982019-12-20T11:57:11ZSergey Smolovsmolov@ispras.ru
<p>Rewrite README to Markdown format.</p> Fortress - Feature #9123 (Closed): calculate DataType for 'BVEXTRACT(i, i, x)' NodeOperation objectshttps://forge.ispras.ru/issues/91232018-07-18T10:16:35ZSergey Smolovsmolov@ispras.ru
<p>For '<abbr title="i, i, x">BVEXTRACT</abbr>' NodeOperation objects, where <em>i</em> is a non-NodeValue object, an attempt to calculate it's DataType causes the following exception:<br /><pre>
java.lang.IllegalStateException: Parameter is not a value: i
at ru.ispras.fortress.expression.NodeOperation.getParams(NodeOperation.java:260)
at ru.ispras.fortress.expression.NodeOperation.getDataType(NodeOperation.java:196)
</pre></p> Fortress - Feature #8709 (Closed): 'public static boolean isOperation(final Node node, final T .....https://forge.ispras.ru/issues/87092018-02-08T07:31:05ZSergey Smolovsmolov@ispras.ruCastle - Task #6507 (Closed): build.gradle: get ANTLR jar from serverhttps://forge.ispras.ru/issues/65072016-01-14T08:53:59ZSergey Smolovsmolov@ispras.ru
<p>Предлагаю не хранить jar-файл компонента ANTLR непосредственно в репозитории проекта, а подгружать с сервера, как это сделано в Retrascope с библиотекой Antlrworks:</p>
<pre>
dependencies {
compile 'antlr:antlrworks:1.4.3'
...
compile files( "${project.projectDir}/share/jar/fortress.jar"
, ...
)
}
</pre>
<p>Для этого нужно проконсультироваться с Алексеем Демаковым, пусть положит ANTLR на forge.ispras.ru (если его ещё там нет).</p> C++TESK Testing ToolKit - Bug #4005 (Rejected): удалить пустой READMEhttps://forge.ispras.ru/issues/40052013-03-15T14:17:10ZSergey Smolovsmolov@ispras.ru
<p>Что делает пустой файл README в trunk основного проекта?</p> C++TESK Testing ToolKit - Bug #4004 (Closed): Из build'а пропал скрипт install-eclipse-plugin.shhttps://forge.ispras.ru/issues/40042013-03-14T17:36:57ZSergey Smolovsmolov@ispras.ru
<p>Т.е. в trunk проекта он есть, а в сборке не присутствует. <br />Без данного скрипта пропадает возможность установить C++TesK Eclipse plug-in из командной строки.</p>
<p>Просьба починить.</p> C++TESK Testing ToolKit - Bug #3805 (Closed): Ошибка в QuickReferencehttps://forge.ispras.ru/issues/38052012-12-18T08:19:48ZSergey Smolovsmolov@ispras.ru
<p>Файл C++TESK.QuickReference.ru.pdf, страница 10:</p>
<p>"CPPTESK_CONT_CAST_MESSAGE(класс_сообщения)."</p>
<p>Видимо, нужно исправить на</p>
<p>"CPPTESK_CONST_CAST_MESSAGE(класс_сообщения)."</p> C++TESK Testing ToolKit - Bug #3590 (Closed): C++TesK installation fails on OpenSUSE 12.2 x64https://forge.ispras.ru/issues/35902012-10-15T11:18:40ZSergey Smolovsmolov@ispras.ru
<p>Попробовал установить subj на OpenSUSE 12.2 x64. Системные требования были удовлетворены (в соответствии с C++TESK.InstallationGuide.ru.pdf), скрипт установки запускался с опцией --force-install-veritool (Veritool и Icarus Verilog предварительно установлены не были, подключение к сети, естественно, есть).</p>
<p>По-видимому, Icarus Verilog установился корректно, а Veritool - нет.</p>
<p>Лог установочного скрипта в аттаче.</p> CTESK - Bug #2494 (New): warning at build loghttps://forge.ispras.ru/issues/24942012-02-24T06:40:28ZSergey Smolovsmolov@ispras.ru
<p>При сборке возникает следующее предупреждение:</p>
<p>gcc -I. -g -ggdb -O0 -fno-inline -D_GLIBCXX_DEBUG -O -DATL_CLONE_DISABLE -DUSE_FOPEN64 -c c_tracer/c_tracer.c -o c_tracer/c_tracer.o<br />c_tracer/c_tracer.c: In function ‘addTraceToFile’:<br />c_tracer/c_tracer.c:117:7: warning: assignment makes pointer from integer without a cast</p>
<p>Сборка завершается корректно, так что это скорее небольшой досадный недочет.</p>