Imagelibrary/seL4
1
0
Fork 1
mirror of https://github.com/seL4/seL4.git synced 2026-04-09 16:59:55 +00:00
Code Issues Packages Projects Releases Wiki Activity

Compare commits

base: Imagelibrary:10.1.0
Branches Tags
Imagelibrary:master Imagelibrary:python-types Imagelibrary:michaelm/ipc_queues Imagelibrary:smc-ifdef Imagelibrary:aos Imagelibrary:lsf37/no-clock-sync-riscv Imagelibrary:lsf37/riscv-clock-test Imagelibrary:zynqmp-12.0.0 Imagelibrary:mbrcknl/mcs-grant-via-reply-alt Imagelibrary:mbrcknl/mcs-grant-via-reply Imagelibrary:lsf37/cython Imagelibrary:axel-h/ci-base Imagelibrary:jade/msi Imagelibrary:exynos5-ver Imagelibrary:mbrcknl/bv-ci Imagelibrary:mbrcknl/preprocess-deploy-mcs Imagelibrary:riscv_he_v0.6 Imagelibrary:rk3288 Imagelibrary:sylvain/gic-v3 Imagelibrary:misra-12.1.0-changes Imagelibrary:riscv-binary-verification Imagelibrary:zynqmp-fpu-ver-v11 Imagelibrary:imx8-fpu-ver-v11 Imagelibrary:imx8-fpu-ver Imagelibrary:kent/riscv-fp-clear-res Imagelibrary:sylvain/zynqmp Imagelibrary:df-public Imagelibrary:qge/arm-smmu-v2 Imagelibrary:riscv_hyp Imagelibrary:cmillar/asid-map Imagelibrary:xu4_vmm_wip RTOS:master RTOS:smc-ifdef RTOS:michaelm/ipc_queues RTOS:microkit RTOS:aos RTOS:lsf37/no-clock-sync-riscv RTOS:lsf37/riscv-clock-test RTOS:zynqmp-12.0.0 RTOS:mbrcknl/mcs-grant-via-reply-alt RTOS:mbrcknl/mcs-grant-via-reply RTOS:lsf37/cython RTOS:axel-h/ci-base RTOS:jade/msi RTOS:exynos5-ver RTOS:mbrcknl/bv-ci RTOS:mbrcknl/preprocess-deploy-mcs RTOS:riscv_he_v0.6 RTOS:rk3288 RTOS:sylvain/gic-v3 RTOS:misra-12.1.0-changes RTOS:riscv-binary-verification RTOS:zynqmp-fpu-ver-v11 RTOS:imx8-fpu-ver-v11 RTOS:imx8-fpu-ver RTOS:kent/riscv-fp-clear-res RTOS:sylvain/zynqmp RTOS:df-public RTOS:qge/arm-smmu-v2 RTOS:riscv_hyp RTOS:cmillar/asid-map RTOS:xu4_vmm_wip
Imagelibrary:15.0.0 Imagelibrary:microkit-pre-2.1.0 Imagelibrary:14.0.0 Imagelibrary:13.0.0 Imagelibrary:12.1.0 Imagelibrary:12.0.0 Imagelibrary:11.0.0 Imagelibrary:10.1.1-mcs Imagelibrary:10.1.1 Imagelibrary:10.1.0 Imagelibrary:mcs-tutorials Imagelibrary:10.0.0-mcs Imagelibrary:10.0.0 Imagelibrary:9.0.1 Imagelibrary:9.0.0-mcs Imagelibrary:9.0.0 Imagelibrary:8.0.0 Imagelibrary:7.0.0 Imagelibrary:6.0.0 Imagelibrary:5.2.0-mcs Imagelibrary:5.2.0 Imagelibrary:5.1.0 Imagelibrary:5.0.0 Imagelibrary:4.0.0 Imagelibrary:rt-deprecated Imagelibrary:3.2.0 Imagelibrary:arm_hyp-deprecated Imagelibrary:3.1.0 Imagelibrary:1.0.0-rt-dev Imagelibrary:experimental-deprecated Imagelibrary:3.0.1 Imagelibrary:3.0.0 Imagelibrary:2.1.0 Imagelibrary:0.0.1-rt-dev Imagelibrary:2.0.0 Imagelibrary:x86_64-deprecated Imagelibrary:1.0.4 Imagelibrary:API-master-01-03--release-2014-08-10 Imagelibrary:API-experimental-01-03--release-2014-08-10 Imagelibrary:API-experimental-01-03--release-2014-07-29 Imagelibrary:API-master-01-03--release-2014-07-29 Imagelibrary:1.0.3 RTOS:14.0.0 RTOS:13.0.0 RTOS:12.1.0 RTOS:12.0.0 RTOS:11.0.0 RTOS:10.1.1-mcs RTOS:10.1.1 RTOS:10.1.0 RTOS:mcs-tutorials RTOS:10.0.0-mcs RTOS:10.0.0 RTOS:9.0.1 RTOS:9.0.0-mcs RTOS:9.0.0 RTOS:8.0.0 RTOS:7.0.0 RTOS:6.0.0 RTOS:5.2.0-mcs RTOS:5.2.0 RTOS:5.1.0 RTOS:5.0.0 RTOS:4.0.0 RTOS:rt-deprecated RTOS:3.2.0 RTOS:arm_hyp-deprecated RTOS:3.1.0 RTOS:1.0.0-rt-dev RTOS:experimental-deprecated RTOS:3.0.1 RTOS:3.0.0 RTOS:2.1.0 RTOS:0.0.1-rt-dev RTOS:2.0.0 RTOS:x86_64-deprecated RTOS:1.0.4 RTOS:API-master-01-03--release-2014-08-10 RTOS:API-experimental-01-03--release-2014-08-10 RTOS:API-experimental-01-03--release-2014-07-29 RTOS:API-master-01-03--release-2014-07-29 RTOS:1.0.3
..
compare: RTOS:10.1.1
Branches Tags
RTOS:master RTOS:smc-ifdef RTOS:michaelm/ipc_queues RTOS:microkit RTOS:aos RTOS:lsf37/no-clock-sync-riscv RTOS:lsf37/riscv-clock-test RTOS:zynqmp-12.0.0 RTOS:mbrcknl/mcs-grant-via-reply-alt RTOS:mbrcknl/mcs-grant-via-reply RTOS:lsf37/cython RTOS:axel-h/ci-base RTOS:jade/msi RTOS:exynos5-ver RTOS:mbrcknl/bv-ci RTOS:mbrcknl/preprocess-deploy-mcs RTOS:riscv_he_v0.6 RTOS:rk3288 RTOS:sylvain/gic-v3 RTOS:misra-12.1.0-changes RTOS:riscv-binary-verification RTOS:zynqmp-fpu-ver-v11 RTOS:imx8-fpu-ver-v11 RTOS:imx8-fpu-ver RTOS:kent/riscv-fp-clear-res RTOS:sylvain/zynqmp RTOS:df-public RTOS:qge/arm-smmu-v2 RTOS:riscv_hyp RTOS:cmillar/asid-map RTOS:xu4_vmm_wip Imagelibrary:master Imagelibrary:python-types Imagelibrary:michaelm/ipc_queues Imagelibrary:smc-ifdef Imagelibrary:aos Imagelibrary:lsf37/no-clock-sync-riscv Imagelibrary:lsf37/riscv-clock-test Imagelibrary:zynqmp-12.0.0 Imagelibrary:mbrcknl/mcs-grant-via-reply-alt Imagelibrary:mbrcknl/mcs-grant-via-reply Imagelibrary:lsf37/cython Imagelibrary:axel-h/ci-base Imagelibrary:jade/msi Imagelibrary:exynos5-ver Imagelibrary:mbrcknl/bv-ci Imagelibrary:mbrcknl/preprocess-deploy-mcs Imagelibrary:riscv_he_v0.6 Imagelibrary:rk3288 Imagelibrary:sylvain/gic-v3 Imagelibrary:misra-12.1.0-changes Imagelibrary:riscv-binary-verification Imagelibrary:zynqmp-fpu-ver-v11 Imagelibrary:imx8-fpu-ver-v11 Imagelibrary:imx8-fpu-ver Imagelibrary:kent/riscv-fp-clear-res Imagelibrary:sylvain/zynqmp Imagelibrary:df-public Imagelibrary:qge/arm-smmu-v2 Imagelibrary:riscv_hyp Imagelibrary:cmillar/asid-map Imagelibrary:xu4_vmm_wip
RTOS:14.0.0 RTOS:13.0.0 RTOS:12.1.0 RTOS:12.0.0 RTOS:11.0.0 RTOS:10.1.1-mcs RTOS:10.1.1 RTOS:10.1.0 RTOS:mcs-tutorials RTOS:10.0.0-mcs RTOS:10.0.0 RTOS:9.0.1 RTOS:9.0.0-mcs RTOS:9.0.0 RTOS:8.0.0 RTOS:7.0.0 RTOS:6.0.0 RTOS:5.2.0-mcs RTOS:5.2.0 RTOS:5.1.0 RTOS:5.0.0 RTOS:4.0.0 RTOS:rt-deprecated RTOS:3.2.0 RTOS:arm_hyp-deprecated RTOS:3.1.0 RTOS:1.0.0-rt-dev RTOS:experimental-deprecated RTOS:3.0.1 RTOS:3.0.0 RTOS:2.1.0 RTOS:0.0.1-rt-dev RTOS:2.0.0 RTOS:x86_64-deprecated RTOS:1.0.4 RTOS:API-master-01-03--release-2014-08-10 RTOS:API-experimental-01-03--release-2014-08-10 RTOS:API-experimental-01-03--release-2014-07-29 RTOS:API-master-01-03--release-2014-07-29 RTOS:1.0.3 Imagelibrary:15.0.0 Imagelibrary:microkit-pre-2.1.0 Imagelibrary:14.0.0 Imagelibrary:13.0.0 Imagelibrary:12.1.0 Imagelibrary:12.0.0 Imagelibrary:11.0.0 Imagelibrary:10.1.1-mcs Imagelibrary:10.1.1 Imagelibrary:10.1.0 Imagelibrary:mcs-tutorials Imagelibrary:10.0.0-mcs Imagelibrary:10.0.0 Imagelibrary:9.0.1 Imagelibrary:9.0.0-mcs Imagelibrary:9.0.0 Imagelibrary:8.0.0 Imagelibrary:7.0.0 Imagelibrary:6.0.0 Imagelibrary:5.2.0-mcs Imagelibrary:5.2.0 Imagelibrary:5.1.0 Imagelibrary:5.0.0 Imagelibrary:4.0.0 Imagelibrary:rt-deprecated Imagelibrary:3.2.0 Imagelibrary:arm_hyp-deprecated Imagelibrary:3.1.0 Imagelibrary:1.0.0-rt-dev Imagelibrary:experimental-deprecated Imagelibrary:3.0.1 Imagelibrary:3.0.0 Imagelibrary:2.1.0 Imagelibrary:0.0.1-rt-dev Imagelibrary:2.0.0 Imagelibrary:x86_64-deprecated Imagelibrary:1.0.4 Imagelibrary:API-master-01-03--release-2014-08-10 Imagelibrary:API-experimental-01-03--release-2014-08-10 Imagelibrary:API-experimental-01-03--release-2014-07-29 Imagelibrary:API-master-01-03--release-2014-07-29 Imagelibrary:1.0.3

