From b825663924061458e63e72bc28067c55bc8b04f8 Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Tue, 7 Feb 2023 20:59:02 +1100 Subject: [PATCH] aspec: name remaining ThreadControl fields This automatically generates matching selectors. Signed-off-by: Corey Lewis --- spec/abstract/Invocations_A.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/abstract/Invocations_A.thy b/spec/abstract/Invocations_A.thy index c9ee26ab1..4fab2d42a 100644 --- a/spec/abstract/Invocations_A.thy +++ b/spec/abstract/Invocations_A.thy @@ -41,7 +41,7 @@ datatype tcb_invocation = WriteRegisters machine_word bool "machine_word list" arch_copy_register_sets | ReadRegisters machine_word bool machine_word arch_copy_register_sets | CopyRegisters machine_word machine_word bool bool bool bool arch_copy_register_sets - | ThreadControl machine_word cslot_ptr + | ThreadControl (tc_target: machine_word) (tc_slot: cslot_ptr) (tc_new_fault_ep: "cap_ref option") (tc_new_mcpriority: "(word8 * obj_ref) option") (tc_new_priority: "(word8 * obj_ref) option")