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

design: generate new GenInvocationLabels type

This commit is contained in:
Gerwin Klein 2018-09-08 17:05:56 +10:00
parent 3a6ce53def
commit 700dab41aa
2 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
spec/design/skel/InvocationLabels_H.thy
View File

@ -23,7 +23,7 @@ text \<open>
An enumeration of all system call labels.
\<close>
#INCLUDE_HASKELL SEL4/API/InvocationLabels.lhs ArchLabels= ONLY InvocationLabel
#INCLUDE_HASKELL SEL4/API/InvocationLabels.lhs ArchLabels= ONLY GenInvocationLabels InvocationLabel
#INCLUDE_HASKELL SEL4/API/InvocationLabels.lhs instanceproofs
end

4
spec/design/skel/Invocations_H.thy
View File

@ -18,8 +18,8 @@ requalify_types (in Arch)
copy_register_sets irqcontrol_invocation
invocation
#INCLUDE_HASKELL SEL4/API/Invocation.lhs Arch=Arch NOT InvocationLabel
#INCLUDE_HASKELL SEL4/API/InvocationLabels.lhs ONLY invocationType
#INCLUDE_HASKELL SEL4/API/Invocation.lhs Arch=Arch NOT GenInvocationLabels InvocationLabel
#INCLUDE_HASKELL SEL4/API/InvocationLabels.lhs ONLY invocationType genInvocationType
context Arch begin
context begin global_naming global