seL4/include
Rafal Kolanski c9989664e3 AArch64: mark isFpuEnable as DONT_TRANSLATE
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>
2024-02-02 09:14:07 +11:00
..
32/mode replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
64/mode replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
api doc: improve comments 2023-08-14 15:41:57 +10:00
arch AArch64: mark isFpuEnable as DONT_TRANSLATE 2024-02-02 09:14:07 +11:00
benchmark benchmark: config opt. name to enable log buffer 2022-03-31 08:56:06 +11:00
drivers Update PLIC handling for Star64/U74-MC 2023-11-08 14:34:18 +00:00
fastpath Implemented the vm fault fastpath on aarch64 2023-03-08 17:58:14 +11:00
kernel mcs: remove getKernelWcetTicks from refill_ready 2023-11-08 11:01:00 +11:00
machine mcs: move setDeadline assertions 2023-11-08 11:01:00 +11:00
model use types time_t and tickts_t properly 2023-08-14 15:41:57 +10:00
object remove Arch_migrateTCB() 2023-06-21 08:58:28 +10:00
plat make physBase a static inline function 2023-03-07 14:29:14 +11:00
smp create helper function handle_SysDebugSendIPI() 2022-01-10 11:58:30 +11:00
api.h replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
assert.h debug: use c99 standard instead of gcc extensions 2023-11-16 12:09:52 +00:00
basic_types.h boot: document region types 2023-04-12 15:07:02 +10:00
bootinfo.h boot: Remove constant BI_FRAME_SIZE_BITS 2023-08-23 15:10:32 +02:00
compound_types.h trivial: remove superfluous empty lines 2021-09-27 23:09:09 +10:00
config.h libsel4: Fix name for AARCH64_VSPACE_S2_START_L1 2021-09-06 08:08:54 +10:00
hardware.h boot: simplify boot code recycling 2023-08-13 09:04:26 +10:00
linker.h replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
machine.h re-use existing functions to avoid redundancy 2022-09-15 11:25:04 +02:00
object.h trivial: remove duplicate headers 2022-02-05 15:30:25 +11:00
stdarg.h trivial: remove superfluous empty lines 2021-09-27 23:09:09 +10:00
stdint.h print 64-bit integers on 32-bits systems fully 2021-11-26 06:01:11 +01:00
string.h trivial: remove superfluous empty lines 2021-09-27 23:09:09 +10:00
types.h trivial: remove superfluous empty lines 2021-09-27 23:09:09 +10:00
util.h make macro ARRAY_SIZE() handle corner cases 2022-03-10 18:16:00 +11:00