Stack check by Code Prover

Hi all,

My first post here...

We are working on an embedded project, bare metal. The customer asks for a analysis of the stack and suggests using static analysis tool. We have Code Prover and we know it can do this stack check, but we are not in need at the moment to perform a whole Code Prover analysis. Can we request Code Prover to execute just the stack check? By removing all of the code prover checks, I'm in the hope of getting fewer reds if none at all and having the info I need more easily and faster.

Thanks

Answer 1

[Anirban]

It is possible to calculate all code metrics other than stack size in the earlier stages of a Code Prover analysis. You have to enable the option Calculate code metrics and set the option Verification level to Source Compliance Checking.

The stack analysis actually computes an accurate picture of the function call hierarchy taking into account red checks (run-time errors) and gray checks (unreachable code). In other words:

• If a function call is not reachable at run-time, it is not taken into account.
• If there is a red-check (definite run-time error), the analysis does not compute the stack size. The idea is: definite run-time errors would typically cause a crash anyway, so function calls following the errors wont be executed anyway. Hence, the errors need to be fixed.

Because of this reason, the stack size computation happens in the later part of the analysis. This computation is richer than a superficial stack size computation that would be based on the apparent function call hierarchy without checking if the calls actually can happen at run-time.

As a result, you cannot separate the run-time error detection from the stack size computation. In other words, you cannot just perform the early stages of the analysis and get the stack size.

[Victor Garcia Santos]

I was afraid of this. Our idea was to avoid the effort needed to setup properly the Code Prover project. To get a software complete analysis solution implies lots of preparation and effort which right now we cannot afford. Anyway, thanks for the deep answer, appreciated.