diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-20 14:30:47 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-20 14:30:47 +0100 |
| commit | 373ad4a6efcb6cd0ecd30e7c131640b9783f1269 (patch) | |
| tree | dc555a7401a74790f629aae02bb919834e1faf94 /aarch64/Asmblock.v | |
| parent | 32abc8049ce030f0e338f526f7d16c585d84025f (diff) | |
| download | compcert-kvx-373ad4a6efcb6cd0ecd30e7c131640b9783f1269.tar.gz compcert-kvx-373ad4a6efcb6cd0ecd30e7c131640b9783f1269.zip | |
Fix the Asmblock/Asm proof
Diffstat (limited to 'aarch64/Asmblock.v')
| -rw-r--r-- | aarch64/Asmblock.v | 4 |
1 files changed, 2 insertions, 2 deletions
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' . |