cpachecker

Начало работы с cpachecker

• Инструкции по установке
• Руководящие принципы вклада
• Инструкции по разработке

Больше документации можно найти в doc/ Directory.

Лицензия и авторское право

Cpachecker имеет лицензию по лицензии Apache 2.0 с Copyright Dirk Beyer и другими (ср. Authors.md для полного списка всех участников). Сторонние библиотеки находятся под различными другими лицензиями и авторскими правами, ср. Файлы в каталоге LICENSES на полные лицензионные тексты. В частности, Mathsat доступен только для целей исследования и оценки (см. LICENSES/LicenseRef-MathSAT-CPAchecker.txt ), поэтому обязательно используйте другой решатель SMT, если это необходимо. Обратите внимание, что, хотя программа GPL распределяется вместе с CPachecker, CPachecker отделен от этой программы и, следовательно, не в условиях GPL.

Подготовить программы для проверки Cpachecker

Все программы должны предварительно обработать препроцессор C, то есть они не могут содержать директивы #define и #include . Вы можете включить предварительную обработку внутри Cpachecker, указав --preprocess в командной строке. Несколько файлов C могут быть предоставлены и будут связаны вместе и проверены как одна программа (экспериментальная функция).

Cpachecker может проанализировать и анализировать большую подмножество (GNU) c. Если анализ не удается для вашей программы, отправьте отчет по адресу [email protected].

Проверка программы с CPachecker

1. Выберите файл исходного кода, который вы хотите проверить. Если вы используете свою собственную программу, не забудьте предварительно обработать ее, как упомянуто выше. Пример: doc/examples/example.c или doc/examples/example_bug.c Хорошим источником для более примеров программ является репозиторий SV-Benchmarks, который используется, например, Международной конкуренцией по проверке программного обеспечения.

2. При желании: если вы хотите выбрать определенные анализы, такие как анализ предикатов, укажите файл конфигурации. Этот файл определяет, например, какие CPA используются. Стандартные файлы конфигурации можно найти в config/ . Если вам не нужна конкретный анализ, мы рекомендуем конфигурацию по умолчанию CPachecker. Тем не менее, обратите внимание, что если вы находитесь в MacOS, вам необходимо предоставить специально считанные двоичные файлы Mathsat для работы по умолчанию (или использовать Docker, чтобы запустить версию Cpachecker Linux). Конфигурация CPachecker объяснена в doc/Configuration.md .

3. Выберите файл спецификации (вам может не понадобиться для некоторых конфигураций). Стандартные конфигурации используют config/specification/default.spc в качестве спецификации по умолчанию. С помощью этого CPachecker будет искать метки с именем ERROR (нечувствительный к случаю) и утверждения в файле исходного кода. Другие примеры для спецификаций можно найти в config/specification/ в каталоге CPachecker.

4. Выполнить bin/cpachecker [ --config <CONFIG_FILE> ] [ --spec <SPEC_FILE> ] <SOURCE_FILE> Дополнительные аргументы командной строки описаны в doc/Configuration.md . Чтобы использовать конфигурацию по умолчанию CPachecker, передайте только исходный файл: bin/cpachecker doc/examples/example.c . Конкретный анализ (например, k-индукция) может быть выбран, например, с помощью bin/cpachecker --config/kInduction.properties doc/examples/example.c или эквивалентный аббревиатура bin/cpachecker --kInduction doc/examples/example.c . Java 17 или позже необходим. Если это не на вашем пути, вам нужно указать его в переменной среды Java. Пример: export JAVA=/usr/lib/jvm/java-17-openjdk-amd64/bin/java для 64bit openjdk 17 на Ubuntu.

   Обратите внимание, что не все конфигурации анализа доступны для MacOS, потому что мы не отправляем двоичные файлы для решателей SMT для этой платформы. Вам нужно либо создать соответствующие двоичные файлы самостоятельно, либо использовать менее мощные анализы, которые работают с решателями на основе Java, например, на конфигурации по умолчанию Cpachecker: --predicateAnalysis-linear --option solver.solver=SMTInterpol конечно, вы также можете использовать такие решения для выполнения линового версии Cpachecker.

   Если вы установили Cpachecker с использованием Docker, приведенная выше командная строка примеров будет выглядеть следующим образом: docker run -v $(pwd):/workdir -u $UID:$GID sosylab/cpachecker /cpachecker/doc/examples/example.c Эта команда делает текущий каталог доступным в контейнере, так что, как и в текущем указывании, а также для того, чтобы в соответствии с этим, как и в текущем указывании, в соответствии с тем, что он находится на примере, чтобы он был примером, чтобы он был примером, чтобы это было примером, чтобы он был примером, чтобы он был примером. Cpachecker. Выходные файлы CPachecker будут размещены в ./output/ .

5. В дополнение к выходу консоли, интерактивный отчет HTML генерируется в output/ , либо с именованным Report.html (для результата True) или Counterexample.*.html (для результата false). Откройте эти файлы в браузере, чтобы просмотреть результат анализа CPachecker (см. doc/Report.md )

Есть также дополнительные выходные файлы в output/ :

• ARG.dot : визуализация дерева абстрактного достижения (формат Graphviz)
• cfa*.dot : Визуализация автомата потока управления (формат Graphviz)
• reached.dot .: Визуализация автомата потока управления с абстрактными состояниями, визуализированными сверху (формат Graphviz)
• coverage.info : Информация о покрытии (аналогичная информации инструментам тестирования) в формате Gcov Используйте следующую командную строку для генерации отчета HTML в качестве output/index.html : genhtml output/coverage.info --output-directory output --legend
• Counterexample.*.txt : путь через программу, которая приводит к ошибке
• Counterexample.*.assignment.txt : назначения для всех переменных на пути ошибки.
• Counterexample.*.harness.c : тестовый жгут, который может воспроизводить путь ошибки посредством выполнения теста. См. DOC/TURANTIONS/TEST-HARNESS.MD для примера использования.
• predmap.txt : предикаты, используемые в результате анализа предикатов для доказывания безопасности программы
• reached.txt .
• Statistics.txt : Статистика времени (также может быть напечатана в консоли с --stats )

Обратите внимание, что не все эти файлы будут доступны для всех конфигураций. Также некоторые из этих файлов создаются только в том случае, если обнаружена ошибка (или наоборот). Cpachecker будет перезаписать файлы в этом каталоге!

Проверка программы с CPA-WiteS2test

Вы можете проверить свидетелей нарушения с помощью CPA-Vitys2test, который является частью CPachecker.

1. Для этого вам нужен свидетель нарушения, файл спецификации, который соответствует свидетельству нарушения, и файл исходного кода, который соответствует свидетельству нарушения.

2. Чтобы подтвердить свидетеля, выполните следующую команду:

    bin/cpa-witness2test --witness <WITNESS_FILE> --spec <SPEC_FILE> <SOURCE_FILE>`
   

   Аргументы административной командной строки просматриваются с помощью bin/cpa-witness2test -h .

3. После завершения, и если свидетель нарушения успешно подтвержден, вывод консоли показывает Verification result: FALSE . В дополнение к выходу консоли, CPA-WITINGS2Test также создает output/*.harness.c . Этот файл может быть составлен против исходного файла для создания исполняемого теста, который отражает свидетель нарушения.

Обратите внимание, что если свидетель нарушения не содержит достаточного количества информации для создания исполняемого теста, результат проверки будет ERROR , а выход консоли будет содержать следующую строку: Could not export a test harness, some test-vector values are missing.