Skip to content
  • Robbert Krebbers's avatar
    mem_force no longer flattens the entire subobject for "unsigned char" · 5644d68f
    Robbert Krebbers authored
    addresses.
    
    The operation "mem_force Γ m a" used to apply the identify function to
    pricisely the object "a", even in case "a" is an "unsigned char" address
    refering to an individual byte. This caused the ctree substructure of the
    entire subobject to disappear and had the undesired effect that:
    
      mem_force Γ a m ⊑{Γ,true@Γm} m
    
    failed to hold (i.e. unused reads cannot be removed).
    5644d68f