#
512a0200 |
|
19-Mar-2020 |
Qian Ge <qian.ge@data61.csiro.au> |
replacing all ifndef with pargma once 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.
|
#
79da0792 |
|
01-Mar-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
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.
|
#
49d2a96d |
|
04-Apr-2019 |
Curtis Millar <curtis.millar@data61.csiro.au> |
Add message register macros to ARMv6
|
#
97bac234 |
|
08-Dec-2016 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
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.
|
#
f658276a |
|
03-Aug-2016 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
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.
|
#
f4188c6c |
|
30-Aug-2016 |
Bamboo <bamboo@keg.ertos.in.nicta.com.au> |
[STYLE_FIX]
|
#
57f1352f |
|
21-Aug-2016 |
amrzar <azarrabi@nicta.com.au> |
SELFOUR-614: calling halt() on the hikey platform results in infinite data abort SELFOUR-408: halt does not halt Remove assembly files for halt and idle thread and add wfi in armv.
|
#
5d439655 |
|
01-Sep-2014 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
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.
|
#
91b7da86 |
|
17-Jul-2014 |
TrusthworthySystems <gatekeeper@sel4.systems> |
Release snapshot
|