After running Polyspace (Code Prover), in the "Reasons for Unchecked Code" section, if the progress of the "code operations" is not 100%, I would like to know how the percenta

After running Polyspace (Code Prover), in the "Reasons for Unchecked Code" section, if the progress of the "code operations" is not 100%, I would like to know how the percentage of "code operations" is calculated and what specifically "code operations" refer to.

Answer 1

[Dheeraj]

Hi 新宝,

I understand you seek to know how the "Code Operations" column which is seen in the Polyspace Code Prover Dashboard.

Code operations is the percentage of elementary operations in verified functions that are checked for run-time errors. Hence, can be calculated as follows,

(number of code operations reached/ total number of code operations present in software) * 100

You could refer to the below MATLAB documentation for more details about the Polyspace Code Prover Dashboard:

https://www.mathworks.com/help/codeprover/ug/dashboard.html?searchHighlight=%22Code%20operations%22&s_tid=srchtitle_support_results_9_%2522Code%2520operations%2522#mw_f6db7b68-2fdc-4965-bbb1-795759aac22b

Thank you.

[新宝]

Hi Dheeraj, I have read your response, but I still have some questions about this part.

What is the definition of code operations, and how are the 'number of code operations reached' and 'total number of code operations present in software' calculated? Is the diagram below an explanation of code operations? It seems to suggest that code operations refer to checks on the code, as the definition of a variable like 'int x' doesn't require any checks, so it doesn't count as a code operation. However, the line 'x = 1 / x; x = x + 1;' undergoes five checks such as 'overflow check', so the total number of code operations is five. But in reality, only the 'Non-initialized local variable' check was performed, so the number of code operations reached is one. The percentage of code operations is then 20%. Is my understanding correct?