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

arm-hyp ainvs: drop removed _impl consts from crunch_ignore

This commit is contained in:
Rafal Kolanski 2017-02-28 03:07:07 +11:00 committed by Alejandro Gomez-Londono
parent 53a2826e77
commit b04eb57d99
1 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
proof/invariant-abstract/ARM_HYP/ArchVSpace_AI.thy
View File

@ -116,11 +116,11 @@ definition
"glob_vs_refs \<equiv> arch_obj_fun_lift glob_vs_refs_arch {}"
crunch_ignore (add: writeContextIDAndPD_impl addressTranslateS1CPR_impl
setSCTLR_impl setHCR_impl getSCTLR_impl setACTLR_impl getACTLR_impl
get_gic_vcpu_ctrl_vmcr_impl set_gic_vcpu_ctrl_vmcr_impl
get_gic_vcpu_ctrl_apr_impl set_gic_vcpu_ctrl_apr_impl
setSCTLR_impl setHCR_impl setACTLR_impl
set_gic_vcpu_ctrl_vmcr_impl
set_gic_vcpu_ctrl_apr_impl
get_gic_vcpu_ctrl_lr_impl set_gic_vcpu_ctrl_lr_impl
get_gic_vcpu_ctrl_hcr_impl set_gic_vcpu_ctrl_hcr_impl
set_gic_vcpu_ctrl_hcr_impl
dsb_impl)
crunch pspace_in_kerbel_window[wp]: do_machine_op "pspace_in_kernel_window"