Ensure lazy byte-code transformation always works correctly in the verification phase under model-checking mode

JetBrains / lincheck

Framework for testing concurrent data structures

Mozilla Public License 2.0

576 stars 33 forks source link

Ensure lazy byte-code transformation always works correctly in the verification phase under model-checking mode #323

Open eupp opened 4 months ago

eupp commented 2 months ago

Quote from @ndkoval about this issue from the discussion of #316 :

By the way, I also think we currently might have a bug with the model-checking mode, as the lazy transformation might not work in the verification phase, as we do not analyze anything in this phase, and, therefore, we do not ensure that the code dependencies are transformed.