Иногда проверка Polyspace ® может остановиться на этапе компиляции или связывания по следующим причинам:
Компилятор Polyspace строго следует стандарту C или C++ (в зависимости от выбора компилятора). См. Стандарт языка C/C + +, используемый в анализе пространства. Если компилятор допускает отклонение от стандартного, компиляция Polyspace с параметрами по умолчанию не может эмулировать компилятор.
Компилятор объявляет стандартные библиотечные функции с типами аргументов или возвращаемых значений, отличными от стандартных типов. Если вы также не предоставите определение функции, для эффективной проверки Polyspace использует собственные определения стандартных библиотечных функций, которые имеют обычный прототип. Несоответствие типов приводит к ошибке связывания.
Можно легко обойти ошибки функции компиляции и стандартной библиотеки. Для обхода ошибок обычно задаются определенные опции анализа. В некоторых случаях может потребоваться добавить несколько строк в код. Например:
Чтобы более точно эмулировать поведение компилятора, необходимо задать параметры «Цель и компилятор». При наличии ошибок компиляции может потребоваться удалить или заменить некоторые нераспознанные ключевые слова с помощью опции 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);