CPAchecker analízis nem fut le Windows-on

Question

Sziasztok!

A labor 1 feladatkiírás alapján (a cpa.sh helyett cpa.bat-ot futtatom) a CPAChecker-t a példakódon lefuttatva az alábbi kimenetet kapom, váratlan kivételek miatt nem tud lefutni a verifikáció. Találkozott valaki hasonló problémával?

C:\Users\Dani\Documents\BME\swsv\CPAchecker-1.7-windows>scripts\cpa.bat -config config\default.properties -spec config\specification\default.spc doc\examples\example.c
CPAchecker 1.7 (Java HotSpot(TM) 64-Bit Server VM 1.8.0_161) started (CPAchecker.run, INFO)

Using Restarting Algorithm (CoreComponentsFactory.createAlgorithm, INFO)

Starting analysis ... (CPAchecker.runAlgorithm, INFO)

Loading analysis 1 from file config\kInduction.properties ... (RestartAlgorithm.run, INFO)

Starting analysis 1 ... (RestartAlgorithm.run, INFO)

Warning: Analysis 1 not completed. (An unexpected exception occured) (ParallelAlgorithm.handleFutureResults, WARNING)

Ignoring restart configuration 'config\valueAnalysis-predicateAnalysis-bam-rec.properties' because condition if-recursive did not match. (RestartAlgorithm.run, INFO)

Ignoring restart configuration 'config\bddAnalysis-concurrency.properties' because condition if-concurrent did not match. (RestartAlgorithm.run, INFO)

No further configuration available. (RestartAlgorithm.run, INFO)

Stopping analysis ... (CPAchecker.runAlgorithm, INFO)

Analysis not completed: there are still states to be processed. (CPAchecker.analyzeResult, WARNING)

Cannot print statistics for config\components\kInduction\kInduction.properties because it is still running. (Analysis1:ParallelAlgorithm$ParallelAlgorithmStatistics.printSubStatistics, INFO)

Cannot print statistics for config\components\invariantGeneration-no-out.properties because it is still running. (Analysis1:ParallelAlgorithm$ParallelAlgorithmStatistics.printSubStatistics, INFO)

Verification result: UNKNOWN, incomplete analysis.
More details about the verification run can be found in the directory ".\output".
Graphical representation included in the file ".\output\Report.html".

Answer 1

Érdemes ilyenkor beállítani a részletes naplózást:

• a config\default.properties végére kell beírni, hogy log.level = ALL
• lefuttatni újra, és a html report-ot megnézve a log résznél látszik a teljes log, és itt ki lehet keresni a kivételt

Másnál az volt a probléma, hogy a solver bináris fájljai hiányoztak. A CPAChecker readme-je írta is ezt:

However, note that if you are on Windows or MacOS you need to provide specifically-compiled MathSAT binaries for this configuration to work.

A MathSAT innen érhető el: http://mathsat.fbk.eu/download.html

De mi alapvetően Linuxról próbáltuk a CPAChecker-t.