Library compcert.common.Memory
This file develops the memory model that is used in the dynamic
semantics of all the languages used in the compiler.
It defines a type mem of memory states, the following 4 basic
operations over memory states, and their properties:
- load: read a memory chunk at a given address;
- store: store a memory chunk at a given address;
- alloc: allocate a fresh memory block;
- free: invalidate a memory block.
Require Import Zwf.
Require Import Axioms.
Require Import Coqlib.
Require Intv.
Require Import Maps.
Require Archi.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Export Memdata.
Require Export Memtype.
CompCertX:test-compcert-param-memory
We moved the concrete implementation of the memory model to Memimpl.
However, we keep this file because other files that do
Require Import Memory may want to use the hints.
Thanks to Xavier Leroy's bright idea of Require Export Memtype,
the operations and properties of the memory model can still be used.
Hint Resolve
Mem.valid_not_valid_diff
Mem.perm_implies
Mem.perm_cur
Mem.perm_max
Mem.perm_valid_block
Mem.range_perm_implies
Mem.range_perm_cur
Mem.range_perm_max
Mem.valid_access_implies
Mem.valid_access_valid_block
Mem.valid_access_perm
Mem.valid_access_load
Mem.load_valid_access
Mem.loadbytes_range_perm
Mem.valid_access_store
Mem.perm_store_1
Mem.perm_store_2
Mem.nextblock_store
Mem.store_valid_block_1
Mem.store_valid_block_2
Mem.store_valid_access_1
Mem.store_valid_access_2
Mem.store_valid_access_3
Mem.storebytes_range_perm
Mem.perm_storebytes_1
Mem.perm_storebytes_2
Mem.storebytes_valid_access_1
Mem.storebytes_valid_access_2
Mem.nextblock_storebytes
Mem.storebytes_valid_block_1
Mem.storebytes_valid_block_2
Mem.nextblock_alloc
Mem.alloc_result
Mem.valid_block_alloc
Mem.fresh_block_alloc
Mem.valid_new_block
Mem.perm_alloc_1
Mem.perm_alloc_2
Mem.perm_alloc_3
Mem.perm_alloc_4
Mem.perm_alloc_inv
Mem.valid_access_alloc_other
Mem.valid_access_alloc_same
Mem.valid_access_alloc_inv
Mem.range_perm_free
Mem.free_range_perm
Mem.nextblock_free
Mem.valid_block_free_1
Mem.valid_block_free_2
Mem.perm_free_1
Mem.perm_free_2
Mem.perm_free_3
Mem.valid_access_free_1
Mem.valid_access_free_2
Mem.valid_access_free_inv_1
Mem.valid_access_free_inv_2
Mem.unchanged_on_refl
: mem.
CompCertX:test-compcert-param-extcall Due to the fact that MemoryModel
is not necessarily directly available in the context (it may have to be
found through CompilerConfiguration), we need to make sure eauto can use
typeclass instance resolution.