diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-17 16:11:43 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-17 16:11:43 +0100 |
| commit | fa0c79015c3ecd2ad63dbf1b50f60039cf043151 (patch) | |
| tree | 93a34c8602948adb99462f7a971283df32796dc5 /aarch64/Asmblockdeps.v | |
| parent | 376315dae506e496d1613934ea6e0e9d056c6526 (diff) | |
| download | compcert-kvx-fa0c79015c3ecd2ad63dbf1b50f60039cf043151.tar.gz compcert-kvx-fa0c79015c3ecd2ad63dbf1b50f60039cf043151.zip | |
Builtin mem spec in scheduler and some needed proof in Postpasssch.v
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. |