checker-framework
checker-framework copied to clipboard
Inconsistent inferred annotated file generation during WPI iterations causing non-termination
Description
We are experiencing a non-termination issue where the Checker Framework inconsistently generates output files during Whole Program Inference (WPI). Specifically, the framework alternates between generating annotated files in one iteration and generating no files in the subsequent iteration. This pattern affects the 'build/whole-program-inference' directory, where output files are expected in each iteration but are absent in even-numbered iterations.
This is causing non-termination in the WPI script.
Diff between two iterations:
Only in ../dataset/june2020_dataset_copy/url7a69e77641_benmouh_MySgbd_tgz-pJ8-Demo_CheckRowNumJ8/wpi-iterations/temp1: Demo
Only in ../dataset/june2020_dataset_copy/url7a69e77641_benmouh_MySgbd_tgz-pJ8-Demo_CheckRowNumJ8/wpi-iterations/temp1: org
Test Project
Steps to Reproduce
- Run the Whole Program Inference (WPI) using the provided script and project.
- In the zip folder, there is one shell script named
wpi.sh
and one folder containing the project's source code. - Run the script with the project path as an argument:
./wpi.sh url7a69e77641_benmouh_MySgbd_tgz-pJ8-Demo_CheckRowNumJ8
- Check the
build/whole-program-inference
directory after each iteration. - After each iteration, the inference outputs are stored in the project's root folder, in the
wpi-iterations
directory. You can also check the inference results for each iteration there.