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