Polyspace error when trying to obtain complexity metrics with auto generated code

I am trying to run an analysis on auto-generated code from another tool and using Polyspace Code Prover (R2015a) as I need to determine the maximum call depth level within the code.

After completing about 46% of Software Safety Analysis on Level 0, I get the following error message and the run is terminated - "Error: The process with PID 7560 (child process of PID 9732) could not be terminated".

Before the error message I also get the warning message "Verified code seems quite complex."

This error has repeated 3 times now however contains different PID number each time and the below are the last few lines from the run log:

"Calling TASKKILL command on Polyspace process with PID 6184..." ERROR: The process with PID 7560 (child process of PID 9732) could not be terminated. Reason: The process cannot terminate itself. SUCCESS: The process with PID 9396 (child process of PID 6184) has been terminated. SUCCESS: The process with PID 9732 (child process of PID 6184) has been terminated.

I could not find any info on these error messages online therefore any help would be appreciated.

Regards, Bibek

Answer 1

[Alexandre De Barros]

Hi Bibek,

This is something that can occur in R2015a. Could you try with the latest version, R2015b?

Best regards,

Alexandre

[Bibek Paudel]

Hi Alexandre,

Thank you for the reply.

I will try with R2015b and get back to you.

Kind Regards,

Bibek

Answer 2

[Bibek Paudel]

Hi Alexandre,

With R2015b, I got failure even before reaching Level 0 Analysis. After running for 24 hours, during C2IL process, it timed out however this process only took couple of hours with R2015a. Below are the last few lines from the run log.

***** C to intermediate language translation - 6.5.2.1 (P_GAA3) took 84146.58real, 84146.58u + 0s (114.47gc) Warning: The C2IL translation has been stopped by timeout (after 86400 seconds).

-------------------------------------------------------------------

--- Verifier has encountered an internal error. ---

--- Please contact your technical support. ---

---------------------------------------------------------------

Failure at: Thu Oct 15 08:38:55 2015

[Alexandre De Barros]

Hi Bibek,

This requires more investigation.

Can you contact the support? And please attach the logs of 15a and 15b : they can help to know more.

Alex