На фазе компиляции программное обеспечение отображает предупреждение или сообщение об ошибке о неизвестном прототипе функции.
the prototype for function 'myfunc' is unknown
Для определения типов данных для таких функций Polyspace следует стандарту C99 (ISO/IEC 9899:1999, глава 6.5.2.2: Вызовы).
Тип возврата принимается следующим int.
Количество и тип аргументов определяются первым вызовом функции. Например, если функция принимает одну double аргумент в первом вызове, для последующих вызовов программное обеспечение принимает один double аргумент. Если вы передаете int аргумент в последующем вызове, преобразование из int на double происходит.
Во время фазы связывания, если происходит несоответствие между количеством или типом аргументов или типом возврата в разных модулях компиляции, верификация останавливается. Для получения дополнительной информации см. раздел «Конфликтующие объявления в различных модулях перевода».
Указанный исходный код не содержит прототипа функции. Например, функция объявлена в файле включения, который Polyspace не может найти.
Если вы #include-d файл включения в исходный код, но не добавил его к своему проекту Polyspace, вы видите предыдущее предупреждение:
Warning: could not find include file "my_include.h"
Поиск объявления функции в вашем исходном репозитории.
Если вы находите объявление функции в файле включения, добавьте папку, которая содержит файл включения.
В пользовательском интерфейсе десктопных продуктов Polyspace добавьте папку к своему проекту.
Для получения дополнительной информации см. раздел «Добавление исходных файлов для анализа» в интерфейсе пользователя Polyspace.
В командной строке используйте флаг -I с polyspace-code-prover команда.
Для получения дополнительной информации смотрите -I.
