-main-generator-bounded-loop

Generate a main that calls functions in a loop with a specific number of iterations

Since R2022a

Syntax

-main-generator-bounded-loop num

Description

Use this option only for C code generated from MATLAB^® code or Simulink^® models.

-main-generator-bounded-loop num generates a main function that calls certain functions in a loop with num iterations. This option allows you to bound the number of calls to the step function in generated code.

When you analyze code generated from Simulink models in the Simulink editor, the analysis first generates a main that calls step functions from the generated code in a loop. This main function acts as the entry point of the subsequent Polyspace^® analysis. Alternatively, to analyze generated code from outside Simulink, you can set equivalent main generation options:

You can use the option Verify model generated code (-main-generator) to generate a main function.
You can use the option Step functions (-functions-called-in-loop) to specify which functions to call in a loop from the generated main.

However, the number of loop iterations is unspecified and the analysis assumes a wide range of possibilities for this number. If you want the step functions to be called a specific number of times, use the option -main-generator-bounded-loop with a positive number as argument.

Bounding the number of calls to the step function:

Reduces the number of unproven orange checks. For instance, operations that might otherwise overflow a buffer when performed an unspecified number of times remain within the bounds of the buffer.
Allows you to prove certain properties of the system after a certain number of simulation steps are completed.

If you are running an analysis from the user interface (Polyspace desktop products only), on the Configuration pane, you can enter this option in the Other field. See Other. To open the Configuration pane from the Simulink editor, see Configure Polyspace Options in Simulink.

Examples

Bounding Number of Calls to Step Function to Reduce Unproven Results (Orange Checks)

You can use this option to reduce the number of unproven orange checks when analyzing generated code with Polyspace Code Prover™.

Consider the following code that could be generated from a Simulink model:

int i;
int array[100];

void init() {
  i = 0;
}

void step() {
  if (i>20)
    array[i] = -1;
  else
    array[i] = 1;
  i++;
}

If you verify this code with regular main-generation options using init as the initialization function and step as the step function, you can see an orange Out of bounds array index check on the first array access in step. Since the function step is called an unspecified number of times, the variable i can be greater than 100, leading to a possible array access outside bounds.

Suppose you know that the function can be called only 100 times. For instance, the Simulink model might be run for at most 100 simulation steps. In this case, generate a main function that calls the function step in a loop with 100 iterations:

Code Prover:

polyspace-code-prover -sources file.c -main-generator -functions-called-before-loop init -functions-called-in-loop custom=step -main-generator-bounded-loop 100

Code Prover Server:

polyspace-code-prover-server -sources file.c -main-generator -functions-called-before-loop init -functions-called-in-loop custom=step -main-generator-bounded-loop 100

The orange Out of bounds array index check on the first array access turns green.

Bounding Number of Calls to Step Function to Prove Behavior Change

You can also use this option to check for a behavior after the step function in the generated code is called a certain number of times. For instance, suppose that a subsystem in a Simulink model changes behavior after a certain number of steps. The step function in the generated code must also show this change of behavior after being called a certain number of times. If you want to verify that the behavior change indeed takes place, you can do the following:

Use the option -main-generator-bounded-loop to call the step function in a loop with a specific number of iterations. The number of iterations must correspond to the number of steps after which you expect the subsystem to change behavior. For instance, if the subsystem is expected to change behavior after 400s and the simulation step size is one second, the behavior change is expected to show after 400 iterations.
Check for the expected behavior after the loop runs are completed by using a custom function:
1. Write a function that checks for the expected changed behavior using assert statements (assertions).
2. Add the file containing this function as an additional source using the Simulink configuration parameter Enable additional file list.
3. Call this function after the loop using the option Termination functions (-functions-called-after-loop).
Code Prover can verify whether the assertions in your custom function are true using the User assertion check. If the assertions are always false, Bug Finder can also detect the issue using the Assertion check.

Version History

Introduced in R2022a