Віктор - Онлайн у хмарі

ПРОГРАМА:

ІМ'Я

victor - намагається розрядити умови перевірки за допомогою розв'язувачів SMT

СИНТАКСИС

переможець [ОДИНИЦЯ]

ОПИС

Команда переможець команда є оболонкою навколо ViCToR (vct), що спрощує його використання. ВІКТОР
переводить умови перевірки SPARK у бібліотеку SMTlib і передає їх до розв’язувача SMT.
SPARK поставляється з одним таким вирішувачем SMT, альт-ерго, але можна використовувати інші розв'язувачі
такий як cvc3.

Передбачене використання victor полягає в тому, щоб розряджати справжні VC, що залишилися від спрощувача, а ні
замініть спрощувач. Також зверніть увагу, що ViCToR вважається експериментальним
функція на даний момент.

Ця сторінка посібника лише підсумовує переможець прапорці командного рядка, див
Посібник VictorWrapper для отримання додаткової інформації.

ВАРІАНТИ

Ці параметри не повністю відповідають звичайному синтаксису командного рядка GNU, оскільки параметри починаються з
одна тире замість звичайних двох.

-h, -допомога
Показує довідку командного рядка.

-t=СЕКУНДИ
Тайм-аут розв’язувача SMT через стільки секунд (за замовчуванням 5) використання Ulimit, до
вимкнути тайм-аут, вказати 0.

-m=МЕГАБАЙТИ
Обмежте використання розв’язувача SMT цією кількістю МіБ віртуальної пам’яті (за замовчуванням без обмежень).
Ulimit.

-v Ігноруйте наявність файлів siv і обробляйте лише файли vcg. За замовчуванням дано
a БЛОК наприклад foo, victor спочатку спробує обробити foo.siv, а потім відступить
до foo.vcg.

- звичайний Звичайний режим — приховування таймінгу та версій.

-solver=РОЗВ'ЯЗУВАЧ
Визначає альтернативний вирішувач SMT. За замовчуванням ми використовуємо alt-ergo. Може бути одним із альтернативних
ergo, cvc3, yices або z3. Alt-ergo Solver поширюється разом із SPARK. CVC3
Solver є частиною Debian. Розв’язувачі yices і z3 є запатентованими.

Використовуйте victor онлайн за допомогою сервісів onworks.net