Project

General

Profile

Task #5433

[test] write executable SMT-LIB code at testcase comments

Added by Sergey Smolov almost 6 years ago. Updated over 5 years ago.

Status:
Closed
Priority:
Normal
Category:
-
Target version:
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 и псевдокод на его основе из тестов необходимо изжить.

History

#1

Updated by Sergey Smolov almost 6 years ago

Также не мешает проследить за Expected output.

#2

Updated by Artem Kotsynyak almost 6 years ago

  • Status changed from New to Resolved

r701

#3

Updated by Sergey Smolov almost 6 years ago

  • Status changed from Resolved to Verified
#4

Updated by Andrei Tatarnikov over 5 years ago

  • Status changed from Verified to Closed
  • % Done changed from 0 to 100
  • Published in build set to 141226

Also available in: Atom PDF