-
Léon Gondelman authored
The effects now must satisfy the following invariants: 1. Every region in eff_writes, eff_taints, and eff_covers must occur in the type of some variable in eff_reads. 2. Both eff_taints and eff_covers are subsets of eff_writes. 3. eff_covers and eff_resets are disjoint. 4. Every region in eff_writes is either in eff_covers or is stale (according to Ity.reg_r_stale) and forbidden for the later use. Also, this commit rewrites Ity.eff_assign and Ity.eff_strong (renamed now to eff_reset_overwritten) to handle correctly parallel assignments.
faf9a2be