Запуск Polyspace® верификация кода, который успешно строится с помощью компилятора. После успешного создания кода настройте проект Polyspace одним из следующих способов:
Проследите систему сборки.
Программа создает проект из ваших скриптов сборки. Он устанавливает соответствующие опции анализа Polyspace, чтобы эмулировать опции сборки.
Если вы не можете проследить систему сборки, создайте проект Polyspace вручную.
Добавьте свои источники и включения в проект. При необходимости измените опции анализа по умолчанию.
Дополнительные сведения см. в разделе Настройка и запуск анализа.
Следующая проблема возникает чаще, если вручную настроить проект.
Перед верификацией и обнаружением ошибок времени выполнения Polyspace компилирует ваш код и обнаруживает ошибки компиляции и связывания. Даже если ваш код успешно строится с помощью компилятора, вы все равно получаете ошибки компиляции с Polyspace.
Фаза компиляции
Отказ компиляции
Компилятор Polyspace строго следует стандарту C или C++. См. C standard version (-c-version) и C++ standard version (-cpp-version). Если ваш компилятор допускает отклонение от Стандарта, компиляция Polyspace, которая использует опции по умолчанию, не может эмулировать ваш компилятор. Например, ваш компилятор может разрешить определенные не-ANSI® ключевые слова, которые Polyspace не распознает по умолчанию.
Чтобы гарантировать отсутствие определенных ошибок времени выполнения, компиляция Polyspace по умолчанию строго соответствует стандарту. Конкретные компиляторы допускают определенные отклонения от этого стандарта и следуют внутренним алгоритмам, чтобы скомпилировать ваш код. Без явных знаний о поведении компилятора, Polyspace не может принять эти отклонения. Принятие этих отклонений через некоторые произвольные внутренние алгоритмы может скомпрометировать окончательные результаты анализа, если алгоритм Polyspace не совпадает с алгоритмом вашего компилятора.
Проверьте сообщение об ошибке, вызвавшей отказ компиляции, и проверьте, можно ли идентифицировать некоторое отклонение от стандарта. В сообщении об ошибке отображается номер линии, вызвавшей отказ компиляции. При запуске верификации из пользовательского интерфейса можно щелкнуть сообщение об ошибке и перейти к соответствующей строке кода.
Измените опции анализа, чтобы лучше эмулировать компилятор.
Если вы включите Compilation Assistant и запустите верификацию в пользовательском интерфейсе, для большинства ошибок компиляции получите предложения на панели Output Summary, которые можно применить одним нажатием кнопки. См. «Просмотр информации об ошибках при остановке анализа».
В противном случае можно вручную настроить опции анализа. Чтобы получить проблемы прошедшей компиляции, используйте эти опции.
| Опция | Цель |
|---|---|
| Опции Target и Compiler | Используя эти предопределенные опции, можно задать поведение компилятора непосредственно и обойти известные отклонения от стандарта. Часто установка |
Используя эти опции, можно иногда обойти неизвестные отклонения от стандарта. Например, можно использовать эти опции, чтобы заменить непризнанные ключевые слова из предварительно обработанного кода тесно соответствующими распознанными ключевыми словами или удалить их полностью. Поскольку вы не меняете свой исходный код, опции позволяют вам работать с ошибками компиляции, сохраняя исходный код нетронутым. |
Для определенных типов ошибок компиляции смотрите Поиск и устранение ошибок компиляции.
Если вы не можете решить ошибку компиляции, обратитесь в MathWorks® Техническая поддержка и укажите имя компилятора для лучшей поддержки. Обратитесь в службу технической поддержки о проблемах с выполняемым Polyspace.
Даже если один модуль компиляции успешно компилируется, вы получите ошибку связывания из-за несоответствия между двумя модулями компиляции. Например, вы задаете ту же функцию в двух .c файлы с различными типами аргументов или возвращаемых типов.
Общие цепочки инструментов компиляции не хранят информацию о прототипах функций в процессе связывания. Поэтому, несмотря на эти типы ошибок связывания, сборка не проваливается. Чтобы гарантировать отсутствие определенных ошибок времени выполнения, Polyspace не продолжает анализ, когда возникают такие ошибки связи.
Исправьте ошибки связывания, которые обнаруживает Polyspace. Даже если процесс сборки допускает эти ошибки, у вас могут быть неожиданные результаты во время выполнения. Например, если в коде существуют два определения функций с одним и тем же именем, но конфликтующими прототипами, при вызове функции результат может оказаться неожиданным.
Когда происходит ошибка связи, в сообщении об ошибке указывается местоположение в вашем файле, где не удается выполнить компиляцию Polyspace. Предыдущие предупреждающие сообщения показывают местоположение конфликтов, которые приводят к ошибке связывания. Используя номера линий в этих сообщениях (или нажав на сообщения, если вы запускаете анализ из интерфейса пользователя), можно перейти к местоположению конфликтов в коде.
Например, в этих сообщениях компиляция прекращается из-за конфликтующих типов возврата функций. Отказ происходит на линии 5 в file2.c при вызове функции. Предыдущие предупреждающие сообщения для линии 1 в file1.c и линия 1 в file2.c показать местоположения, в которых происходят конфликты.
Для определенных типов ошибок связи смотрите Поиск и устранение ошибок компиляции.
Polyspace использует собственную реализацию стандартных библиотечных функций для более эффективной верификации. Если ваш компилятор пересматривает и переопределяет стандартную функцию библиотеки, можно получить предупреждение или ошибку при вызове функции.
Ошибка подразумевает, что Polyspace нашел редекларацию, но не может найти тело вашей переопределенной функции библиотеки. Верификация продолжает использовать реализацию функции Polyspace, но предоставляет предупреждение. Если ваша переопределенная функция имеет отличную сигнатуру от обычной сигнатуры функции, верификация останавливается с ошибкой.
Предупреждения и ошибки этого типа часто относятся к файлу __polyspace__stdstubs.c. Этот файл содержит прототипы для реализации Polyspace стандартных библиотечных функций. Файл расположен в polyspaceroot\ polyspace\verifier\cxx\polyspace _ stubs\polyspaceroot
Если вы знаете расположение файла, который содержит тело переопределенной стандартной функции библиотеки, добавьте файл к своей верификации. Для получения дополнительной информации см. «Ошибки из конфликтов с файлами заголовков Polyspace».
Если у вас нет доступного тела функции:
Если вы видите предупреждение этого типа, можно игнорировать предупреждение. Результаты верификации основаны на реализациях Polyspace стандартных библиотечных функций. Если ваше переопределение компилятора тесно соответствует стандартным спецификациям библиотечных функций, результаты верификации все еще применяются для кода, скомпилированного с помощью компилятора.
Если вы видите ошибку:
Задайте макрос __ полипространство _ в вашем проекте. Например, если ошибка возникает из-за конфликта с определением no _ function_namesprintf function, задайте макрос __polyspace_no_sprintf. Для получения информации о том, как задать макросы, смотрите Preprocessor definitions (-D).
Макрос отключает использование реализаций Polyspace стандартной функции библиотеки. Программа заглушает стандартную функцию библиотеки, как и любую другую неопределенную функцию. У вас нет ошибки из-за несоответствия подписей с реализациями Polyspace.
Обратитесь в службу технической поддержки MathWorks и предоставьте информацию о вашем компиляторе.
Для некоторых стандартных функций библиотеки, таких как assert, и такие функции выделения памяти, как malloc и callocPolyspace продолжает использовать собственные реализации, даже если переопределить функцию и предоставить тело функции. Для получения дополнительной информации смотрите Ошибки из Assertion или Функции выделения памяти.
