Originally building the kernel was largely considered to be done in
one of two ways
1. Release build with no assertions, no debug symbols and no printing.
   This was generally considered to be a 'verified' build
2. Debug build with assertions, debug symbols and printing

Since then various options were added, such as the 'code injection'
option, which we wanted on builds that did not have assertions or
other options that affected performance. As such it did not depend
upon a debug build and had large warning signs saying that enabling
this in a release build would not give you a verified or trusted
kernel.

Most recently the ability to print from the kernel in release mode
was added. For the same reason that tying the ability to print with
the performance reduction of various debugging was not always desireable.

This change attempts to unify the current state and have a single top
level option to enable a 'verification friendly' build. All other
options (assertions, printing, code injection) then depend upon
this configuration not being set.

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.