summaryrefslogtreecommitdiff
path: root/backend/Mach.v
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-01-11 11:57:02 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-01-11 11:57:02 +0000
commitbb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc (patch)
tree3efa5cb51e9bb3edc935f42dbd630fce9a170804 /backend/Mach.v
parentcd2449aabe7b259b0fdb8aaa2af65c2b8957ab32 (diff)
- Added alignment constraints to memory loads and stores.
- In Cminor and below, removed pointer validity check in semantics of comparisons, so that evaluation of expressions is independent of memory state. - In Cminor and below, removed "alloc" instruction. - Cleaned up commented-away parts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Mach.v')
-rw-r--r--backend/Mach.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/backend/Mach.v b/backend/Mach.v
index c64903b..3f25137 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -58,7 +58,6 @@ Inductive instruction: Set :=
| Mstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction
| Mcall: signature -> mreg + ident -> instruction
| Mtailcall: signature -> mreg + ident -> instruction
- | Malloc: instruction
| Mlabel: label -> instruction
| Mgoto: label -> instruction
| Mcond: condition -> list mreg -> label -> instruction