Generate stubs for Embedded Coder lookup tables (-stub-embedded-coder-lookup-table-functions)

Stub autogenerated functions that use lookup tables and model them more precisely

Description

This option is available only for model-generated code. The option is relevant only if you generate code from a Simulink^® model that uses Lookup Table blocks using MathWorks^® code generation products.

Specify that the verification must stub autogenerated functions that use certain kinds of lookup tables in their body. Polyspace^® supports stubbing lookup table functions that use linear interpolation and do not allow linear extrapolation. That is, the result of using the lookup table must always lie between the lower and upper bounds of the table.

Set Option

If you are running verification from Simulink, use the option Stub lookup tables in Simulink Configuration Parameters, which performs the same task.

User interface (desktop products only): In your Polyspace project configuration, the option is on the Inputs & Stubbing node.

Command line and options file: Use the option -stub-embedded-coder-lookup-table-functions. See Command-Line Information.

Why Use This Option

If you use this option, the verification is more precise and has fewer orange checks. The verification of lookup table functions is usually imprecise. The software has to make certain assumptions about these functions. To avoid missing a run-time error, the verification assumes that the result of using the lookup table is within the full range allowed by the result data type. This assumption can cause many unproven results (orange checks) when a lookup table function is called. By using this option, you narrow down the assumption. For functions that use lookup tables with linear interpolation and no extrapolation, the result is at least within the bounds of the table.

The option is relevant only if your model has Lookup Table blocks. In the generated code, the functions corresponding to Lookup Table blocks also use lookup tables. The function names follow specific conventions. The verification uses the naming conventions to identify if the lookup tables in the functions use linear interpolation and no extrapolation. The verification then replaces such functions with stubs for more precise verification.

Settings

On (default)

For autogenerated functions that use lookup tables with linear interpolation and no extrapolation, the verification:

• Does not check for run-time errors in the function body.

• Calls a function stub instead of the actual function at the function call sites. The stub ensures that the result of using the lookup table is within the bounds of the table. Polyspace stubs these lookup table functions:

  • Linear interpolation lookup table functions

  • Extrapolation lookup table functions that clips the output

To identify the lookup table in the function, the verification uses the function name. In your analysis results, you see that the function is not analyzed. If you place your cursor on the function name, you see the following message:

    Function has been recognized as an Embedded Coder Lookup-Table function.
    It was stubbed by Polyspace to increase precision.
    Unset the -stub-embedded-coder-lookup-table-functions option to analyze the code below.

Off

The verification does not stub autogenerated functions that use lookup tables.

Tips

• The option applies to only autogenerated functions. If you integrate your own C/C++ S-Function using lookup tables with the model, these functions do not follow the naming conventions for autogenerated functions. The option does not cause them to be stubbed. If you want the same behavior for your handwritten lookup table functions as the autogenerated functions, use the option -code-behavior-specifications and map your function to the __ps_lookup_table_clip function.

• If you run verification from Simulink, the option is on by default. For certification purposes, if you want your verification tool to be independent of the code generation tool, turn off the option.

• This option does not stub a lookup table that uses linear extrapolation.

Command-Line Information

Parameter: -stub-embedded-coder-lookup-table-functions

Default: On

Example (Code Prover): polyspace-code-prover -sources file_name -stub-embedded-coder-lookup-table-functions

Example (Code Prover Server): polyspace-code-prover-server -sources file_name -stub-embedded-coder-lookup-table-functions

Version History

Introduced in R2016b