Polyspace® верификация может иногда остановиться в фазе компиляции или связывания по следующим причинам:
Компилятор Polyspace строго следует стандарту C или C++ (в зависимости от вашего выбора компилятора). См. Стандарт языка C/C + +, используемый в анализе Polyspace. Если ваш компилятор допускает отклонение от Стандарта, компиляция Polyspace с использованием опций по умолчанию не может эмулировать ваш компилятор.
Компилятор объявляет стандартные функции библиотеки с аргументами или возвращаемыми типами, отличными от стандартных типов. Если вы также не предоставляете определение функции, для эффективной верификации Polyspace использует свои собственные определения стандартных библиотечных функций, которые имеют обычный прототип. Несоответствие типов вызывает ошибку связывания.
Можно легко обойти ошибки компиляции и стандартные функции библиотеки. Чтобы обойти ошибки, вы обычно задаете определенные опции анализа. В некоторых случаях, возможно, вам придется добавить несколько линии к своему коду. Для образца:
Чтобы лучше эмулировать поведение компилятора, задайте опции Target & Compiler. Если вы все еще столкнулись с ошибками компиляции, вам, возможно, придется удалить или заменить некоторые непризнанные ключевые слова с помощью опции Preprocessor definitions (-D). Однако опция допускает только простое замещение строки другой строкой. Для более сложных замен, возможно, придется добавить #define операторы в ваш код.
Чтобы избежать ошибок от упорства стандартных библиотечных функций, вам, возможно, придется #define некоторые специфичные для Polyspace макросы так, что Polyspace не использует собственного определения стандартных библиотечных функций.
Вместо добавления этих изменений к оригинальному коду создайте одну polyspace.h файл, содержащий все изменения. Используйте опцию Include (-include) для принудительного включения polyspace.h файл во всех исходных файлах, подлежащих верификации.
Преимущества этого подхода включают:
Выявление ошибок происходит намного быстрее, так как оно будет обнаружено во время компиляции, а не в ссылке или последующих фазах.
Нет необходимости изменять исходные исходные файлы.
Файл автоматически включается в качестве самого первого файла в исходном .c файлы.
Файл можно повторно использовать для других проектов, разработанных в том же окружении.
Это пример файла, который можно использовать с опцией Include (-include).
// The file may include (say) a standard include file implicitly
// included by the cross compiler
#include <stdlib.h>
#include "another_file.h"
// Workarounds for compilation errors
#define far
#define at(x)
// Workarounds for errors due to redefining standard library functions
#define POLYSPACE_NO_STANDARD_STUBS // use this flag to prevent the
//automatic stubbing of std functions
#define __polyspace_no_sscanf
#define __polyspace_no_fgetc
void sscanf(int, char, char, char, char, char);
void fgetc(void);