Hello
I ran into the following issue while running seL4test suite on Odroid-XU4:
Exynos5422 # fatload mmc 0 0x48000000
sel4test-driver-image-arm-exynos5
there are pending interrupts
0x00000001
reading
sel4test-driver-image-arm-exynos5
3149364 bytes
read
Exynos5422 # bootelf
0x48000000
## Starting application at 0x41000000
...
ELF-loader started on CPU: ARM Ltd. Cortex-A7
r0p3
Switching
CPU...
ELF-loader started on CPU: ARM Ltd. Cortex-A15
r2p3
paddr=[41000000..4130441f]
ELF-loading image
'kernel'
paddr=[60000000..60037fff]
vaddr=[e0000000..e0037fff]
virt_entry=e0000000
ELF-loading image
'sel4test-driver'
paddr=[60038000..60411fff]
vaddr=[10000..3e9fff]
virt_entry=1e74c
Enabling MMU and
paging
Jumping to kernel-image entry
point...
Bootstrapping
kernel
Kernel init: Too many untyped regions for boot
info
Kernel init: Too many untyped regions for boot
info
Kernel init: Too many untyped regions for boot info
....
1 untypeds of size
10
1 untypeds of size
11
126 untypeds of size
12
2 untypeds of size
13
3 untypeds of size
14
3 untypeds of size
15
5 untypeds of size
16
3 untypeds of size
17
3 untypeds of size
18
3 untypeds of size
19
3 untypeds of size
20
2 untypeds of size
21
2 untypeds of size
22
1 untypeds of size
23
2 untypeds of size
24
2 untypeds of size
25
2 untypeds of size
26
2 untypeds of size
27
1 untypeds of size 29
Switching to a safer, bigger
stack...
seL4
Test
=========
_allocman_utspace_alloc@allocman.c:301 Regular utspace alloc failed and not
watermark for size 31 type 0
vka_alloc_object_at@object.h:57 Failed to allocate object of size
2147483648, error 1
_allocman_utspace_alloc@allocman.c:301 Regular utspace alloc failed and not
watermark for size 30 type 0
vka_alloc_object_at@object.h:57 Failed to allocate object of size
1073741824, error 1
_allocman_utspace_alloc@allocman.c:301 Regular utspace alloc failed and not
watermark for size 29 type 0
vka_alloc_object_at@object.h:57 Failed to allocate object of size
536870912, error 1
.....
_utspace_split_alloc@split.c:247 Failed to find any untyped capable of
creating an object at address 0x12dd0000
vka_alloc_object_at@object.h:64 Failed to allocate object of size 4096 at
paddr 0x12dd0000, error 1
init_timer_caps@main.c:348 [Cond failed:
error]
Failed to get untyped at paddr 0x12dd0000 for
timer
Ignoring call to
sys_rt_sigprocmask
Ignoring call to
sys_gettid
sys_tkill assuming self kill
HYP mode is enabled, and seL4test suite is compiled in Debug Mode. Prior to
running seL4test, I ran code from seL4 tutorials and those ran w/o any
problems. Any suggestions on what I might have done wrong?
Thanks
