From bea92de3b9a395892648407a6b58ed6c059737ed Mon Sep 17 00:00:00 2001 From: Thomas Sewell Date: Mon, 21 Mar 2016 15:31:03 +1100 Subject: [PATCH] Verification: adjust use of new bf proof features. Apologies, some final adjustments got lost in the previous pull request round. This version actually works. --- tools/bitfield_gen.py | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/tools/bitfield_gen.py b/tools/bitfield_gen.py index fa922b69f..3187b446a 100755 --- a/tools/bitfield_gen.py +++ b/tools/bitfield_gen.py @@ -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