goto-cc - Інтернет у хмарі

ПРОГРАМА:

ІМ'Я

cbmc - Перевірка обмеженої моделі для програм C/C++ і Java

СИНТАКСИС

cbmc [--власність ідентифікатор власності] файл.c ...

cbmc [--show-properties] файл.c ...

cbmc [--всі властивості] файл.c ...

goto-cc [-І включати-шлях] [-c] файл.c [-або outfile.o]

goto-інструмент infile вихідний файл

Тут наведено лише найбільш корисні параметри; решту дивіться нижче.

ОПИС

cbmc створює сліди, які демонструють, як твердження може бути порушено, або доводить це
твердження не може бути порушено протягом заданої кількості ітерацій циклу. CBMC може читати
вихідний код безпосередньо, або goto-двійковий, згенерований goto-cc. Програми на Java подаються як
файли класу. Без будь-яких додаткових опцій cbmc перевіряє всі властивості (автоматично
створені або визначені користувачем), знайдені в програмі. Якщо якась із властивостей може бути
порушено, контрприклад друкується, а аналіз припиняється. Аналіз може бути
обмежено певною властивістю за допомогою параметра --property. Результат перевірки
для всіх властивостей можна отримати за допомогою параметра --all-properties.

goto-cc читає вихідний код і генерує двійковий файл goto. Його інтерфейс командного рядка
розроблений, щоб імітувати, що з ПКУ(1). Зазначимо, зокрема, що goto-cc розрізняє між
етапи компіляції та зв'язування, як це робить gcc. cbmc очікує goto-двійковий для якого
зв'язування завершено.

goto-інструмент зчитує двійковий перехід, виконує задане перетворення програми, а потім
записує отриману програму як goto-binary на диск.

Звичайний потік полягає в тому, щоб (1) перевести джерело в двійковий файл goto за допомогою goto-cc, потім (2)
виконати інструментування за допомогою goto-instrument і, нарешті, (3) виконати аналіз за допомогою
cbmc.

ВАРІАНТИ

ФРОНТЕНД ВАРІАНТИ (cbmc та goto-cc)
- Я шлях
Встановити шлях для включення (C/C++)

-D макрос
Визначити макрос препроцесора (C/C++)

-- попередня обробка
Зупинити після попередньої обробки

--показати-символ-таблицю
Показати таблицю символів

--show-goto-functions
Показати програму переходу

АРХІТЕКТУРНИЙ ВАРІАНТИ (cbmc та goto-cc)
cbmc за замовчуванням використовує архітектурні налаштування, які відповідають параметрам машини cbmc is
виконується на, тобто наведені нижче налаштування потрібні лише під час перевірки програмного забезпечення, яке є
призначений для роботи на іншій архітектурі або ОС. goto-cc генерує двійковий перехід для a
конкретна архітектура, тобто архітектура не може бути змінена після того, як goto-бінарний є
генерується.

--16, --32, --64
Встановити ширину int

--LP64, --ILP64, --LLP64, --ILP32, --LP32
Встановити ширину int, long і покажчиків

--little-endian
Дозволити перетворення слова-байти з маленьким байтом

--big-endian
Дозволити перетворення слова в байти з великим порядком

--unsigned-char
Зробіть "char" непідписаним за замовчуванням

--arch Встановити цільову архітектуру

--os Встановити цільову операційну систему

--без арки
Не створюйте архітектуру

--без бібліотеки
Вимкніть вбудовану абстрактну бібліотеку C

--округлення до найближчого, --округлення до плюс-inf, --округлення до мінус-inf, --округлення до нуля
Режим округлення з плаваючою комою IEEE, який використовується під час початку програми (за умовчанням — округлення
до найближчого). Програма, що перевіряється, може замінити це налаштування, наприклад, with
fesetround(3).

ПРОГРАМА ІНСТРУМЕНТАЦІЯ ВАРІАНТИ (cbmc та goto-інструмент)
обидві cbmc та goto-інструмент може генерувати твердження, які ловлять конкретні поширені помилки,
як зазначено нижче.

