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

SELFOUR-421: fixed Refine after merge with master

This commit is contained in:
Joel Beeren 2016-02-29 15:20:56 +11:00 committed by Rafal Kolanski
parent 78bd770240
commit 765d8aa88e
2 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/refine/Untyped_R.thy
View File

@ -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)+

2
spec/abstract/Decode_A.thy
View File

@ -470,7 +470,7 @@ where
new_type \<leftarrow> data_to_obj_type (args!0);
user_obj_size \<leftarrow> 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 \<and> user_obj_size = 0)
$ throwError (InvalidArgument 1);