diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-11 08:48:31 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-11 08:48:31 +0100 |
commit | bac2a0854ea51217690bc6f225da62053ed7ac06 (patch) | |
tree | 752e3b627d70450f544c182b06a70f803ef73965 /powerpc/Asmgen.v | |
parent | 7247e4bb85d50834983bc71e6415fe1bf065aa46 (diff) | |
download | compcert-bac2a0854ea51217690bc6f225da62053ed7ac06.tar.gz compcert-bac2a0854ea51217690bc6f225da62053ed7ac06.zip |
Removed unused parameter from is_small/rel_data.
The ofs parameter is no longer used. Adopted the proofs and ml
code using it.
Bug 18394
Diffstat (limited to 'powerpc/Asmgen.v')
-rw-r--r-- | powerpc/Asmgen.v | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 4ad5e2f9..f961ad73 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -331,9 +331,9 @@ Definition transl_op do r <- freg_of res; OK (Plfis r f :: k) | Oaddrsymbol s ofs, nil => do r <- ireg_of res; - OK (if symbol_is_small_data s ofs then + OK (if symbol_is_small_data s then Paddi r GPR0 (Csymbol_sda s ofs) :: k - else if symbol_is_rel_data s ofs then + else if symbol_is_rel_data s then Paddis r GPR0 (Csymbol_rel_high s ofs) :: Paddi r r (Csymbol_rel_low s ofs) :: k else @@ -352,10 +352,10 @@ Definition transl_op do r1 <- ireg_of a1; do r <- ireg_of res; OK (addimm r r1 n k) | Oaddsymbol s ofs, a1 :: nil => do r1 <- ireg_of a1; do r <- ireg_of res; - OK (if symbol_is_small_data s ofs then + OK (if symbol_is_small_data s then Paddi GPR0 GPR0 (Csymbol_sda s ofs) :: Padd r r1 GPR0 :: k - else if symbol_is_rel_data s ofs then + else if symbol_is_rel_data s then Pmr GPR0 r1 :: Paddis r GPR0 (Csymbol_rel_high s ofs) :: Paddi r r (Csymbol_rel_low s ofs) :: @@ -536,9 +536,9 @@ Definition transl_memory_access do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (mk2 r1 r2 :: k) | Aglobal symb ofs, nil => - OK (if symbol_is_small_data symb ofs then + OK (if symbol_is_small_data symb then mk1 (Csymbol_sda symb ofs) GPR0 :: k - else if symbol_is_rel_data symb ofs then + else if symbol_is_rel_data symb then Paddis temp GPR0 (Csymbol_rel_high symb ofs) :: Paddi temp temp (Csymbol_rel_low symb ofs) :: mk1 (Cint Int.zero) temp :: k @@ -547,10 +547,10 @@ Definition transl_memory_access mk1 (Csymbol_low symb ofs) temp :: k) | Abased symb ofs, a1 :: nil => do r1 <- ireg_of a1; - OK (if symbol_is_small_data symb ofs then + OK (if symbol_is_small_data symb then Paddi GPR0 GPR0 (Csymbol_sda symb ofs) :: mk2 r1 GPR0 :: k - else if symbol_is_rel_data symb ofs then + else if symbol_is_rel_data symb then Pmr GPR0 r1 :: Paddis temp GPR0 (Csymbol_rel_high symb ofs) :: Paddi temp temp (Csymbol_rel_low symb ofs) :: @@ -736,4 +736,3 @@ Definition transf_fundef (f: Mach.fundef) : res Asm.fundef := Definition transf_program (p: Mach.program) : res Asm.program := transform_partial_program transf_fundef p. - |