Polyspace® использует собственную реализацию стандартных библиотечных функций для более эффективного анализа. Если вы переопределяете стандартную функцию библиотеки и предоставляете тело функции Polyspace, анализ использует ваше определение.
Однако для некоторых стандартных библиотечных функций Polyspace продолжает использовать собственные реализации, даже если переопределить функцию и предоставить тело функции. Функции включают в себя assert и такие функции выделения памяти, как malloc, calloc и alloca.
Вы видите предупреждение, например:
Body of routine "malloc" was discarded.
Эти функции имеют особое значение для анализа Polyspace, поэтому вам не разрешено их переопределять. Для образца:
Реализация Polyspace malloc функция позволяет программному обеспечению проверять, выделена ли память с помощью malloc освобождается позже.
Реализация Polyspace assert используется внутри для улучшения анализа.
Если вы особенно не хотите использовать свои собственные переопределения, игнорируйте предупреждение. Результаты анализа основаны на реализациях Polyspace стандартной функции библиотеки, которые следуют исходным спецификациям функции.
Если вы хотите, чтобы ваши собственные переопределения использовались и вы уверены, что ваша переопределенная функция ведет себя так же, как и исходная функция, переименуйте функции. Переименовать функцию можно только для целей анализа с помощью опции Preprocessor definitions (-D). Например, чтобы переименовать функцию malloc на my_malloc, использовать malloc=my_malloc для аргумента опции.
