Skip to content

Internal cpachecker engine

Henrik Wachowitz requested to merge internal-cpachecker-engine into main

This merge request introduces the internal CPAchecker Engine. Instead of invoking a new process, CPAchecker is executed directly inside the current JVM.

The heavy lifting is performed by the CpacheckerRunner class. This class itself is Runnable and encapsulates the invocation of the CPAchecker run method. The Factory building this class sets up the logManager, shutdownManager and parses the configuration into a CPAchecker compatible format. Similar to the process runs, the InternalJVMRun launches and monitors the CpacheckerRunner instance.

My preliminary testing already showed, that for a simple task (safe.c with Value Analysis) the execution time can be reduced from ~2s to 0.2s hinting that we were successful in mitigation JVM startup costs.

TODOs:

  • Add more tests
  • Fix Pipeline
Edited by Henrik Wachowitz

Merge request reports