adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

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 <Matthew.Brecknell@data61.csiro.au>
This commit is contained in:
Matthew Brecknell 2020-07-22 17:13:34 +10:00
parent b356f65969
commit 9e685553d2
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/asmrefine/SEL4GraphRefine.thy
View File

@ -65,7 +65,7 @@ lemma snd_snd_gs_new_frames_new_cnodes[simp]:
ML \<open>
\<comment>\<open> VER-1166 \<close>
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 [];
\<close>