MATLAB: Do I get an unjustified error message with critical sections

criticalpolyspacePolyspace Code ProverPolyspace Code Prover Serversection

We explain why Polyspace gives a wrong error message about a limitation with critical sections.

Best Answer

There is a documented limitation with critical sections when the beginning and end of a critical section are not in the same block. The message will occur on the C to Il phase and will look like:
...
** C to intermediate language translation - 12 (P_G)
----------------------------------------------------------------------
Limitation: Beginning then end of critical section must be in same block : file.function
|This construction is not supported by PolySpace Verifier.
|The computation has been halted.
But this limitation is raised if the parameters of the functions defining the beginning and end of the critical section are pointers to an object.
Ex:
        MyType variable;
        CriticalRegion_Enter(&variable);
       // some code 
        CriticalRegion_Exit(&variable);
The workaround is to use a temporary variable as the argument:
        MyType variable;
        MyType * p_variable;
        p_variable = &variable;
        CriticalRegion_Enter(p_variable);
       // some code 
        CriticalRegion_Exit(p_variable);
Related Question