goto-cc - Интернет в облаке

ПРОГРАММА:

ИМЯ

cbmc - Средство проверки ограниченных моделей для программ на C / C ++ и Java

СИНТАКСИС

CBMC [--имущество свойство-id] файл.с ...

CBMC [--показать-свойства] файл.с ...

CBMC [--все свойства] файл.с ...

перейти к копия [-Я включить-путь] [-с] файл.с [-или же Outfile.o]

гото-инструмент вводить Outfile

Здесь перечислены только самые полезные опции; остаток см. ниже.

ОПИСАНИЕ

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

перейти к копия читает исходный код и генерирует бинарный файл goto. Его интерфейс командной строки
разработан, чтобы имитировать GCC(1). Отметим, в частности, что перейти к копия различает
фазы компиляции и компоновки, как это делает gcc. CBMC ожидает бинарный goto, для которого
связывание завершено.

гото-инструмент читает бинарный goto, выполняет заданное преобразование программы, а затем
записывает полученную программу в виде двоичного файла на диск.

Обычный поток: (1) преобразовать исходный код в бинарный goto с помощью goto-cc, затем (2)
выполнить контрольно-измерительную аппаратуру с помощью инструмента goto, и, наконец, (3) выполнить анализ с помощью
cbmc.

ДОПОЛНИТЕЛЬНЫЕ ОПЦИИ

FRONTEND ДОПОЛНИТЕЛЬНЫЕ ОПЦИИ (кбмк и перейти-cc)
-I путь
Установить путь включения (C / C ++)

-D макрос
Определить макрос препроцессора (C / C ++)

--предпроцесс
Остановить после предварительной обработки

--show-символ-таблица
Показать таблицу символов

--show-goto-функции
Показать программу перехода

АРХИТЕКТУРНЫЙ ДОПОЛНИТЕЛЬНЫЕ ОПЦИИ (кбмк и перейти-cc)
CBMC по умолчанию использует архитектурные настройки, соответствующие параметрам машины CBMC is
выполняется, т. е. указанные ниже настройки необходимы только при проверке программного обеспечения, которое
предназначен для работы на другой архитектуре или ОС. перейти к копия генерирует goto-бинарный файл для
конкретная архитектура, т. е. архитектура не может быть изменена после того, как бинарный goto
генерируется.

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

--LP64, --ILP64, --LLP64, --ILP32, --LP32
Установить ширину int, long и указателей

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

- с прямым порядком байтов
Разрешить обратное преобразование слов в байты

--unsigned-char
Сделать "char" беззнаковым по умолчанию

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

--os Установить целевую операционную систему

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

--нетибиблиотека
Отключить встроенную абстрактную библиотеку C

--round-to-ближайший, --round-плюс-inf, --round-to-minus-inf, --round-to-ноль
Режим округления с плавающей запятой IEEE для использования при запуске программы (по умолчанию округлено
до ближайшего). Проверяемая программа может переопределить этот параметр, например, с помощью
фесеткруглый(3).

ПРОГРАММА ПРИБОРЫ ДОПОЛНИТЕЛЬНЫЕ ОПЦИИ (кбмк и гото-инструмент)
Оба формата CBMC и гото-инструмент может генерировать утверждения, которые отлавливают конкретные распространенные ошибки,
Как указано ниже.

--bounds-проверить
Включить проверку границ массива

--div-на-ноль-проверка
Включить деление на ноль проверок

--поинтер-чек
Включить проверку указателя

--signed-overflow-check
Включить арифметические проверки переполнения и потери значимости для целочисленной арифметики со знаком

--unsigned-overflow-check
Включить арифметические проверки переполнения и потери значимости для беззнаковой целочисленной арифметики

--нан-проверить
Проверить вычисления с плавающей запятой на NaN

- нет утверждений
Игнорировать утверждения, предоставленные пользователем

- без допущений
Игнорировать предположения, сделанные пользователем

- метка-ошибки
Убедитесь, что данный ярлык недоступен

ПРОГРАММА ПРИБОРЫ ДОПОЛНИТЕЛЬНЫЕ ОПЦИИ (гото-инструмент только)
гото-инструмент поддерживает дальнейшие, более сложные преобразования программ.

--нонде-летучие
Делает чтение из изменчивых переменных недетерминированным

--isr функция
Инструментирует процедуру обслуживания прерывания с заданным именем

--mmio Instruments ввод-вывод с отображением в память

--nondet-static
Переменные со статическим временем жизни инициализируются недетерминированно.

--дамп-с
Выведите исходный код ANSI-C вместо двоичного файла goto.

BMC ДОПОЛНИТЕЛЬНЫЕ ОПЦИИ (кбмк)
--все свойства
Сообщить о статусе всех свойств

--show-свойства
Показывать только свойства

--show-лупы
Показать петли в программе

--cover-утверждения
Проверить, какие утверждения достижимы

- название функции
Установить имя основной функции

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

- только программа
Показывать только выражение программы

- номер глубины
Ограничить глубину поиска

--раскрутить номер
Размотайте петли nr раз

- без ветра L: B, ...
Размотайте цикл L с границей B (используйте --show-loops, чтобы получить идентификаторы цикла)

--show-vcc
Показать условия проверки

--слайс-формула
Удалить назначения, не относящиеся к собственности

--no-раскрутка-утверждения
Не генерировать раскручивающие утверждения

--нет-красивых имен
Не упрощайте идентификаторы

НАЗАД ДОПОЛНИТЕЛЬНЫЕ ОПЦИИ (кбмк)
--димакс
Генерация CNF в формате DIMACS для использования внешними решателями SAT

- украсить-жадный
Украсить контрпример (жадная эвристика)

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

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

--булектор
Использовать логический объект (экспериментальный)

--матсат
Использовать MathSAT (экспериментальный)

--cvc Использовать CVC3 (экспериментально)

--да
Использовать Yices (экспериментально)

--z3 Использовать Z3 (экспериментально)

- уточнение
Использовать процедуру уточнения (экспериментальную)

--outfile имя файла
Формула вывода в данный файл

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

--массивы-uf-всегда
Всегда превращайте массивы в неинтерпретируемые функции

ОКРУЖАЮЩАЯ СРЕДА

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

АВТОРСКИЕ ПРАВА

2001-2014, Дэниел Кренинг, Эдмунд Кларк

Используйте goto-cc онлайн с помощью сервисов onworks.net