diff options
Diffstat (limited to 'common/Memtype.v')
| -rw-r--r-- | common/Memtype.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/common/Memtype.v b/common/Memtype.v index b7d953f..a39daf4 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -414,6 +414,7 @@ Axiom load_store_similar: forall chunk m1 b ofs v m2, store chunk m1 b ofs v = Some m2 -> forall chunk', size_chunk chunk' = size_chunk chunk -> + align_chunk chunk' <= align_chunk chunk -> exists v', load chunk' m2 b ofs = Some v' /\ decode_encode_val v chunk chunk' v'. Axiom load_store_same: |