From 2245717b5800da80371952999bc0cff5f75aa490 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 1 Jan 2009 12:47:42 +0000 Subject: Continuation of ARM port. Cleaned up Makefile and SVN properties. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@935 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Asmgen.v | 29 ----------------------------- 1 file changed, 29 deletions(-) (limited to 'arm/Asmgen.v') diff --git a/arm/Asmgen.v b/arm/Asmgen.v index a360bded..5e21e14e 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -26,35 +26,6 @@ Require Import Locations. Require Import Mach. Require Import Asm. -(** Translation of the LTL/Linear/Mach view of machine registers - to the ARM view. ARM has two different types for registers - (integer and float) while LTL et al have only one. The - [ireg_of] and [freg_of] are therefore partial in principle. - To keep things simpler, we make them return nonsensical - results when applied to a LTL register of the wrong type. - The proof in [ARMgenproof] will show that this never happens. - - Note that no LTL register maps to [IR14]. - This register is reserved as temporary, to be used - by the generated ARM code. *) - -Definition ireg_of (r: mreg) : ireg := - match r with - | R0 => IR0 | R1 => IR1 | R2 => IR2 | R3 => IR3 - | R4 => IR4 | R5 => IR5 | R6 => IR6 | R7 => IR7 - | R8 => IR8 | R9 => IR9 | R11 => IR11 - | IT1 => IR10 | IT2 => IR12 - | _ => IR0 (* should not happen *) - end. - -Definition freg_of (r: mreg) : freg := - match r with - | F0 => FR0 | F1 => FR1 - | F4 => FR4 | F5 => FR5 | F6 => FR6 | F7 => FR7 - | FT1 => FR2 | FT2 => FR3 - | _ => FR0 (* should not happen *) - end. - (** Recognition of integer immediate arguments. - For arithmetic operations, immediates are 8-bit quantities zero-extended and rotated right by 0, 2, 4, ... 30 bits. -- cgit