Avoid Red Checks in Unreachable Code When Using C++ STL Containers

Issue

By default, Code Prover analyzes the implementations of methods in STL containers such as std::map, std::vector, and std::list. This analysis can be time-consuming and sometimes lead to issues such as red checks in otherwise unreachable code.

For instance, you might see issues such as a red check in an if statement branch, even if the if condition is always false in the current context (and the code in the if statement can never execute or trigger a run-time error).

Possible Solutions

Enable a Code Prover analysis mode that does not analyze implementations of methods in STL containers. Specify the value stdlibcxx for the option Libraries used (-library).

In this mode, the analysis uses smart stubs for methods from C++ Standard Library containers even if their implementations are available. The smart stubs emulate STL container methods only as much as needed for the verification. In exchange, the stubs work around the problem of long analysis times or red checks in unreachable code. For the full list of containers that are supported with smart stubs, see Libraries used (-library).

Note that all methods of a container might not be stubbed when you use this option. A message in the analysis log states how many methods were stubbed. With each release of Polyspace^® Code Prover™, more container methods are covered by the smart stubbing.