Provide an implementation of the header function plat_SGITargetValid
even for non-GIC platforms. This function will not be called, but
verification has a general lemma about it, and the default
implementation makes that lemma true without adding special cases.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Helps the C compiler to recognise irqInvalid as a constant. This in
turn helps with binary verification, because irqInvalid is already
parsed as a constant in Isabelle since it is never written to.
See also the discussion in #1349 and #1324
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The GIC platforms use irq_t for irqInvalid -- bring remaining AArch32
platforms in line with that.
irq_t is an unsigned type (when it is an integer) and enum constants are
signed. For the proofs to treat these platforms uniformly, they need to
be the same kind. They can't all be enums, because irq_t can be a more
complex type for SMP platforms.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
All the kernel header files now use pargma once rather than the ifndef,
as the pre-processed C files do not change while header files
are protected with pargma once. This will also solve any naming issues
caused by ifndef.
This commit also converts our own copyright headers to directly use
SPDX, but leaves all other copyright header intact, only adding the
SPDX ident. As far as possible this commit also merges multiple
Data61 copyright statements/headers into one for consistency.
Every platform has to implement a standard set of interrupt interfaces
that the kernel uses to interract with a machine's interrupt controller.
Providing a single header file for each of these functions provides a
single location to document their behavior.
