Hi Hong,
A Code Prover analysis makes several passes on your code. If the analysis stops after pass1 has begun, you can restart from pass1 instead of from the beginning.
To achieve this, there are a couple of undocumented options that are required. You have to use the option -keep-all-files in the current run (so if you have not used it already for the current power cut, you might be out of luck but see a possible solution at the end). Then if there is a power cut or something and the analysis stops, you can check the log file of the analysis for lines like Beginning Software Safety Analysis Level 0 or Beginning Software Safety Analysis Level 1. Start from the end of the log file so that you can see which is the level that began last.
Say, the level that began last is level 1. You can restart analysis from that level with the option -from pass1. The option -from takes the same arguments as the documented option -to.
There are two caveats:
- -keep-all-files can result in a large number of intermediate files being stored. If you use this option, make sure that you monitor the size of the result folder and you are okay with the disk space used.
- Both -keep-all-files and -from are command-line-only options. If you are running analysis from the Polyspace user interface, you can enter them in the field Other.
There is a chance that for an abnormal shutdown, -from will work even without you having used -keep-all-files previously. Since you have not used used -keep-all-files in the current run that stopped, you can try just using a -from from whichever pass the analysis stopped at, and see if it works.
