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

workaround for bad bug in dcorres 

This line invokes "wp" with a schematic postcondition, which makes
this proof very unstable when new wp rules are added.
This commit is contained in:
Daniel Matichuk 2017-04-13 16:05:34 +10:00
parent 196e2e2e0a
commit ad82c6c751
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/drefine/Ipc_DR.thy
View File

@ -2270,7 +2270,7 @@ lemma dcorres_set_thread_state_Restart:
apply (simp add: get_etcb_def)
apply (simp add: not_idle_thread_def)
apply (simp add: tcb_pending_op_slot_def)
apply ((wp | clarsimp | simp)+)[2]
apply ((wp del: use_corresK | clarsimp | simp)+)[2]
apply (frule(1) valid_etcbs_get_tcb_get_etcb, clarsimp simp: get_etcb_def)
apply (simp add:KHeap_D.set_cap_def set_object_def gets_the_def gets_def bind_assoc)
apply (rule dcorres_absorb_get_l)