Анализ останавливается с сообщением об ошибке, которое ссылается на такие шаблоны классов, как map
и vector
из библиотеки стандартных шаблонов.
Часто в сообщении об ошибке указывается, что либо оператор не может быть найден, либо более одного оператора соответствуют заданным операндам.
Polyspace® программное обеспечение обеспечивает эффективную реализацию всех шаблонов классов из библиотеки стандартных шаблонов (STL). Если ваш исходный код пересмотрит шаблоны, анализ может быть остановлен с сообщением об ошибке.
Чтобы использовать собственные реализации шаблонов из библиотеки стандартных шаблонов:
Отключите реализации Polyspace, используя опцию No STL stubs (-no-stl-stubs)
.
Добавьте папки, содержащие ваши реализации, к верификации.
В пользовательском интерфейсе добавьте папку к своему проекту.
Для получения дополнительной информации см. раздел «Добавление исходных файлов для анализа» в интерфейсе пользователя Polyspace.
В командной строке используйте флаг -I
с polyspace-code-prover
команда.
Для получения дополнительной информации смотрите -I
.
Примечание
Использование собственных определений шаблонов может вызвать другие ошибки компиляции и связывания.