Imagelibrary/seL4
1
0
Fork 1
mirror of https://github.com/seL4/seL4.git synced 2026-04-04 22:39:54 +00:00
Code Issues Packages Projects Releases Wiki Activity

FPU: ease verification

Browse Source 
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
This commit is contained in:
Corey Lewis
2025-03-24 13:45:05 +11:00
committed by Gerwin Klein
parent ed33077f54
commit 504f1ccf00
4 changed files with 8 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
include/arch/arm/arch/32/mode/machine/fpu.h
View File

@@ -154,7 +154,8 @@ static inline void saveFpuState(tcb_t *thread)
* it.
*
*/
/** MODIFIES: phantom_machine_state */
/** DONT_TRANSLATE */
static inline void enableFpu(void)
{
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT

2
include/arch/arm/arch/64/mode/machine/fpu.h
View File

@@ -107,6 +107,8 @@ static inline void enableFpuEL01(void)
/* Enable the FPU to be used without faulting.
* Required even if the kernel attempts to use the FPU. */
/** MODIFIES: phantom_machine_state */
/** DONT_TRANSLATE */
static inline void enableFpu(void)
{
if (config_set(CONFIG_ARM_HYPERVISOR_SUPPORT)) {

2
include/arch/riscv/arch/machine/fpu.h
View File

@@ -152,6 +152,8 @@ static inline void loadFpuState(const tcb_t *thread)
write_fcsr(src->fcsr);
}
/** MODIFIES: phantom_machine_state */
/** DONT_TRANSLATE */
static inline void enableFpu(void)
{
isFPUEnabled[CURRENT_CPU_INDEX()] = true;

2
include/arch/x86/arch/machine/fpu.h
View File

@@ -89,6 +89,8 @@ static inline void finit(void)
* Enable the FPU to be used without faulting.
* Required even if the kernel attempts to use the FPU.
*/
/** MODIFIES: phantom_machine_state */
/** DONT_TRANSLATE */
static inline void enableFpu(void)
{
asm volatile("clts" :: "m"(control_reg_order));