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

aspec: name remaining ThreadControl fields 

This automatically generates matching selectors.

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
This commit is contained in:
Corey Lewis 2023-02-07 20:59:02 +11:00 committed by Corey Lewis
parent cf1af81384
commit b825663924
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
spec/abstract/Invocations_A.thy
View File

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