Свяжитесь с технической поддержкой о проблемах с рабочим Polyspace

Чтобы связаться с MathWorks® Technical Support, используйте эту страницу. Вам нужны вход в систему MathWorks Account и пароль. Для более быстрого благоприятного поворота с проблемой в Polyspace®, помимо запрошенной системной информации, предоставляют соответствующий код, который воспроизводит проблему или файл журнала верификации.

Предоставьте информацию о системе

При вводе запрос поддержки, предоставляете следующую информацию о системе:

  • Аппаратная конфигурация

  • Операционная система

  • Polyspace и номера лицензии MATLAB®

  • Определенные номера версий для Продуктов polyspace

  • Установленные закрашенные фигуры Отчета об ошибках

Чтобы получить вашу конфигурационную информацию, выполнить одно из следующих действий:

  • В пользовательском интерфейсе Polyspace выберите Help> About.

  • В командной строке запустите следующую команду, заменив polyspaceroot с вашей папкой установки Polyspace:

    • UNIX®polyspaceroot/polyspace/bin/polyspace-code-prover-ver

    • Windows®polyspaceroot\polyspace\bin\polyspace-code-prover-ver

Предоставьте информацию о проблеме

В зависимости от проблемы обеспечьте соответствующие артефакты, чтобы помочь Технической поддержке изучить и воспроизвести проблему.

Ошибки компиляции

Если вы сталкиваетесь с проблемами компиляции со своим проектом, смотрите Ошибки компиляции Поиска и устранения неисправностей. Если у вас все еще есть проблемы, свяжитесь с технической поддержкой со следующей информацией:

  • Аналитический журнал.

    Аналитический журнал является текстовым файлом, сгенерированным в вашей папке результатов и названном Polyspace_version_projectдатаВремяжурнал. Это содержит сообщение об ошибке, опции, используемые для анализа и другой релевантной информации.

  • Исходные файлы связаны с ошибкой компиляции или полной папкой результатов, если это возможно.

    Если вы не можете обеспечить исходные файлы:

    • Попытайтесь предоставить снимок экрана раздела исходного кода, который вызывает проблему компиляции.

    • Попытайтесь воспроизвести проблему с различным кодом. Предоставьте тот код технической поддержке.

Ошибки в создании проекта от систем сборки

Если вы сталкиваетесь с ошибками в создании проекта от вашей системы сборки, смотрите Создание Проекта Поиска и устранения неисправностей.

Если у вас все еще есть проблемы, свяжитесь с технической поддержкой с отладочной информацией. Обеспечить отладочную информацию:

  1. Запущенный polyspace-configure в командной строке с опцией -easy-debug. Например:

    polyspace-configure options -easy-debug pathToFolder buildCommand

    Здесь:

    • options список polyspace-configure опции, которые вы обычно используете.

    • buildCommand команда сборки, что вы используете, например, make.

    • pathToFolder папка, где вы хотите сохранить отладочную информацию, например, C:\Temp\BuildLogs. После polyspace-configure запуститесь, обеспеченный путь содержит заархивированный файл, заканчивающийся pscfg-output.zip. Заархивированный файл содержит отладочную информацию только и не содержит исходные файлы, прослеженные в сборке.

    Убедитесь, что вы не используете опцию -verbose или -silent после -easy-debug. Эти опции уменьшают или изменяют регистрируемую информацию и могут сделать отладку трудного.

  2. Отправьте этот заархивированный файл, заканчивающийся pscfg-output.zip к MathWorks Technical Support для дальнейшей отладки.

Можно также создать заархивированный файл с отладочной информацией во время каждого polyspace-configure запуститесь путем создания переменной окружения PS_CONFIGURE_OPTIONS и устанавливание его значения к:

-easy-debug pathToFolder
где pathToFolder папка, где вы хотите сохранить отладочную информацию.

Результат верификации

Если вы испытываете затруднения при понимании результата, смотрите Результаты Polyspace Code Prover Access (Polyspace Code Prover Access).

Если вы все еще испытываете затруднения при понимании результата, свяжитесь с технической поддержкой со следующей информацией:

  • Аналитический журнал.

    Аналитический журнал является текстовым файлом, сгенерированным в вашей папке результатов и названном Polyspace_version_projectдатаВремяжурнал. Это содержит опции, используемые для анализа и другой релевантной информации.

  • Исходные файлы связаны с результатом или полной папкой результатов, если это возможно.

    Если вы не можете обеспечить исходные файлы:

    • Попытка предоставляет снимок экрана соответствующего исходного кода от панели Source в пользовательском интерфейсе Polyspace.

    • Попытайтесь воспроизвести проблему с различным кодом. Предоставьте тот код технической поддержке.