What to do when facing "scaling behavior" with Polyspace Code Prover?

When using the Polyspace Code Prover, I encountered the following different scenarios:

i) An "out of memory" error, or a "crash" for example:

**** Software Safety Analysis Level 0 - 61 (P_ILOI)
**** Software Safety Analysis Level 0 - 61 (P_ILOI) took 2.13real, 1.92u + 0.03s
**** Software Safety Analysis Level 0 - 62 (P_ENVT)
Fatal error: out of memory.

or:

****** Software Safety Analysis Level 1 - 3.1.2494 (* analyzing MyFunction)exception SML_Pre_Basis.Fail("failure in job")(Fail: failure in job) raised.raised at: Raised at Parallel.really_apply_in_parallel_on_sccs in file "../../verifier/kernel_api/IL/parallel.sml", line 531, characters 32-33

ii) A 24-hour timeout (timeout after 86400 seconds), for example:

***** Software Safety Analysis Level 0 - 32.2 (P_I1)
Warning: The analysis has been stopped by timeout (after 86400 seconds).
Maximum Memory Usage: 1720 MB

or:

4.5.2.1.1 (Loading) took 0.27real, 0.21u + 0.05s (0.1gc)
[64928 -> 192289]
Warning: The C2IL translation has been stopped by timeout (after 86400 seconds).

iii) An analysis showing no progress.

These seem to be symptoms of a "scaling behavior" with the Polyspace Code Prover. What are some solutions to these behaviors?

Answer 1

[MathWorks Support Team]

Please find the attached PDF file for a guide on scaling behaviors for Polyspace Code Prover, which includes explanations on how to identify scaling behaviors, and the solutions against these different scenarios.