proposition: Lemma BV_sizeof_pos: forall t m, access_mode t = By_value m -> BV_sizeof t > 0.
proof: Proof. intros. erewrite BV_sizeof_size_chunk by eauto. apply size_chunk_pos. 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