Convert license tags to SPDX identifiers

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.

ARM: Add support to flush L1 caches

Extend the existing seL4_BenchmarkFlushCaches without modifing the usage
of it. Will be used in sel4bench to measure the cold cache performance.

style: consistently attach return type

Add attach-return-type to astyle

Remove many DONT_TRANSLATE markers.

The vast majority of the DONT_TRANSLATE markers in the kernel are used
to hide __asm__ statements and builtin functions
(e.g. __builtin_unreachable ()) from the C-to-Isabelle parser.

The parser now supports underscore identifiers and many __asm__ statements,
and the builtin functions are prototyped, meaning the vast majority of the
DONT_TRANSLATE markers can be dropped. The remaining markers cover functions
that must be treated specially.

DONT_TRANSLATE more inline asm functions.

The c-parser can now parse these functions, but it does it by
discarding the inline ASM block, creating a misleading and likely
malformed function body. It is better to not translate these
with a DONT_TRANSLATE comment.

This change has been made for the current verification platform
only, and should probably be extended to any other verification
targets as necessary.

Release snapshot