The following options can be set to assist you with this:
1.(Before 17a) "Optimize large static initializers" (internal option name : -no-fold)
When variables are defined with huge static initialisation, scaling problems may occur during the compilation phase. This option approximates the initialisation of array types of integer, floating point, and char types (included string) if needed. It can speed up the analysis, but may decrease precision for some applications
Default : Option not set.
Example Shell Script Entry :
(before R2013b) polyspace-c -no-fold ...
(since R2013b) polyspace-code-prover-nodesktop -no-fold ...
2. "Precision Level" (-O)
This option specifies the precision level to be used. It provides higher selectivity in exchange for more analysis time, therefore making results review more efficient and hence making bugs in the code easier to isolate. It does so by specifying the algorithms used to model the program state space during analysis.
It is recommended that analyses should begin with a low precision. Red errors and grey code can then be addressed before re-launching Polyspace using this option, applying a precision level as described below.
Benefits - A higher precision level contributes to a higher selectivity rate, making results review more efficient and hence making bugs in the code easier to isolate. - A higher precision level also means higher analysis time
-O0 corresponds to static interval analysis.
-O1 corresponds to complex polyhedron model of domain values.
-O2 corresponds to more complex algorithms to closely model domain values (a mixed approach with integer lattices and complex polyhedrons).
-O3 is only suitable for small code. For such codes, the resulting selectivity might reach high values such as 98%, resulting in a very long analysis time, such as an hour per 1000 lines of code.
Default: -O2
3. (before 17a) "Reduce task complexity" (-lightweight-thread-model) for multitasking verifications.
Allows to simplify task modeling inside Polyspace Code Prover.
Other options are available as "extra options" (to be specified in "Other Polyspace options) since R2013b or regular options for earlier versions:
4. "Depth of verification inside structure" (-k-limiting)
This is a scaling option to limits the depth of analysis into nested structures during pointer analysis.
This option is only available for Polyspace C and C++.
Default: There is no fixed limit.
Example Shell Script Entry:
polyspace-code-prover-nodesktop -k-limiting 1 ...
In this example above, analysis will be precise to only one level of nesting.
3. -respect-types-in-fields
This is a scaling option, designed to help process complex code. When it is applied, Polyspace assumes that structure fields not declared as containing pointers are never used for holding pointer values. This option should only be used with Type-safe C/C++ code, when it does not cause a loss of precision. See also -respect-types-in-globals
Default: Polyspace assumes that structure fields may contain pointer values.
4. -respect-type-in-globals
This is a scaling option, designed to help process complex code. When it is applied, Polyspace assumes that global variables not declared as containing pointers are never used for holding pointer values. This option should only be used with Type-safe C/C++ code, when it does not cause a loss of precision. See also -respect-types-in-fields.
Default: Polyspace assumes that global variables may contain pointer values.
Please note that when facing out-of-memory problems, the recommandation is to decrease the size of the application given to Polyspace.
This is explained in this document:
