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

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

В этом разделе описывается компонентный подход к проверке кода AUTOSAR с помощью Polyspace. Подход к интеграционному анализу см. в разделе Выбор между компонентным и интеграционным анализом кода AUTOSAR с Polyspace.

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

Анализ по умолчанию предполагает, что аргументы указателя на выполняемые объекты и указатели возвращены из Rte_ функции не являются NULL. Например, в этом примере анализ предполагает, что aInput, aOutput и aOut2 не являются NULL. Условия, сравнивающие эти аргументы с 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;
}

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

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

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

См. также

polyspace-autosar

Связанные темы

• Запустить Polyspace для кода AUTOSAR