proposition: Lemma exp_mapsto_precise: forall sh t p, precise (EX v: val, mapsto sh t p v).
proof: Proof. intros. unfold mapsto. destruct (access_mode t); try apply @exp_FF_precise with (H := algPreciseSepLog _). destruct (type_is_volatile t); try apply @exp_FF_precise with (H := algPreciseSepLog _). destruct p; try apply @exp_FF_precise with (H := algPreciseSepLog _). if_tac. + apply derives_precise with (exp (fun v0 => address_mapsto m v0 sh (b, Ptrofs.unsigned i))); [| apply address_mapsto__precise]. apply exp_left; intro v. apply orp_left. - apply andp_left2, (exp_right v). auto. - apply andp_left2; auto. + apply derives_precise with (nonlock_permission_bytes sh (b, Ptrofs.unsigned i) (size_chunk m)). - apply exp_left; intro. apply andp_left2. auto. - apply nonlock_permission_bytes_precise. Qed.
imports: VST.msl.seplog VST.msl.log_normalize CertiGraph.msl_ext.seplog CertiGraph.msl_ext.log_normalize VST.veric.base VST.veric.rmaps VST.veric.rmaps_lemmas VST.veric.compcert_rmaps VST.veric.slice VST.veric.res_predicates VST.veric.tycontext VST.veric.expr VST.veric.address_conflict VST.veric.seplog VST.veric.mapsto_memory_block VST.msl.msl_standard VST.msl.alg_seplog CertiGraph.msl_ext.alg_seplog CertiGraph.veric_ext.res_predicates