Exponenta Banner

Запустите Polyspace на коде AUTOSAR с консервативными предположениями

Эта тема описывает компонентно-ориентированный подход к проверке кода AUTOSAR с Polyspace. Для аналитического подхода интегрирования смотрите, Выбирают Between Component-Based и Integration Analysis of AUTOSAR Code with Polyspace.

Polyspace® для AUTOSAR запускает статический анализ программы реализации кода компонентов программного обеспечения AUTOSAR. Анализ ищет возможные ошибки времени выполнения или несоответствие с техническими требованиями в AUTOSAR XML (ARXML).

Анализ по умолчанию принимает что аргументы указателя к runnables и указателям, возвращенным в Rte_ функции не являются ПУСТЫМИ. Например, в этом примере, анализ принимает тот aInput, aOutput и aOut2 не являются ПУСТЫМИ. Условия, которые сравнивают эти аргументы с NULL_PTR всегда оценивайте ко лжи и кажитесь серыми в результатах. Здесь, NULL_PTR макрос, который представляет NULL.

iOperations_ApplicationError foo(
    Rte_Instance const self,
    app_Array_2_n320to320ConstRef aInput,
    app_Array_2_n320to320Ref aOutput,
    app_Enum001Ref aOut2)
{
    iOperations_ApplicationError rc = E_NOT_OK;
    if (aInput==NULL_PTR) {
        rc = RTE_E_iOperations_ERR001;
    } else if (aOutput==NULL_PTR) {
        rc = 43;
    } else {
        unsigned int i=0;
        for (;i<2U;++i) {
            aOutput[1-i] = aInput[i];
        }
        if (aOut2!=NULL_PTR) {
            *aOut2 = 1234;
            rc = RTE_E_OK;
        }
    }
    return rc;
}

Вы можете хотеть запустить консервативный анализ где аргументы указателя к runnables и указателям, возвращенным в Rte_ функции могут быть с пустым знаком. Консервативный анализ помогает вам определить, приняли ли вы меры против возможности указателей с пустым знаком в вашем выполнимом.

Чтобы позволить возможность указателей с пустым знаком из внешних источников, не задайте макро-RTE_PTR2USERCODE_SAFE. Чтобы не задать макрос, используйте один из этих методов в зависимости от того, как вы запускаете анализ.

  • В пользовательском интерфейсе Polyspace макрос задан с опцией Preprocessor definitions (-D). Удалите макрос из этой опции и переместите в опцию Disabled preprocessor definitions (-U).

  • Если вы запускаетесь polyspace-autosar в командной строке используйте опцию -U не задавать макрос.

Если вы отключаете макрос, вы больше не видите недостижимый код при сравнении аргументов указателей с runnables против NULL. Чтобы видеть эффект этого макроса, запустите консервативный анализ Polyspace демонстрационных файлов в polyspaceroot\help\toolbox\codeprover\examples\polyspace_autosar.

Смотрите также

Похожие темы

Документация Polyspace Code Prover

Поддержка