Skip to content

Commit

Permalink
x64 spec squash: PR suggestions
Browse files Browse the repository at this point in the history
Signed-off-by: Corey Lewis <[email protected]>
  • Loading branch information
corlewis committed Dec 17, 2024
1 parent 52a23eb commit f2100f6
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion spec/abstract/X64/FPU_A.thy
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ definition load_fpu_state :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad
do_machine_op (writeFpuState fpu_state)
od"

\<comment> \<open>FIXME: maybe use an if instead of the case (depends on if wpc or if\_split is easier)\<close>
\<comment> \<open>FIXME FPU: maybe use an if instead of the case (depends on if wpc or if\_split is easier)\<close>
definition switch_local_fpu_owner :: "obj_ref option \<Rightarrow> (unit,'z::state_ext) s_monad" where
"switch_local_fpu_owner new_owner \<equiv> do
do_machine_op enableFpu;
Expand Down

0 comments on commit f2100f6

Please sign in to comment.