发送短信: Two for the Price of One: Lifting Separation Logic Assertions