Imagelibrary/seL4
1
0
Fork 1
mirror of https://github.com/seL4/seL4.git synced 2026-03-27 10:29:57 +00:00
Code Issues Packages Projects Releases Wiki Activity

AArch64: mark isFpuEnable as DONT_TRANSLATE

Browse Source 
Current verification model does not include lazy FPU switching, i.e. it
acts as if this function always returns true, so no FPU faults could be
produced. In order to guard against deriving a contradiction, we don't
allow the C parser to translate it.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This commit is contained in:
Rafal Kolanski
2024-02-01 14:14:11 +11:00
committed by Gerwin Klein
parent 91ec17c5bf
commit c9989664e3
1 changed files with 6 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -134,6 +134,12 @@ static inline void enableFpu(void)
isFPUEnabledCached[CURRENT_CPU_INDEX()] = true;
}
/* Current verification model does not include lazy FPU switching, i.e. it acts
* as if this function always returns true, so no FPU faults could be produced.
* In order to guard against deriving a contradiction, we don't allow the C
* parser to translate it. */
/** MODIFIES: */
/** DONT_TRANSLATE */
static inline bool_t isFpuEnable(void)
{
return isFPUEnabledCached[CURRENT_CPU_INDEX()];