Klever

Note, that you will need to do a minor refactoring of Klever components to support new formats updated in BenchExec. And doing this you will likely ignore VerifierCloud scheduler that work with verification tasks and results a bit differently. VerifierCloud is currently broken and you are unable to do testing until supporting the newest format of tasks for the cloud. Ideally it is better to solve these two tasks together.

Ilja Zakharov wrote:

Note, that you will need to do a minor refactoring of Klever components to support new formats updated in BenchExec. And doing this you will likely ignore VerifierCloud scheduler that work with verification tasks and results a bit differently. VerifierCloud is currently broken and you are unable to do testing until supporting the newest format of tasks for the cloud. Ideally it is better to solve these two tasks together.

According to documentation it seems that the old format should be okay. This issue is for getting rid of redundant LDV-BenchExec primarily. Other issues should be fixed separately. BTW, there is already #9507 that touches exactly topics you talked about. There you said that using old scripts for accessing VerifierCloud is pretty well, so, this is not such the awful issue.

So, my plan is the following. First, switch to BenchExec 1.18 without any changes in the benchmark format (this issue, perhaps we will make some small tuning). Then, switch to the new format and to the new VerifierCloud scripts (#9507).