The joinImpl in the IDEInstInteractionAnalysis does not correctly model a join-lattice for the edge values l_t.
This PR fixes this issue and also fixes the subsequent errors that showed up after the joinImpl-fix.
Concretely, the edge-functions have been changed that were created when generating a fact from zero. In this case, the attached edge-value should not depend on the value attached to zero.
Furthermore, the kill-or-replace edge function has been identified as "constant" and adapted accordingly.
The
joinImplin theIDEInstInteractionAnalysisdoes not correctly model a join-lattice for the edge valuesl_t.This PR fixes this issue and also fixes the subsequent errors that showed up after the joinImpl-fix. Concretely, the edge-functions have been changed that were created when generating a fact from zero. In this case, the attached edge-value should not depend on the value attached to zero. Furthermore, the kill-or-replace edge function has been identified as "constant" and adapted accordingly.
699 Should be merged first.