Code Prover show a new Orange warning but I can't find any relationship between changed source code and this new warning.

Good morning!

I have a problem with Code Prover. When I run Code Prover with new source code (base on project of old source code), Code Prover show an new Illegally dereferenced pointer warning but I can't find any relationship between changed source code and this new warning. Does it happen because I missing some changed source code or it happen because verification engine of Code Prover? I also compare both source code but the change not effect to this warning. (both is not a defect)

Answer 1

[Anirban]

Hi,

It is difficult to answer without the complete project (or at least the changes made to the project). It is possible that the change you made is indirectly related to the new orange warning.

You have to search for all references to ult_tmp_buf and then see if you can trace the issue to your changes. Here are some steps you can take in the Polyspace user interface to investigate this warning further: Review and Fix Illegally Dereferenced Pointer Checks.

Polyspace checks do depend on each other in a very specific way. If an error occurs on a specific execution path, the execution path is eliminated from the remainder of the verification. Once you understand this logic, you can trace how a check in a part of code you did not touch can depend on a check in the code that you changed. See more details here: Code Prover Analysis Following Red and Orange Checks.

But ultimately, the new warning should be traceable to the changes you made in the code (in the sense that some variable in the code you changed must be indirectly related to ult_tmp_buf). If the release version of Code Prover and the verification options stay the same, any new result should be completely traceable to the changes made in the source code.

[Tran Thang]

Hi Anirban,

Whether the result of Code Prover is depend on the power of Computer which run it?