This makes it possible to statically check if the kernel is the master
kernel from user level. This is useful when when writing user level code
that's expected to work with different kernel versions.

* commit 'e7c6140c':
  Benchmarks: Add definition of seL4_LogBufferSize to x86

They would get shifted by the size of the type rather than the
size of the word. This wasn't detected initially as the master
branch of the kernel does not have any double word types in the API.

Updates SELFOUR-446

This patch just reorders the code, to actually do the check if there are any
modules (represented by `mod_count`) before any setup or lookup is done.

`syscall_stub_gen` has hardcoded constants for word size, this patch removes
that constraint and makes the word size an argument to the program instead.
The word size can either be passed either as command line arugmemt (-w option)
or a path to the build configuration file can be given(-c option) and the
generator will use the value of `CONFIG_WORD_SIZE` instead.
The `Makefile` in `libsel4` calls the generator with the configuration file as
an option.

Ideally, the architecture should be determined from the configration file, but
since we don't have unit tests for the generator, I will make one change at a
time.

This commit also includes a few changes to make it Python 2.7 compliant.

* commit 'b9410822':
  arm/tk1: add support for Nvidia Tegra K1 board

Apologies, some final adjustments got lost in the previous pull
request round. This version actually works.

* commit '13715658':
  Verification: bf: use new proof features.

Inline text blocks are not permitted without extra spacing in literate
Haskell files. This tweak makes the Haskell kernel build again.

The plan here is to move some of the proof script complexity embedded
in the text of the bitfield_gen utility into generic proof helpers in the
l4v repository that bitfield_gen can use more modularly. This is a simple
first step.

* commit '3554358c':
  Use correct version file in manual.tex

The type of irq_t differs per platform, this commit just forces
a conversion to an int, which should be sufficient for a debug
message

* commit '9ae867cb':
  SELFOUR-435: change kernel timer from GPT11 to 9

GPT1-9 are configured by uboot to run at 13Mhz,
while GPT10-11 are not and run with a much slower clock.

* commit '289bf92b':
  SELFOUR-114: remove bootinfo.h duplication

* commit '602f5369':
  x86: Change some PHYS_CODE to BOOT_CODE

* commit '2027e2e3':
  SELFOUR-251 Add descriptions of the seL4_Page_GetAddress_t

* commit 'd2030938':
  Added API documentation for the ARM cache flushing functions.

The functions pit_init and pit_wait_wraparound were previously marked as
PHYS_CODE, despite being called from BOOT_CODE elsewhere. This bug has
been present for some time but can be masked by the compiler inlining
all the involved functions, which is what typically happens.

SELFOUR-262

Previously the external build system was relied upon for disablingdisabling sse.
This is not desirable as it has the affect of disabling sse for the entire user
level build. Instead, since we only want to disable it for the kernel, we will
disable it here in the kernel Makefile

Diminish rights were to prevent a user from sending a writeable
cap over a read only endpoint. It turns out this 'security' can
be worked around without difficulty (by putting caps in a cnode
and sending the cnode) making the current diminish rights
implementation functionally useless.

Removing diminish rights has the benefit of simplifying all the
IPC paths.

Newline for latex compilation. This one isn't strictly required but will clash with the regression test.