diff options
Diffstat (limited to 'aarch64/Asmblockdeps.v')
-rw-r--r-- | aarch64/Asmblockdeps.v | 4 |
1 files changed, 2 insertions, 2 deletions
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. |