From 39710f78062a4a999c079b58181a58e62b78c30b Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Thu, 13 May 2021 17:26:05 +0200
Subject: Register X1 is destroyed by some built-in functions

E.g. __builtin_bswap.  Update Asm modeling of builtins accordingly.
---
 riscV/Asm.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'riscV/Asm.v')

diff --git a/riscV/Asm.v b/riscV/Asm.v
index 7e1b1fc8..a47573a2 100644
--- a/riscV/Asm.v
+++ b/riscV/Asm.v
@@ -1080,7 +1080,7 @@ Inductive step: state -> trace -> state -> Prop :=
       rs' = nextinstr
               (set_res res vres
                 (undef_regs (map preg_of (destroyed_by_builtin ef))
-                   (rs#X31 <- Vundef))) ->
+                   (rs #X1 <- Vundef #X31 <- Vundef))) ->
       step (State rs m) t (State rs' m')
   | exec_step_external:
       forall b ef args res rs m t rs' m',
-- 
cgit