#
a424d55e |
|
09-Mar-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
licenses: convert license tags to SPDX
|
#
65074bc3 |
|
19-Feb-2020 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
c-kernel: add Makefile targets useful for binary verification - Add Makefile targets for building ELF binaries and various dumps that are used in binary verification. - Add support for extra CMake command-line arguments. For binary verification, this is used to set the optimisation level for the ELF targets. - Add support for the Debian RISC-V toolchain packages, without breaking existing users with a manually built RISC-V toolchain. - Move reusable parts of the C kernel Makefile out to a separate include file, with support for configuring the build directory. For binary verification, this is used to allow multiple builds at different optimisation levels.
|
#
31d5c1c7 |
|
25-Jul-2019 |
Edward Pierzchalski <ed.pierzchalski@data61.csiro.au> |
cspec: Add feature selection variable. Adds an 'L4V_FEATURES' variable which can be used to select different CMake configurations for seL4. This makes it easier to build and test alternative configurations (like MCS).
|
#
89372de5 |
|
17-Mar-2019 |
Luke Mondy <luke.mondy@data61.csiro.au> |
Update to new toolchain
|
#
d262d7f7 |
|
19-Jul-2018 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
cspec Makefile: add target for kernel source. Adds a target name that ensures that the preprocessed kernel source is up to date, but doesn't do any other work. This avoids confusion when doing a check of source compatibility in building the seL4 input for graph-refine.
|
#
31b63540 |
|
14-Jun-2018 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
riscv: setup cspec build for L4V_ARCH=RISCV64 C parser and word setup copied from X64
|
#
1966c2e0 |
|
13-Apr-2018 |
Japheth Lim <Japheth.Lim@data61.csiro.au> |
cspec: fix make dependency breakage when CMake command fails Once again, with feeling. This commit uses a dummy file as the CMake dependency, to avoid re-running the kernel build in parallel.
|
#
b264f59f |
|
13-Apr-2018 |
Japheth Lim <Japheth.Lim@data61.csiro.au> |
Revert "cspec: fix make dependency breakage when CMake command fails" This reverts commit 16356963878d82c6c227d58e00c04807e1d572f0. Unconditionally cleaning and invoking the kernel build system turns out to be a bad idea; it breaks when multiple builds are run in parallel.
|
#
16356963 |
|
11-Apr-2018 |
Japheth Lim <Japheth.Lim@data61.csiro.au> |
cspec: fix make dependency breakage when CMake command fails
|
#
668d6ea3 |
|
23-Oct-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
cspec: Pass SORRY_BITFIELD_PROOFS to kernel build SORRY_BITFIELD_PROOFS is potentially specified as an environment variable, which does not implicitly become a CMake variable, and so must be explicitly constructed.
|
#
5f012d9c |
|
23-Oct-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
cspec: Reconfigure kernel build on sources change Previously the kernel build would be reconfigured only if the explicit config file passed in -C changed, but this file is very minimal and is only used when a variable needs to be set to a non default value. As a result when default values are added or changed a reconfigure will not be triggered. This commit pays higher build times (by completely purging the build directory) in order to more reliably capture reconfigures and rebuilds.
|
#
8273ca81 |
|
12-Sep-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
cspec: Remove redundancy in build rules and theory files for c-kernel builds Removes files that were duplicated in cspec/$L4V_ARCH directories to exist directly in the cspec directory and contain $L4V_ARCH switches where needed. This allows for a single Makefile for building the C kernel and the KernelInc_C theory, which is different between architectures, to still exist per L4V_ARCH. As the build location of the C kernel, and the resulting kernel_all.c_pp artifact, is moved this change needs to be reflected in all the theory files that refer to it.
|
#
bcf92fb0 |
|
01-May-2017 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
x64 cspec: add x86-64 kernel config for building CKernel This should be the right configuration. However, the c-parser does not yet successfully parse the preprocessed source.
|
#
ea771a8f |
|
15-Jun-2016 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
arm-hyp: configure kernel Makefile for L4V_ARCH=ARM_HYP Set as required for TK1 platform.
|
#
bee4ba00 |
|
17-Jan-2016 |
Gao Xin <xin.gao@nicta.com.au> |
l4v-sabre: fix refine
|
#
c1574f1f |
|
16-Feb-2016 |
Matthew Brecknell <Matthew.Brecknell@nicta.com.au> |
cspec: build: avoid re-entering isabelle via dash-0.5.8
|
#
fad2c6aa |
|
11-Jan-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
paramatrised abstract and haskell specs over L4V_ARCH Haskell translator was modified to support multiple translations of the haskell, with different build parameters.
|
#
d92666bc |
|
10-Dec-2015 |
Japheth Lim <Japheth.Lim@nicta.com.au> |
regression: remove forceful build options from CSpec makefiles. They don't seem to be needed.
|
#
2b23652b |
|
21-Jan-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
cspec: Check CPP exists and fallback on native CPP if possible.
|
#
2a03e81d |
|
14-Jul-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
Import release snapshot.
|