- 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

1 files changed, 0 insertions, 14 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index 72534c0..3bb2cca 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -145,7 +145,6 @@ Inductive instruction : Set :=
   | Psufd: freg -> freg -> freg -> instruction     (**r float subtraction *)
 
   (* Pseudo-instructions *)
-  | Pallocblock: instruction                       (**r dynamic allocation *)
   | Pallocframe: Z -> Z -> int -> instruction      (**r allocate new stack frame *)
   | Pfreeframe: int -> instruction                 (**r deallocate stack frame and restore previous frame *)
   | Plabel: label -> instruction                   (**r define a code label *)
@@ -232,11 +231,6 @@ lbl:    .long   0x43300000, 0x00000000
 >>
   Again, our memory model cannot comprehend that this operation
   frees (logically) the current stack frame.
-- [Pallocheap]: in the formal semantics, this pseudo-instruction
-  allocates a heap block of size the contents of [GPR3], and leaves
-  a pointer to this block in [GPR3].  In the generated assembly code,
-  it is turned into a call to the allocation function of the run-time
-  system.
 *)
 
 Definition code := list instruction.
@@ -538,14 +532,6 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
   | Psufd r1 r2 r3 =>     
       OK (nextinstr (rs#r1 <- (Val.subf rs#r2 rs#r3))) m
   (* Pseudo-instructions *)
-  | Pallocblock =>
-      match rs#IR0 with
-      | Vint n =>
-          let (m', b) := Mem.alloc m 0 (Int.signed n) in
-          OK (nextinstr (rs#IR0 <- (Vptr b Int.zero)
-                           #IR14 <- (Val.add rs#PC Vone))) m'
-      | _ => Error
-      end
   | Pallocframe lo hi pos =>             
       let (m1, stk) := Mem.alloc m lo hi in
       let sp := (Vptr stk (Int.repr lo)) in