From 373ad4a6efcb6cd0ecd30e7c131640b9783f1269 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Sun, 20 Dec 2020 14:30:47 +0100 Subject: Fix the Asmblock/Asm proof --- aarch64/Asmblock.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'aarch64/Asmblock.v') diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index a4decae7..58817776 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -640,7 +640,7 @@ Definition exec_cfi (f: function) (cfi: cf_instruction) (rs: regset) (m: mem) : match (rs#X16 <- Vundef)#r with | Vint n => SOME lbl <- list_nth_z tbl (Int.unsigned n) IN - goto_label f lbl (rs#X16 <- Vundef #X17 <- Vundef) m + goto_label f lbl (rs#X16 <- Vundef) m | _ => Stuck end end. @@ -951,7 +951,7 @@ Inductive exec_exit (f: function) size_b (rs: regset) (m: mem): (option control) external_call ef ge vargs m t vres m' -> rs' = incrPC size_b (set_res (map_builtin_res DR res) vres - (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) -> + (undef_regs (DR (IR X16) :: DR (IR X30) :: map preg_of (destroyed_by_builtin ef)) rs)) -> exec_exit f size_b rs m (Some (Pbuiltin ef args res)) t rs' m' . -- cgit