Actions
Task #5433
closed[test] write executable SMT-LIB code at testcase comments
Start date:
11/17/2014
Due date:
% Done:
100%
Estimated time:
Detected in build:
svn
Published in build:
141226
Description
Предлагается в комментариях к jUnit-тестам писать только исполняемый код на SMT-LIB. Например, в ru.ispras.fortress.solver.constraint.BitVectorExtractionTestCase вместо:
[comment]
(declare-const x (_ BitVec 32))
(declare-const y (_ BitVec 8))
(assert (= x (_ bv100 257)))
(assert (= y ((_ extract 0 7) x))
(check-sat)
(get-value (x))
(exit)
[/comment]
нужно писать:
[comment]
(declare-const x (_ BitVec 32))
(declare-const y (_ BitVec 8))
(assert (= x (_ bv257 32)))
(assert (= y ((_ extract 7 0) x)))
(check-sat)
(get-value (x y))
(exit)
[/comment]
Для проверки можно использовать http://rise4fun.com/Z3
Некорректный SMT-LIB и псевдокод на его основе из тестов необходимо изжить.
Updated by Sergey Smolov about 10 years ago
Также не мешает проследить за Expected output.
Updated by Sergey Smolov almost 10 years ago
- Status changed from Resolved to Verified
Updated by Andrei Tatarnikov almost 10 years ago
- Status changed from Verified to Closed
- % Done changed from 0 to 100
- Published in build set to 141226
Actions