Support Limitations and Considerations for S-Functions and C/C++ Code

Enabling S-Functions in Simulink Design Verifier

Simulink^® Design Verifier™ supports test case generation for code generated with Embedded Coder^®. Simulink Design Verifier also supports error detection, test case generation, and property proving for S-Functions that:

The Legacy Code Tool generates, with def.Options.supportCoverageAndDesignVerifier set to true.
The S-Function Builder generates, with Enable support for Design Verifier selected on the Build Info tab of the S-Function Builder dialog box.
The function slcovmex compiles, with the option -sldv passed to the function when compiling the S-function.

For more information on the three approaches, see How to Create C MEX S-Functions.

Support Limitations for S-Functions and C/C++ Code

Simulink Design Verifier does not support S-Functions or C/C++ code containing:
- Continuous states. Simulink Design Verifier does not analyze such code.
- Zero-crossing functions. Simulink Design Verifier ignores such code during analysis.
- Constants that describe INF or NaN objects. Simulink Design Verifier considers such code as containing floating-point overflow errors. Although Simulink Design Verifier analysis cannot determine the type of overflow error for such cases, the analysis can determine which lines of code introduce the incompatibility. Polyspace^® can provide more information on why your code contains floating-point overflow errors.
- Volatile constants and variables. Simulink Design Verifier supports volatile variables and constants through stubbing. A model that contains volatile variables or constants is compatible and can be analyzed, but the analysis may result in objectives undecided due to stubbing.
You must specify that the signal elements entering the ports of S-Functions compiled with slcovmex are contiguous. Use the SimStruct function ssSetInputPortRequiredContiguous.

Simulink Design Verifier supports the following design errors for S-Function and C/C++ code:

Dead logic including active logic.
Array out of bounds. This includes pointer out of bounds in case of C/C++.
Division-by-Zero.

Handle Volatile Variables as Normal Variables

Simulink Design Verifier allows the option for volatile variables to be stubbed or handled as normal variables. When you select the Ignore the volatile qualifier parameter, volatile elements will be treated in the same as the non-volatile elements. Deselecting the Ignore the volatile qualifier will revert to the previous behavior of stubbing access to volatile elements.

Considerations for Enabling S-Functions and C/C++ Code in Simulink Design Verifier

When performing property proving or test generation analysis for models with enabled S-Functions or C/C++ code generated with Embedded Coder, Simulink Design Verifier assumes that the code contains no run-time errors. If the code contains run-time errors such as division by zero, access to non-initialized variables or array out of bounds, the property proving or test generation analysis can produce incorrect results. Code that has been checked by Polyspace and is free of run-time errors provide correct results in Simulink Design Verifier analysis.
To avoid incorrect results that are produced due to run-time errors, perform design error detection analysis first, and then perform property proving or test generation analysis.
If Simulink Design Verifier cannot determine the size of arrays in your code (for instance for arrays that are dynamically allocated with non-constant size), Simulink Design Verifier assumes an upper bound for the array. Ensure that the given upper bound is appropriate.
If you do not enable Simulink Design Verifier support for an S-function, Simulink Design Verifier stubs the S-function. With S-function support enabled, Simulink Design Verifier analyzed the content of the S-function to get more detailed information. Sometimes, Simulink Design Verifier internally stubs the S-function. Internal stubs can be the result of different C/C++ constructs, such as:
- Calls to library functions (the library function is replaced by a stub).
- Complex pointer operations.
- Casts to or from incompatible or unknown pointer types.
Models containing such constructs are labeled Partially compatible.

Source Code Protection

To analyze the contents of an S-function, information about the implementation of the S-function, including information derived from the source code, are stored within the shared object. Although this information is not directly accessible to users, consider disabling Simulink Design Verifier support for S-Functions in models that are released externally if the S-Functions contain sensitive source code.