From 34261e53d0da905307eb3e0a0b711571365b078e Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 3 Apr 2019 12:04:33 +0200 Subject: Preuve du transl_load et transl_store registre offset --- mppa_k1c/Asmblockgen.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'mppa_k1c/Asmblockgen.v') diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 54a1b0f4..3260312d 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -825,8 +825,8 @@ Definition transl_load_rrr (chunk: memory_chunk) (addr: addressing) Definition transl_load (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := - match args with - | a1 :: a2 :: nil => transl_load_rrr chunk addr args dst k + match addr with + | Aindexed2 => transl_load_rrr chunk addr args dst k | _ => transl_load_rro chunk addr args dst k end. @@ -854,9 +854,9 @@ Definition transl_store_rrr (chunk: memory_chunk) (addr: addressing) Definition transl_store (chunk: memory_chunk) (addr: addressing) (args: list mreg) (src: mreg) (k: bcode) : res bcode := - match args with - | a1 :: a2 :: nil => transl_store_rrr chunk addr args src k - | _ => transl_load_rro chunk addr args src k + match addr with + | Aindexed2 => transl_store_rrr chunk addr args src k + | _ => transl_store_rro chunk addr args src k end. (** Function epilogue *) -- cgit