From fa0c79015c3ecd2ad63dbf1b50f60039cf043151 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 17 Nov 2020 16:11:43 +0100 Subject: Builtin mem spec in scheduler and some needed proof in Postpasssch.v --- aarch64/Asmblockdeps.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'aarch64/Asmblockdeps.v') diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v index 25b9c5c5..4297cfd8 100644 --- a/aarch64/Asmblockdeps.v +++ b/aarch64/Asmblockdeps.v @@ -1088,7 +1088,7 @@ Definition trans_control (ctl: control) : inst := (#PC, Op (Control (Obtbl tbl)) (PReg(#r) @ PReg(#PC) @ Enil)); (#X16, Op (Constant Vundef) Enil); (#X17, Op (Constant Vundef) Enil)] - | Pbuiltin ef args res => [(#PC, Op (Control (OError)) Enil)] + | Pbuiltin ef args res => [] end. Definition trans_exit (ex: option control) : L.inst := @@ -2637,7 +2637,7 @@ End SECT_BBLOCK_EQUIV. (** REWRITE RULES *) Definition is_constant (o: op): bool := - match o with + match o with (* TODO *) | OArithP _ | OArithRR0_XZR _ _ | Ofmovi_XZR _ => true | _ => false end. -- cgit