--bounds-check
Увімкнути перевірку меж масиву

--div-by-zero-check
Увімкнути перевірку поділу на нуль

--покажчик-перевірка
Увімкнути перевірку покажчика

--signed-overflow-check
Увімкнути арифметичну перевірку переповнення та заниження для цілочисельної арифметики зі знаком

--unsigned-overflow-check
Увімкнути арифметичну перевірку переповнення та заниження для цілочисельної арифметики без знака

--нан-чек
Перевірте обчислення з плаваючою комою для NaN

-- немає тверджень
Ігноруйте твердження, надані користувачами

--без припущень
Ігноруйте припущення, надані користувачем

--мітка мітки помилки
Переконайтеся, що дана мітка недоступна

ПРОГРАМА ІНСТРУМЕНТАЦІЯ ВАРІАНТИ (goto-інструмент тільки)
goto-інструмент підтримує подальші, більш складні перетворення програм.

--непостійний
Робить читання змінних змінних недетермінованими

--isr функція
Інструментує процедуру обслуговування переривань із заданим іменем

--mmio Інструменти введення/виведення з відображенням пам'яті

--нестатичний
Змінні зі статичним часом життя ініціалізуються недетерміновано

--dump-c
Виведіть вихідний код ANSI-C замість двійкового переходу.

BMC ВАРІАНТИ (cbmc)
--всі властивості
Повідомити про стан усіх властивостей

--show-properties
Показувати лише властивості

--show-loops
Показати цикли в програмі

--обкладинки-твердження
Перевірте, які твердження доступні

--назва функції
Встановити назву основної функції

-- ідентифікатор власності
Перевіряйте лише конкретну властивість із заданим ідентифікатором

--лише для програми
Показувати лише програмний вираз

-- глибина №
Обмежте глибину пошуку

--розмотати nr
Розмотайте петлі nr разів

--розслабтеся L:B,...
Розгорнути цикл L з обмеженням B (використовуйте --show-loops, щоб отримати ідентифікатори циклу)

--show-vcc
Покажіть умови перевірки

--зріз-формула
Видалити призначення, не пов’язані з властивістю

--не-розкручування-тверджень
Не генеруйте невтішних тверджень

--ні-гарні-імена
Не спрощуйте ідентифікатори

НАЗАД ВАРІАНТИ (cbmc)
--dimacs
Згенеруйте CNF у форматі DIMACS для використання зовнішніми розв’язувачами SAT

--прикрасити-жадібний
Прикрашайте контрприклад (жадібна евристика)

--smt1 Вивести підцілі в синтаксисі SMT1 (експериментальний)

--smt2 Вивести підцілі в синтаксисі SMT2 (експериментальний)

-- булектор
Використовуйте Boolector (експериментальний)

--mathsat
Використовуйте MathSAT (експериментальний)

--cvc Використовуйте CVC3 (експериментальний)

--так
Використовуйте Yices (експериментальний)

--z3 Використовуйте Z3 (експериментальний)

-- уточнити
Використовуйте процедуру уточнення (експериментально)

-- ім'я файлу вихідного файлу
Вивести формулу в заданий файл

--масиви-uf-ніколи
Ніколи не перетворюйте масиви на неінтерпретовані функції

--масиви-uf-завжди
Завжди перетворюйте масиви в неінтерпретовані функції

НАВКОЛИШНЄ СЕРЕДОВИЩЕ

Усі інструменти враховують змінну середовища TMPDIR під час створення тимчасових файлів і
каталогів. Крім того, зауважте, що препроцесор, який використовується CBMC, використовуватиме середовище
змінні для пошуку заголовних файлів. GOTO-CC має на меті прийняти всі змінні середовища, які
GCC робить.

АВТОРСЬКЕ

2001-2014, Деніел Кронінг, Едмунд Кларк

Використовуйте goto-cc онлайн за допомогою служб onworks.net