Выполните проверку Polyspace ® для кода, который успешно создается с помощью компилятора. После успешного создания кода настройте проект Polyspace одним из следующих способов:
Выполните трассировку системы сборки.
Программа создает проект на основе сценариев сборки. Он задает соответствующие опции анализа Polyspace для эмуляции опций построения.
Если не удается отследить систему построения, создайте проект Polyspace вручную.
Добавьте свои источники и включите их в проект. При необходимости измените параметры анализа по умолчанию.
Дополнительные сведения см. в разделе Настройка и выполнение анализа.
При настройке проекта вручную чаще возникает следующая проблема.
Перед проверкой и обнаружением ошибок времени выполнения Polyspace компилирует код и обнаруживает ошибки компиляции и связывания. Даже если ваш код успешно создается с помощью компилятора, вы все равно получаете ошибки компиляции с помощью Polyspace.
Этап компиляции
Сбой компиляции
Компилятор Polyspace строго следует стандарту C или C++. Посмотрите C standard version (-c-version) и C++ standard version (-cpp-version). Если компилятор допускает отклонение от стандартного, компиляция Polyspace, использующая параметры по умолчанию, не сможет эмулировать компилятор. Например, компилятор может разрешить использование определенных ключевых слов, отличных от ANSI ®, которые не распознаются Полиспейсом по умолчанию.
Чтобы гарантировать отсутствие определенных ошибок времени выполнения, компиляция Polyspace по умолчанию строго соответствует стандарту. Определенные компиляторы допускают определенные отклонения от этого стандарта и следуют внутренним алгоритмам для компиляции кода. Без явного знания поведения компилятора Polyspace не может учесть эти отклонения. Учет этих отклонений через некоторые произвольные внутренние алгоритмы может скомпрометировать результаты окончательного анализа, если алгоритм Polyspace не соответствует алгоритму компилятора.
Проверьте сообщение об ошибке, вызвавшей сбой компиляции, и проверьте, можно ли определить некоторое отклонение от стандарта. Сообщение об ошибке содержит номер строки, вызвавшей сбой компиляции. При выполнении проверки из пользовательского интерфейса можно щелкнуть сообщение об ошибке и перейти к соответствующей строке кода.
Измените параметры анализа, чтобы более точно эмулировать компилятор.
Если включить Compilation Assistant и запустить проверку в интерфейсе пользователя, для большинства ошибок компиляции на панели Output Summary появятся предложения, которые можно применить одним щелчком мыши. См. раздел Просмотр информации об ошибках при остановке анализа.
В противном случае можно вручную скорректировать параметры анализа. Чтобы преодолеть проблемы компиляции, используйте эти опции.
| Выбор | Цель |
|---|---|
| Параметры цели и компилятора | Используя эти предопределенные опции, можно задать поведение компилятора напрямую и обойти известные отклонения от стандарта. Часто, настройка |
С помощью этих опций иногда можно обойти неизвестные отклонения от стандарта. Например, эти параметры можно использовать для замены нераспознанных ключевых слов из предварительно обработанного кода точно совпадающими распознанными ключевыми словами или для их полного удаления. Поскольку исходный код не изменяется, параметры позволяют обойти ошибки компиляции, сохранив исходный код нетронутым. |
Сведения о конкретных типах ошибок компиляции см. в разделе Устранение ошибок компиляции.
Если вы не можете устранить ошибку компиляции, обратитесь в службу технической поддержки MathWorks ® и укажите имя компилятора для улучшения поддержки. Обратитесь в службу технической поддержки по вопросам работы Polyspace.
Даже в случае успешной компиляции одной единицы компиляции возникает ошибка связывания из-за несоответствия между двумя единицами компиляции. Например, одна и та же функция определяется двумя способами. .c файлы с различными типами аргументов или возвращаемых значений.
Общие цепочки инструментов компиляции не хранят информацию о прототипах функций во время процесса связывания. Поэтому, несмотря на эти типы ошибок связывания, построение не приводит к сбою. Чтобы гарантировать отсутствие определенных ошибок времени выполнения, 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 стандартных библиотечных функций. Если переопределение компилятора точно соответствует спецификациям стандартных библиотечных функций, результаты проверки по-прежнему применимы для кода, скомпилированного с компилятором.
При обнаружении ошибки:
Определение макроса __polyspace_no_ в проекте. Например, если возникает ошибка из-за конфликта с определением function_namesprintf функция, определение макроса __polyspace_no_sprintf. Сведения об определении макросов см. в разделе Preprocessor definitions (-D).
Макрос отключает использование реализаций Polyspace стандартной библиотечной функции. Программное обеспечение блокирует стандартную библиотечную функцию, как и любую другую неопределенную функцию. Ошибка отсутствует из-за несоответствия подписи реализациям Polyspace.
Обратитесь в службу технической поддержки MathWorks и предоставьте сведения о компиляторе.
Для некоторых стандартных библиотечных функций, таких как assertи функции выделения памяти, такие как malloc и calloc, Polyspace продолжает использовать собственные реализации, даже если переопределить функцию и предоставить тело функции. Дополнительные сведения см. в разделе Ошибки из функций утверждения или распределения памяти.