Imagelibrary/seL4
1
0
Fork 1
mirror of https://github.com/seL4/seL4.git synced 2026-04-09 08:49:54 +00:00
Code Issues Packages Projects Releases Wiki Activity

Verification: adjust use of new bf proof features.

Browse Source 
Apologies, some final adjustments got lost in the previous pull
request round. This version actually works.
This commit is contained in:
Thomas Sewell
2016-03-21 15:31:03 +11:00
parent b327dac1f9
commit bea92de3b9
1 changed files with 8 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files

13
tools/bitfield_gen.py
View File

@@ -800,7 +800,9 @@ done'''],
ptr_set_template('set_%(field)s', direct_ptr_name),
''' unfolding ptrval_def
apply(rule allI, rule conseqPre, vcg)
apply(clarsimp simp add: packed_heap_update_collapse_hrs typ_heap_simps guard_simps)
apply(clarsimp simp:guard_simps)
apply(prove_bf_clift_invariance?)
apply(clarsimp simp add: packed_heap_update_collapse_hrs typ_heap_simps)?
apply(rule exI, rule conjI[rotated], rule refl)
apply(clarsimp simp:h_t_valid_clift_Some_iff
@@ -826,7 +828,7 @@ done'''],
apply(simp add:h_t_valid_c_guard guard_simps)
(* Discharge heap-invariance conjuncts *)
apply prove_bf_clift_invariance
apply(prove_bf_clift_invariance?)
(* Lift field updates to bitfield struct updates *)
apply(simp add:heap_update_field_hrs h_t_valid_c_guard typ_heap_simps)
@@ -970,6 +972,7 @@ done'''],
apply(frule h_t_valid_c_guard_cparent, simp, simp add: typ_uinfo_t_def)
apply(clarsimp simp: h_t_valid_clift_Some_iff)
apply(frule clift_subtype, simp+)
apply(prove_bf_clift_invariance?)
apply(clarsimp simp: typ_heap_simps c_guard_clift)
apply(simp add: guard_simps mask_shift_simps
@@ -997,7 +1000,7 @@ done
apply(frule h_t_valid_c_guard_cparent, simp, simp add: typ_uinfo_t_def)
apply(drule h_t_valid_clift_Some_iff[THEN iffD1], erule exE)
apply(frule clift_subtype, simp, simp)
apply prove_bf_clift_invariance
apply(prove_bf_clift_invariance?)
apply(clarsimp simp: typ_heap_simps c_guard_clift)
apply(simp add: guard_simps mask_shift_simps
@@ -1094,7 +1097,7 @@ done
apply(frule h_t_valid_c_guard_cparent, simp, simp add: typ_uinfo_t_def)
apply(drule h_t_valid_clift_Some_iff[THEN iffD1], erule exE)
apply(frule clift_subtype, simp, simp)
apply prove_bf_clift_invariance
apply(prove_bf_clift_invariance?)
apply(clarsimp simp: typ_heap_simps c_guard_clift)
apply(simp add: guard_simps mask_shift_simps)
apply(simp add:%(name)s_%(block)s_lift_def)
@@ -1116,7 +1119,7 @@ done
apply(frule h_t_valid_c_guard_cparent, simp, simp add: typ_uinfo_t_def)
apply(drule h_t_valid_clift_Some_iff[THEN iffD1], erule exE)
apply(frule clift_subtype, simp, simp)
apply prove_bf_clift_invariance
apply(prove_bf_clift_invariance?)
apply(clarsimp simp: typ_heap_simps c_guard_clift)
apply(simp add: guard_simps mask_shift_simps