Non-termination of WPI on NJR Benchmarks for Nullness Checker Annotations

Tested on CF versions 3.34.0 and 3.42.0

I executed WPI on NJR benchmarks to infer annotations for Nullness Checker. And observed that in the majority of benchmarks, WPI consistently performs over a thousand to two thousands iterations without terminating.

I extracted one benchmark out of 288 existing benchmarks and made a repository with all my scripts to run the WPI available here. For your convenience, I stored the result of the first hundred iteration.diff as well in iterations directory for a quick view of the contents in the iteration diffs.

The repository is ready to use, after downloading checker framework jar (details in the repo readme), please run wpi/run_wpi.py which will execute wpi on the benchmarks in dataset.

Please let me know if I made a mistake in the configurations or you need more information to resolve this.

Best,

Nima

Start with the linked wpi/run_wpi.py script and its README instructions, using the benchmark in the dataset directory. Compare the generated iteration.diff files with the supplied iterations directory to confirm the non-termination behavior. Done means reproducing the issue and identifying the cause or a concrete path to termination.