How Polyspace Analysis of Generated Code Works

When you generate code from a Simulink^® model, the generated code can contain these components:

initialize() functions that run before the simulation starts.
terminate() functions that run after the simulation ends.
step() functions that run in a loop to perform the simulation.

Additionally, the generated code might have a placeholder main() function that contains calls to the above. You might edit the placeholder main() to fit your deployment purposes. For more information about the main generated by Embedded Coder^®, see Main Program (Embedded Coder).

When you run Polyspace^® on generated code, Polyspace gathers this information from your code:

initialize() functions
terminate() functions
step() functions
List of parameter variables
List of input variables

When you run Code Prover, the software uses this information to generate a separate main() function to facilitate the analysis. Regardless of the presence of the generated placeholder main(), Polyspace uses its own main() function that performs these tasks:

Initializes parameters by using the Polyspace option Parameters (-variables-written-before-loop).
Calls initialization functions by using the option Initialization functions (-functions-called-before-loop).
Initializes inputs using the option Inputs (-variables-written-in-loop).
Calls the step function in a loop by using the option Step functions (-functions-called-in-loop). By default, Polyspace assumes that the step function might be called an arbitrary number of times in the loop. To specify the number of iterations in the loop for a more precise Code Prover analysis, use the option -main-generator-bounded-loop.
Calls the terminate function by using the option Termination functions (-functions-called-after-loop).

The Polyspace generated main function might have this structure:

init parameters    \\ -variables-written-before-loop
init_fct()	         \\ -functions-called-before-loop
  while(random){        \\ start main loop with one or more iterations
  init inputs      \\ -variables-written-in-loop
  step_fct()       \\ -functions-called-in-loop
}
terminate_fct()    \\ -functions-called-after-loop

For C++ code generated with Embedded Coder, the initialize(), step(), and terminate() functions and associated variables are either class members or have global scope.