Inconsistent inferred annotated file generation during WPI iterations causing non-termination

[iamsanjaymalakar]

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

benmouh_repro.zip

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.