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

asmrefine: skip `init_freemem` 

`init_freemem` isn't verified (and therefore is low-priority for
translation validation). It also takes several hours to show refinement,
much longer than any other function. Until we need to validate it, we
should skip it to improve regression times.

Signed-off-by: Edward Pierzchalski <ed.pierzchalski@data61.csiro.au>
This commit is contained in:
Edward Pierzchalski 2020-09-04 14:50:05 +10:00 committed by Matthew Brecknell
parent 87de976c9b
commit 0bea82f481
1 changed files with 4 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
proof/asmrefine/SEL4GraphRefine.thy
View File

@ -61,10 +61,13 @@ lemma snd_snd_gs_new_frames_new_cnodes[simp]:
by (simp_all add: gs_new_frames_def gs_new_cnodes_def gs_clear_region_def)
ML \<open>
val broken = ["Kernel_C.reserve_region", "Kernel_C.merge_regions", "Kernel_C.arch_init_freemem"];
val slow = ["Kernel_C.init_freemem"];
val dbg = ProveSimplToGraphGoals.new_debug
{
\<comment>\<open> VER-1166 \<close>
skips = ["Kernel_C.reserve_region", "Kernel_C.merge_regions", "Kernel_C.arch_init_freemem"],
skips = broken @ slow,
only = [],
timeout = NONE
};