Main Content

Run Polyspace on AUTOSAR Code with Conservative Assumptions

This topic describes a component-based approach to verifying AUTOSAR code with Polyspace. For an integration analysis approach, see Choose Between Component-Based and Integration Analysis of AUTOSAR Code with Polyspace.

Polyspace® for AUTOSAR runs static program analysis on code implementation of AUTOSAR software components. The analysis looks for possible run-time errors or mismatch with specifications in the AUTOSAR XML (ARXML).

The default analysis assumes that pointer arguments to runnables and pointers returned from Rte_ functions are not NULL. For instance, in this example, the analysis assumes that aInput, aOutput and aOut2 are not NULL. The conditions that compare these arguments against NULL_PTR always evaluate to false and appear gray in the results. Here, NULL_PTR is a macro that represents 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;
}

You might want to run a conservative analysis where pointer arguments to runnables and pointers returned from Rte_ functions can be NULL-valued. The conservative analysis helps you determine if you have guarded against the possibility of NULL-valued pointers within your runnable.

To allow the possibility of NULL-valued pointers from external sources, undefine the macro RTE_PTR2USERCODE_SAFE. To undefine a macro, use one of these methods depending on how you run the analysis.

If you disable the macro, you no longer see unreachable code when comparing pointers arguments to runnables against NULL. To see the effect of this macro, run a conservative Polyspace analysis on the demo files in polyspaceroot\polyspace\examples\doc_cxx\polyspace_autosar.

See Also

Related Topics