Upgrading to gcc4.8 worked. I also noticed this was covered in http://sel4.systems/Download/DebianToolChain.pml#Ubuntu which I didnt notice earlier. oops. On Wed, Jul 30, 2014 at 3:43 PM, Peter Chubb wrote:

...

...

...

...

...

"Tim" == Tim Newsham writes:

Tim> I'm getting an error Tim> when building from Ubuntu.

Tim> [KERNEL] [CC] kernel_final.s Tim> src/sel4/sel4test/kernel/src/arch/ia32/kernel/vspace.c: In Tim> function ‘init_boot_pd’: Tim> src/sel4/sel4test/kernel/src/arch/ia32/kernel/vspace.c:58:23: Tim> error: array subscript is above array bounds Tim> [-Werror=array-bounds] cc1: all warnings being treated as errors Tim> make[1]: *** [kernel_final.s] Error 1 make: *** [kernel_elf] Tim> Error 2

That's the error one sees when building with the default compiler (gcc 4.6 IIRC) on Ubuntu Precise. Either install gcc 4.8, or upgrade to Trusty.

The error doesn't make sense, if you look at the code. It's something like p->word[0] = 0;

where p is defined as pde_t *, and a pde_t has int word[1]; as a member.

-- Dr Peter Chubb peter.chubb AT nicta.com.au http://www.ssrg.nicta.com.au Software Systems Research Group/NICTA

-- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com