From 6dd45e2d5f22bea7e276406ee26ef5fc33bc529f Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Wed, 3 Jul 2019 20:06:31 +1000 Subject: [PATCH] riscv aspec: sync max_untyped_size with Haskell/C --- spec/abstract/RISCV64/Arch_Structs_A.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/abstract/RISCV64/Arch_Structs_A.thy b/spec/abstract/RISCV64/Arch_Structs_A.thy index 28ec2a1da..a2f060b3d 100644 --- a/spec/abstract/RISCV64/Arch_Structs_A.thy +++ b/spec/abstract/RISCV64/Arch_Structs_A.thy @@ -156,7 +156,7 @@ definition untyped_min_bits :: nat definition untyped_max_bits :: nat where - "untyped_max_bits \ 47" + "untyped_max_bits \ 38" primrec arch_kobj_size :: "arch_kernel_obj \ nat" where