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 для аргумента опции.
