From 5e3898945c063801d4a93f44182d160ccfe4badc Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Sun, 6 Dec 2020 16:47:19 +0100
Subject: PowerPC modeling of registers destroyed by pseudo-instructions

Inlined built-in functions destroy GPR0
---
 powerpc/Asm.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'powerpc/Asm.v')

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 6ec20d62..d9901960 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -1195,7 +1195,7 @@ Inductive step: state -> trace -> state -> Prop :=
       external_call ef ge vargs m t vres m' ->
       rs' = nextinstr
               (set_res res vres
-                (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) ->
+                (undef_regs (IR GPR0 :: map preg_of (destroyed_by_builtin ef)) rs)) ->
       step (State rs m) t (State rs' m')
   | exec_step_external:
       forall b ef args res rs m t rs' m',
-- 
cgit