From 9e685553d2f3147f7e1626ff0ea625495abd85c7 Mon Sep 17 00:00:00 2001 From: Matthew Brecknell Date: Wed, 22 Jul 2020 17:13:34 +1000 Subject: [PATCH] risc-v simpl-export: ignore `arch_init_freemem` A new version of `arch_init_freemem` for RISC-V introduces some heap access patterns which are not well supported by SimplExportAndRefine. `arch_init_freemem` is already ignored by `graph-refine`, because it is inlined into `init_freemem`, which contains complex loops. Therefore, we don't lose anything by ignoring it in SimplExportAndRefine. Although the problem only manifests on RISC-V, we ignore it on all platforms. Signed-off-by: Matthew Brecknell --- proof/asmrefine/SEL4GraphRefine.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proof/asmrefine/SEL4GraphRefine.thy b/proof/asmrefine/SEL4GraphRefine.thy index a4a142675..4a3f79cdb 100644 --- a/proof/asmrefine/SEL4GraphRefine.thy +++ b/proof/asmrefine/SEL4GraphRefine.thy @@ -65,7 +65,7 @@ lemma snd_snd_gs_new_frames_new_cnodes[simp]: ML \ \\ VER-1166 \ -val blacklist = ["Kernel_C.reserve_region", "Kernel_C.merge_regions"] +val blacklist = ["Kernel_C.reserve_region", "Kernel_C.merge_regions", "Kernel_C.arch_init_freemem"] val dbg = ProveSimplToGraphGoals.new_debug blacklist []; \