From 765d8aa88e0b0479e78c82d5892749b8c9dc9316 Mon Sep 17 00:00:00 2001 From: Joel Beeren Date: Mon, 29 Feb 2016 15:20:56 +1100 Subject: [PATCH] SELFOUR-421: fixed Refine after merge with master --- proof/refine/Untyped_R.thy | 2 +- spec/abstract/Decode_A.thy | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/proof/refine/Untyped_R.thy b/proof/refine/Untyped_R.thy index 5eebf1dc6..4d77b41f7 100644 --- a/proof/refine/Untyped_R.thy +++ b/proof/refine/Untyped_R.thy @@ -882,7 +882,7 @@ lemma decodeUntyped_wf[wp]: apply (simp add:empty_descendants_range_in') apply (clarsimp simp:image_def isCap_simps nullPointer_def word_size cte_level_bits_def field_simps) - apply (rule conjI[rotated], rule conjI[rotated], clarsimp simp: Types_H.isFrameType_def) (* peel of device goal *) + apply (rule conjI[rotated], clarsimp simp: Types_H.isFrameType_def) (* peel of device goal *) apply (clarsimp simp: image_def isCap_simps nullPointer_def word_size cte_level_bits_def field_simps) apply (drule_tac x = x in spec)+ diff --git a/spec/abstract/Decode_A.thy b/spec/abstract/Decode_A.thy index 92df63ff8..383d02ca4 100644 --- a/spec/abstract/Decode_A.thy +++ b/spec/abstract/Decode_A.thy @@ -470,7 +470,7 @@ where new_type \ data_to_obj_type (args!0); user_obj_size \ returnOk $ data_to_nat (args!1); - unlessE (user_obj_size < word_bits - 1) + unlessE (user_obj_size < word_bits - 2) $ throwError (RangeError 0 (of_nat word_bits - 3)); (* max size of untyped = 2^30 *) whenE (new_type = CapTableObject \ user_obj_size = 0) $ throwError (InvalidArgument 1);