3 Commits
10.1.0 ... 10.1.1

Author SHA1 Message Date
Bamboo
57e5417ce2 Release 10.1.1 
Update VERSION
Update CHANGES
 2018-11-12 05:17:02 +11:00
Rafal Kolanski
d12bb374ab remove theoretical uninitialised variable use in infer_cpu_gic_id 
The C semantics used by our binary correctness mechanism understand
uninitialised variables as non-deterministic assignment. The translation
to a simplified form suitable for further analysis occurs on a
per-function basis which does not support non-determinism. This means
uninitialised local variables must not be used for decision making in
any function.

In infer_cpu_gic_id, 'target' is initialised in the loop, which will not
be executed if nirqs <= 0, after which the uninitialised 'target' is
examined. We address this by initialising 'target' to 0.

The overall C code is still safe, as infer_cpu_gic_id is only called
once in dist_init, where 0 < nirqs.
 2018-11-08 16:28:55 +11:00
Bamboo
7d16e3dcae Update VERSION file to 10.1.0-dev 2018-11-07 14:47:15 +11:00
3 changed files with 11 additions and 2 deletions
Expand all files Collapse all files

9
CHANGES
View File

@@ -14,6 +14,15 @@ Upcoming release: BINARY COMPATIBLE
## Upgrade Notes
---
10.1.1 2018-11-12: BINARY COMPATIBLE
## Changes
* Remove theoretical uninitialised variable use in infer_cpu_gic_id for binary translation validation
## Upgrade Notes
* 10.1.0 has a known broken test in the proofs. 10.1.1 fixes this test.
---
10.1.0 2018-11-07: SOURCE COMPATIBLE

2
VERSION
View File

@@ -1 +1 @@
10.1.0
10.1.1

2
src/arch/arm/machine/gic_pl390.c
View File

@@ -53,7 +53,7 @@ BOOT_CODE static uint8_t
infer_cpu_gic_id(int nirqs)
{
word_t i;
uint32_t target;
uint32_t target = 0;
for (i = 0; i < nirqs; i += 4) {
target = gic_dist->targets[i >> 2];
target |= target >> 16;