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

armv7: Remove unused function

ARM: Stop using SEL4_ARCH for selective compilation for armv source files

Remove many MODIFIES annotations.

These are redundant for any function which the C-to-Isabelle parser
actually analyses, which is now the vast majority of functions.

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.

fix for asmrefine

l4v-proof-porting: make c-parser and haskell translator happy

Remove CLZ indirection via the CLZL macro.

arm: Use CLZL instead of CLZ

Release snapshot