From e2ea45f5ba656254fa11bf3f355da67292c11f06 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 10 May 2019 23:37:07 +0200 Subject: more integer Op --- mppa_k1c/Machregs.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'mppa_k1c/Machregs.v') diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index cd8c6606..6e0efe28 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -213,7 +213,10 @@ Global Opaque Definition two_address_op (op: operation) : bool := match op with - | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ + | Omadd | Omaddimm _ + | Omaddl | Omaddlimm _ + | Omsub | Omsubimm _ + | Omsubl | Omsublimm _ | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ | Oinsf _ _ | Oinsfl _ _ => true | _ => false -- cgit From ae22df3c5ef0a60527ea85b83bb71e8c95a6ab9c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 11 May 2019 07:59:11 +0200 Subject: Pmsub compiled --- mppa_k1c/Machregs.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'mppa_k1c/Machregs.v') diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index 6e0efe28..db3dfe64 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -215,8 +215,7 @@ Definition two_address_op (op: operation) : bool := match op with | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ - | Omsub | Omsubimm _ - | Omsubl | Omsublimm _ + | Omsub | Omsubl | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ | Oinsf _ _ | Oinsfl _ _ => true | _ => false -- cgit