From cfc681ae18c59f4a19143a7245be23eb6a4045a0 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 30 Aug 2019 10:10:06 +0200 Subject: add finvw ; not yet generated --- mppa_k1c/NeedOp.v | 1 + 1 file changed, 1 insertion(+) (limited to 'mppa_k1c/NeedOp.v') diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index 84e32d0f..856f5b54 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -124,6 +124,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oaddf | Osubf | Omulf | Odivf | Ominf | Omaxf => op2 (default nv) | Onegfs | Oabsfs => op1 (default nv) | Oaddfs | Osubfs | Omulfs | Odivfs | Ominfs | Omaxfs => op2 (default nv) + | Oinvfs => op1 (default nv) | Ofloatofsingle | Osingleoffloat => op1 (default nv) | Ointoffloat | Ointuoffloat => op1 (default nv) | Olongoffloat | Olonguoffloat | Ofloatoflong | Ofloatoflongu => op1 (default nv) -- cgit