diff --git a/libsel4/Makefile b/libsel4/Makefile
index 529bdff047e1002bd19b7e5eebf1e67108d9d252..c1324561bbf13ff3650d7c3aeed6d8290ba9ff27 100644
--- a/libsel4/Makefile
+++ b/libsel4/Makefile
@@ -113,4 +113,4 @@ include/interfaces/sel4_client.h: \
 	@${CHANGED_PATH} $@ \
         python ${SOURCE_DIR}/tools/syscall_stub_gen.py \
         --buffer \
-        -a $(SEL4_ARCH) -o $@ $^
+        -a $(SEL4_ARCH) -c ${srctree}/.config -o $@ $^
diff --git a/libsel4/tools/syscall_stub_gen.py b/libsel4/tools/syscall_stub_gen.py
index 92816b1cb8b160499414604dcd9e70ead1ec8c95..c2784613aead32c9dba48ec670879e4a2b92a0f8 100644
--- a/libsel4/tools/syscall_stub_gen.py
+++ b/libsel4/tools/syscall_stub_gen.py
@@ -35,12 +35,6 @@
 #     object's size wrong, which should help mitigate the number of bugs caused
 #     because of this script becoming out of date compared to the source files.
 #
-#   * The word-size is fixed at 32 bits, and we may implicitly assume that
-#     sizeof(int) == sizeof(long) == 32.
-#
-#     Though the constant 'WORD_SIZE_BITS' has been used throughout, there
-#     may be implicit assumptions hanging around causing things to fail.
-#
 #   * The script has only been tested on the actual seL4 API XML description.
 #
 #     No stress testing has taken place; there may be bugs if new and wonderful
@@ -48,12 +42,21 @@
 #
 
 import xml.dom.minidom
-import optparse
+from argparse import ArgumentParser
+import sys
 
 # Number of bits in a standard word
 WORD_SIZE_BITS_ARCH = {
     "aarch32": 32,
     "ia32": 32,
+    "aarch64": 64,
+    "ia64": 64,
+    "x86_64": 64
+}
+
+MESSAGE_REGISTERS_FOR_ARCH = {
+    "aarch32": 4,
+    "ia32": 2,
 }
 
 WORD_CONST_SUFFIX_BITS = {
@@ -64,11 +67,6 @@ WORD_CONST_SUFFIX_BITS = {
 # Maximum number of words that will be in a message.
 MAX_MESSAGE_LENGTH = 32
 
-MESSAGE_REGISTERS_FOR_ARCH = {
-    "aarch32": 4,
-    "ia32": 2,
-}
-
 # Headers to include
 INCLUDES = [
     'autoconf.h', 'sel4/types.h'
@@ -87,7 +85,7 @@ class Type(object):
     pointer.
     """
 
-    def __init__(self, name, size_bits, double_word=False, native_size_bits=None):
+    def __init__(self, name, size_bits, wordsize, double_word=False, native_size_bits=None):
         """
         Define a new type, named 'name' that is 'size_bits' bits
         long.
@@ -95,6 +93,7 @@ class Type(object):
 
         self.name = name
         self.size_bits = size_bits
+        self.wordsize = wordsize
         self.double_word = double_word
 
         #
@@ -110,7 +109,7 @@ class Type(object):
             self.native_size_bits = size_bits
 
     def pass_by_reference(self):
-        return self.size_bits > WORD_SIZE_BITS and not self.double_word
+        return self.size_bits > self.wordsize and not self.double_word
 
     def render_parameter_name(self, name):
         """
@@ -124,7 +123,7 @@ class Type(object):
         Return a new Type class representing a pointer to this
         object.
         """
-        return PointerType(self)
+        return PointerType(self, self.wordsize)
 
     def c_expression(self, var_name, word_num=0):
         """
@@ -136,20 +135,21 @@ class Type(object):
 
     def double_word_expression(self, var_name, word_num):
 
-        assert(word_num == 0 or word_num == 1)
-        
+        assert word_num == 0 or word_num == 1
+
         if word_num == 0:
-            return "({0}) {1}".format(TYPES[WORD_SIZE_BITS], var_name)
+            return "({0}) {1}".format(TYPES[self.size_bits], var_name)
         elif word_num == 1:
-            return "({0}) ({1} >> {2})".format(TYPES[WORD_SIZE_BITS], var_name, WORD_SIZE_BITS)
-        
+            return "({0}) ({1} >> {2})".format(TYPES[self.size_bits], var_name,
+                                               self.size_bits)
+
 
 class PointerType(Type):
     """
     A pointer to a standard type.
     """
-    def __init__(self, base_type):
-        Type.__init__(self, base_type.name, WORD_SIZE_BITS)
+    def __init__(self, base_type, wordsize):
+        Type.__init__(self, base_type.name, wordsize, wordsize)
         self.base_type = base_type
 
     def render_parameter_name(self, name):
@@ -166,18 +166,18 @@ class CapType(Type):
     """
     A type that is just a typedef of seL4_CPtr.
     """
-    def __init__(self, name):
-        Type.__init__(self, name, WORD_SIZE_BITS)
+    def __init__(self, name, wordsize):
+        Type.__init__(self, name, wordsize, wordsize)
 
 class StructType(Type):
     """
     A C 'struct' definition.
     """
-    def __init__(self, name, size_bits):
-        Type.__init__(self, name, size_bits)
+    def __init__(self, name, size_bits, wordsize):
+        Type.__init__(self, name, size_bits, wordsize)
 
     def c_expression(self, var_name, word_num, member_name):
-        assert word_num < self.size_bits / WORD_SIZE_BITS
+        assert word_num < self.size_bits / self.wordsize
 
         # Multiword structure.
         assert self.pass_by_reference()
@@ -187,80 +187,80 @@ class BitFieldType(Type):
     """
     A special C 'struct' generated by the bitfield generator
     """
-    def __init__(self, name, size_bits):
-        Type.__init__(self, name, size_bits)
-    
+    def __init__(self, name, size_bits, wordsize):
+        Type.__init__(self, name, size_bits, wordsize)
+
     def c_expression(self, var_name, word_num=0):
-        
+
         return "%s.words[%d]" % (var_name, word_num)
-        
+
 class Parameter(object):
     def __init__(self, name, type):
         self.name = name
         self.type = type
 
 #
-# Return the size (in bits) of a particular type.
+# Types
 #
-def InitTypes():
-    global types
-    global arch_types
+def init_data_types(wordsize):
     types = [
         # Simple Types
-        Type("int", WORD_SIZE_BITS),
+        Type("int", wordsize, wordsize),
 
-        Type("seL4_Uint8", 8),
-        Type("seL4_Uint16", 16),
-        Type("seL4_Uint32", 32),
-        Type("seL4_Uint64", 64, double_word=(WORD_SIZE_BITS == 32)),
-        Type("seL4_Word", WORD_SIZE_BITS),
-        Type("seL4_Bool", 1, native_size_bits=8),
-        Type("seL4_CapRights", WORD_SIZE_BITS),
+        Type("seL4_Uint8", 8, wordsize),
+        Type("seL4_Uint16", 16, wordsize),
+        Type("seL4_Uint32", 32, wordsize),
+        Type("seL4_Uint64", 64, wordsize, double_word=(wordsize == 32)),
+        Type("seL4_Word", wordsize, wordsize),
+        Type("seL4_Bool", 1, wordsize, native_size_bits=8),
+        Type("seL4_CapRights", wordsize, wordsize),
 
         # seL4 Structures
-        BitFieldType("seL4_CapData_t", WORD_SIZE_BITS),
+        BitFieldType("seL4_CapData_t", wordsize, wordsize),
 
         # Object types
-        CapType("seL4_CPtr"),
-        CapType("seL4_CNode"),
-        CapType("seL4_IRQHandler"),
-        CapType("seL4_IRQControl"),
-        CapType("seL4_TCB"),
-        CapType("seL4_Untyped"),
-        CapType("seL4_DomainSet"),
+        CapType("seL4_CPtr", wordsize),
+        CapType("seL4_CNode", wordsize),
+        CapType("seL4_IRQHandler", wordsize),
+        CapType("seL4_IRQControl", wordsize),
+        CapType("seL4_TCB", wordsize),
+        CapType("seL4_Untyped", wordsize),
+        CapType("seL4_DomainSet", wordsize),
     ]
 
-    #
-    # Arch-specific types.
-    #
+    return types
+
+def init_arch_types(wordsize):
     arch_types = {
         "aarch32" : [
-            Type("seL4_ARM_VMAttributes", WORD_SIZE_BITS),
-            CapType("seL4_ARM_Page"),
-            CapType("seL4_ARM_PageTable"),
-            CapType("seL4_ARM_PageDirectory"),
-            CapType("seL4_ARM_ASIDControl"),
-            CapType("seL4_ARM_ASIDPool"),
-            StructType("seL4_UserContext", WORD_SIZE_BITS * 17),
+            Type("seL4_ARM_VMAttributes", wordsize, wordsize),
+            CapType("seL4_ARM_Page", wordsize),
+            CapType("seL4_ARM_PageTable", wordsize),
+            CapType("seL4_ARM_PageDirectory", wordsize),
+            CapType("seL4_ARM_ASIDControl", wordsize),
+            CapType("seL4_ARM_ASIDPool", wordsize),
+            StructType("seL4_UserContext", wordsize * 17, wordsize),
         ],
 
         "ia32" : [
-            Type("seL4_X86_VMAttributes", WORD_SIZE_BITS),
-            CapType("seL4_X86_IOPort"),
-            CapType("seL4_X86_ASIDControl"),
-            CapType("seL4_X86_ASIDPool"),
-            CapType("seL4_X86_IOSpace"),
-            CapType("seL4_X86_Page"),
-            CapType("seL4_X86_PageDirectory"),
-            CapType("seL4_X86_PageTable"),
-            CapType("seL4_X86_IOPageTable"),
-            StructType("seL4_UserContext", WORD_SIZE_BITS * 13),
+            Type("seL4_X86_VMAttributes", wordsize, wordsize),
+            CapType("seL4_X86_IOPort", wordsize),
+            CapType("seL4_X86_ASIDControl", wordsize),
+            CapType("seL4_X86_ASIDPool", wordsize),
+            CapType("seL4_X86_IOSpace", wordsize),
+            CapType("seL4_X86_Page", wordsize),
+            CapType("seL4_X86_PageDirectory", wordsize),
+            CapType("seL4_X86_PageTable", wordsize),
+            CapType("seL4_X86_IOPageTable", wordsize),
+            StructType("seL4_UserContext", wordsize * 13, wordsize),
         ]
     }
 
+    return arch_types
+
 # Retrieve a member list for a given struct type
-def struct_members(type, structs):
-    members = [member for struct_name, member in structs if struct_name == type.name]
+def struct_members(typ, structs):
+    members = [member for struct_name, member in structs if struct_name == typ.name]
     assert len(members) == 1
     return members[0]
 
@@ -270,7 +270,7 @@ def align_up(x, a):
         return x
     return x + a - (x % a)
 
-def get_parameter_positions(parameters):
+def get_parameter_positions(parameters, wordsize):
     """
     Determine where each parameter should be packed in the generated message.
     We generate a list of:
@@ -281,7 +281,6 @@ def get_parameter_positions(parameters):
 
     We guarantee that either (num_words == 1) or (bit_offset == 0).
     """
-    words_used = 0
     bits_used = 0
     results = []
 
@@ -290,10 +289,10 @@ def get_parameter_positions(parameters):
         type_size = param.type.size_bits
 
         # We need everything to be a power of two, or word sized.
-        assert ((type_size & (type_size - 1)) == 0) or (type_size % WORD_SIZE_BITS == 0)
+        assert ((type_size & (type_size - 1)) == 0) or (type_size % wordsize == 0)
 
         # Align up to our own size, or the next word. (Whichever is smaller)
-        bits_used = align_up(bits_used, min(type_size, WORD_SIZE_BITS))
+        bits_used = align_up(bits_used, min(type_size, wordsize))
 
         # Place ourself.
         results.append((param, bits_used, type_size))
@@ -316,7 +315,7 @@ def generate_param_list(input_params, output_params):
     return ", ".join(params)
 
 
-def generate_marshal_expressions(params, num_mrs, structs):
+def generate_marshal_expressions(params, num_mrs, structs, wordsize):
     """
     Generate marshalling expressions for the given set of inputs.
 
@@ -324,7 +323,7 @@ def generate_marshal_expressions(params, num_mrs, structs):
     to marshal all the inputs.
     """
 
-    def generate_param_code(param, first_bit, num_bits, word_array):
+    def generate_param_code(param, first_bit, num_bits, word_array, wordsize):
         """
         Generate code to marshal the given parameter into the correct
         location in the message.
@@ -335,8 +334,8 @@ def generate_marshal_expressions(params, num_mrs, structs):
         be bitwise-or'ed into it.
         """
 
-        target_word = first_bit / WORD_SIZE_BITS
-        target_offset = first_bit % WORD_SIZE_BITS
+        target_word = first_bit / wordsize
+        target_offset = first_bit % wordsize
 
         # double word type
         if param.type.double_word:
@@ -345,16 +344,17 @@ def generate_marshal_expressions(params, num_mrs, structs):
             return
 
         # Single full word?
-        if num_bits == WORD_SIZE_BITS:
+        if num_bits == wordsize:
             assert target_offset == 0
-            expr = param.type.c_expression(param.name);
+            expr = param.type.c_expression(param.name)
             word_array[target_word].append(expr)
             return
 
         # Part of a word?
-        if num_bits < WORD_SIZE_BITS:
-            expr = param.type.c_expression(param.name);
-            expr = "(%s & %#x%s)" % (expr, (1 << num_bits) - 1, WORD_CONST_SUFFIX)
+        if num_bits < wordsize:
+            expr = param.type.c_expression(param.name)
+            expr = "(%s & %#x%s)" % (expr, (1 << num_bits) - 1,
+                                     WORD_CONST_SUFFIX_BITS[wordsize])
             if target_offset:
                 expr = "(%s << %d)" % (expr, target_offset)
             word_array[target_word].append(expr)
@@ -362,24 +362,24 @@ def generate_marshal_expressions(params, num_mrs, structs):
 
         # Multiword array
         assert target_offset == 0
-        num_words = num_bits / WORD_SIZE_BITS
+        num_words = num_bits / wordsize
         for i in range(num_words):
-            expr = param.type.c_expression(param.name, i, struct_members(param.type, structs));
+            expr = param.type.c_expression(param.name, i, struct_members(param.type, structs))
             word_array[target_word + i].append(expr)
 
 
     # Get their marshalling positions
-    positions = get_parameter_positions(params)
+    positions = get_parameter_positions(params, wordsize)
 
     # Generate marshal code.
     words = [[] for _ in range(num_mrs, MAX_MESSAGE_LENGTH)]
     for (param, first_bit, num_bits) in positions:
-        generate_param_code(param, first_bit, num_bits, words)
+        generate_param_code(param, first_bit, num_bits, words, wordsize)
 
     # Return list of expressions.
     return [" | ".join(x) for x in words if len(x) > 0]
 
-def generate_unmarshal_expressions(params):
+def generate_unmarshal_expressions(params, wordsize):
     """
     Generate unmarshalling expressions for the given set of outputs.
 
@@ -390,37 +390,37 @@ def generate_unmarshal_expressions(params):
     in them, indicating a read from a word in the message.
     """
 
-    def unmarshal_single_param(first_bit, num_bits):
+    def unmarshal_single_param(first_bit, num_bits, wordsize):
         """
         Unmarshal a single parameter.
         """
-        first_word = first_bit / WORD_SIZE_BITS
-        bit_offset = first_bit % WORD_SIZE_BITS
+        first_word = first_bit / wordsize
+        bit_offset = first_bit % wordsize
 
         # Multiword type?
-        if num_bits > WORD_SIZE_BITS:
+        if num_bits > wordsize:
             result = []
-            for x in range(num_bits / WORD_SIZE_BITS):
+            for x in range(num_bits / wordsize):
                 result.append("%%(w%d)s" % (x + first_word))
             return result
 
         # Otherwise, bit packed.
-        if num_bits == WORD_SIZE_BITS:
+        if num_bits == wordsize:
             return ["%%(w%d)s" % first_word]
         elif bit_offset == 0:
             return ["(%%(w%d)s & %#x)" % (
-                    first_word, (1 << num_bits) - 1)]
+                first_word, (1 << num_bits) - 1)]
         else:
             return ["(%%(w%d)s >> %d) & %#x" % (
-                    first_word, bit_offset, (1 << num_bits) - 1)]
+                first_word, bit_offset, (1 << num_bits) - 1)]
 
     # Get their marshalling positions
-    positions = get_parameter_positions(params)
+    positions = get_parameter_positions(params, wordsize)
 
     # Generate the unmarshal code.
     results = []
     for (param, first_bit, num_bits) in positions:
-        results.append((param, unmarshal_single_param(first_bit, num_bits)))
+        results.append((param, unmarshal_single_param(first_bit, num_bits, wordsize)))
     return results
 
 def generate_result_struct(interface_name, method_name, output_params):
@@ -461,12 +461,12 @@ def generate_result_struct(interface_name, method_name, output_params):
             result.append("\t%s;" % i.type.render_parameter_name(i.name))
     result.append("};")
     result.append("typedef struct %s_%s %s_%s_t;" % (
-            (interface_name, method_name, interface_name, method_name)))
+        (interface_name, method_name, interface_name, method_name)))
     result.append("")
 
     return "\n".join(result)
 
-def generate_stub(arch, interface_name, method_name, method_id, input_params, output_params, structs, use_only_ipc_buffer):
+def generate_stub(arch, wordsize, interface_name, method_name, method_id, input_params, output_params, structs, use_only_ipc_buffer):
     result = []
 
     if use_only_ipc_buffer:
@@ -501,13 +501,14 @@ def generate_stub(arch, interface_name, method_name, method_id, input_params, ou
     #
     result.append("LIBSEL4_INLINE %s" % return_type)
     result.append("%s_%s(%s)" % (interface_name, method_name,
-        generate_param_list(input_params, output_params)))
+                                 generate_param_list(input_params, output_params)))
     result.append("{")
 
     #
     # Get a list of expressions for our caps and inputs.
     #
-    input_expressions = generate_marshal_expressions(standard_params, num_mrs, structs)
+    input_expressions = generate_marshal_expressions(standard_params, num_mrs,
+                                                     structs, wordsize)
     cap_expressions = [x.name for x in cap_params]
     service_cap = cap_expressions[0]
     cap_expressions = cap_expressions[1:]
@@ -516,7 +517,7 @@ def generate_stub(arch, interface_name, method_name, method_id, input_params, ou
     # Compute how many words the inputs and output will require.
     #
     input_param_words = len(input_expressions)
-    output_param_words = sum([p.type.size_bits for p in output_params]) / WORD_SIZE_BITS
+    output_param_words = sum([p.type.size_bits for p in output_params]) / wordsize
 
     #
     # Setup variables we will need.
@@ -573,7 +574,7 @@ def generate_stub(arch, interface_name, method_name, method_id, input_params, ou
         result.append("\t/* Perform the call, passing in-register arguments directly. */")
         result.append("\toutput_tag = seL4_CallWithMRs(%s, tag," % (service_cap))
         result.append("\t\t%s);" % ', '.join(
-                [call_arguments[i] for i in range(num_mrs)]))
+            [call_arguments[i] for i in range(num_mrs)]))
     result.append("")
 
     #
@@ -584,18 +585,21 @@ def generate_stub(arch, interface_name, method_name, method_id, input_params, ou
         source_words = {}
         for i in range(MAX_MESSAGE_LENGTH):
             if i < num_mrs:
-                source_words["w%d" % i] = "mr%d" % i;
+                source_words["w%d" % i] = "mr%d" % i
             else:
-                source_words["w%d" % i] = "seL4_GetMR(%d)" % i;
-        unmashalled_params = generate_unmarshal_expressions(output_params)
+                source_words["w%d" % i] = "seL4_GetMR(%d)" % i
+        unmashalled_params = generate_unmarshal_expressions(output_params, wordsize)
         for (param, words) in unmashalled_params:
             if param.type.pass_by_reference():
-                members = struct_members(param.type, structs);
+                members = struct_members(param.type, structs)
                 for i in range(len(words)):
-                    result.append("\t%s->%s = %s;" % (param.name, members[i], words[i] % source_words))
+                    result.append("\t%s->%s = %s;" %
+                                  (param.name, members[i], words[i] % source_words))
             else:
                 if param.type.double_word:
-                    result.append("\tresult.%s = ((%s)%s + ((%s)%s << 32));" % (param.name, TYPES[64], words[0] % source_words, TYPES[64], words[1] % source_words))
+                    result.append("\tresult.%s = ((%s)%s + ((%s)%s << 32));" %
+                                  (param.name, TYPES[64], words[0] % source_words,
+                                   TYPES[64], words[1] % source_words))
                 else:
                     for word in words:
                         result.append("\tresult.%s = %s;" % (param.name, word % source_words))
@@ -632,12 +636,12 @@ def parse_xml_file(input_file, valid_types):
     doc = xml.dom.minidom.parse(input_file)
 
     for struct in doc.getElementsByTagName("struct"):
-        struct_members = []
+        _struct_members = []
         struct_name = struct.getAttribute("name")
         for members in struct.getElementsByTagName("member"):
             member_name = members.getAttribute("name")
-            struct_members.append(member_name)
-        structs.append( (struct_name, struct_members) )
+            _struct_members.append(member_name)
+        structs.append((struct_name, _struct_members))
 
     for interface in doc.getElementsByTagName("interface"):
         interface_name = interface.getAttribute("name")
@@ -659,7 +663,7 @@ def parse_xml_file(input_file, valid_types):
                     raise Exception("Unknown type '%s'." % (param.getAttribute("type")))
                 param_dir = param.getAttribute("dir")
                 assert (param_dir == "in") or (param_dir == "out")
-                if (param_dir == "in"):
+                if param_dir == "in":
                     input_params.append(Parameter(param_name, param_type))
                 else:
                     output_params.append(Parameter(param_name, param_type))
@@ -667,28 +671,24 @@ def parse_xml_file(input_file, valid_types):
 
     return (methods, structs)
 
-def generate_stub_file(arch, input_files, output_file, use_only_ipc_buffer):
+def generate_stub_file(arch, wordsize, input_files, output_file, use_only_ipc_buffer):
     """
     Generate a header file containing system call stubs for seL4.
     """
     result = []
 
     # Ensure architecture looks sane.
-    if not arch in WORD_SIZE_BITS_ARCH.keys():
-        raise Exception("Invalid architecture. Expected %s.",
-                " or ".join(arch_types.keys()))
+    if arch not in WORD_SIZE_BITS_ARCH.keys():
+        raise Exception("Invalid architecture.")
 
-    global WORD_SIZE_BITS
-    global WORD_CONST_SUFFIX
-    WORD_SIZE_BITS = WORD_SIZE_BITS_ARCH[arch]
-    WORD_CONST_SUFFIX = WORD_CONST_SUFFIX_BITS[WORD_SIZE_BITS]
-    InitTypes()
+    data_types = init_data_types(wordsize)
+    arch_types = init_arch_types(wordsize)
 
     # Parse XML
     methods = []
     structs = []
-    for file in input_files:
-        method, struct = parse_xml_file(file, types + arch_types[arch])
+    for infile in input_files:
+        method, struct = parse_xml_file(infile, data_types + arch_types[arch])
         methods += method
         structs += struct
 
@@ -700,10 +700,10 @@ def generate_stub_file(arch, input_files, output_file, use_only_ipc_buffer):
 
 #ifndef __LIBSEL4_SEL4_CLIENT_H
 #define __LIBSEL4_SEL4_CLIENT_H
-""");
+""")
 
     # Emit the includes
-    result.append('\n'.join(map(lambda x: '#include <%s>' % x, INCLUDES)))
+    result.append('\n'.join(['#include <%s>' % include for include in INCLUDES]))
 
     #
     # Emit code to ensure that all of our type sizes are consistent with
@@ -721,7 +721,7 @@ def generate_stub_file(arch, input_files, output_file, use_only_ipc_buffer):
         typedef unsigned long __type_##type##_size_incorrect[ \\
                 (sizeof(type) == expected_bytes) ? 1 : -1]
 """)
-    for x in types + arch_types[arch]:
+    for x in data_types + arch_types[arch]:
         result.append("assert_size_correct(%s, %d);" % (x.name, x.native_size_bits / 8))
     result.append("")
 
@@ -746,8 +746,8 @@ def generate_stub_file(arch, input_files, output_file, use_only_ipc_buffer):
     result.append(" * Generated stubs.")
     result.append(" */")
     for (interface_name, method_name, method_id, inputs, outputs) in methods:
-        result.append(generate_stub(arch, interface_name, method_name,
-                method_id, inputs, outputs, structs, use_only_ipc_buffer))
+        result.append(generate_stub(arch, wordsize, interface_name, method_name,
+                                    method_id, inputs, outputs, structs, use_only_ipc_buffer))
 
     # Print footer.
     result.append("#endif /* __LIBSEL4_SEL4_CLIENT_H */")
@@ -758,32 +758,65 @@ def generate_stub_file(arch, input_files, output_file, use_only_ipc_buffer):
     output.write("\n".join(result))
     output.close()
 
+def process_args():
+    usage_str = """
+    %(prog)s [OPTIONS] [FILES] """
+    epilog_str = """
+
+    """
+    parser = ArgumentParser(description='seL4 System Call Stub Generator.',
+                            usage=usage_str,
+                            epilog=epilog_str)
+    parser.add_argument("-o", "--output", dest="output", default="/dev/stdout",
+                        help="Output file to write stub to. (default: %(default)s).")
+    parser.add_argument("-b", "--buffer", dest="buffer", action="store_true", default=False,
+                        help="Use IPC buffer exclusively, i.e. do not pass syscall arguments by registers. (default: %(default)s)")
+    parser.add_argument("-a", "--arch", dest="arch", required=True, choices=WORD_SIZE_BITS_ARCH,
+                        help="Architecture to generate stubs for.")
+
+    wsizegroup = parser.add_mutually_exclusive_group()
+    wsizegroup.add_argument("-w", "--word-size", dest="wsize",
+                            help="Word size(in bits), for the platform.")
+    wsizegroup.add_argument("-c", "--cfile", dest="cfile",
+                            help="Config file for Kbuild, used to get Word size.")
+
+    parser.add_argument("files", metavar="FILES", nargs="+",
+                        help="Input XML files.")
+
+    return parser
+
 def main():
-    #
-    # Read command line arguments.
-    #
-    parser = optparse.OptionParser()
-    parser.add_option("-a", "--arch",
-            dest="arch", help="Architecture to generate stubs for.")
-    parser.add_option("-o", "--output",
-            dest="output", help="Output file to write stub to.")
-    parser.add_option("-b", "--buffer", action="store_true",
-            help="Use IPC buffer exclusively (i.e. do not pass syscall "
-            "arguments by registers).")
-    (options, args) = parser.parse_args()
-
-    # Validate arguments
-    if len(args) < 1:
-        parser.error("Require at least one input file.")
-    if not options.arch:
-        parser.error("Require an architecture to be specified.")
-    if not options.output:
-        options.output = "/dev/stdout"
-    input_files = args
+
+    parser = process_args()
+    args = parser.parse_args()
+
+    if not (args.wsize or args.cfile):
+        parser.error("Require either -w/--word-size or -c/--cfile argument.")
+        sys.exit(2)
+
+    # Get word size
+    wordsize = -1
+
+    if args.cfile:
+        try:
+            with open(args.cfile) as conffile:
+                for line in conffile:
+                    if line.startswith('CONFIG_WORD_SIZE'):
+                        wordsize = int(line.split('=')[1].strip())
+        except IndexError:
+            print "Invalid word size in configuration file."
+            sys.exit(2)
+    else:
+        wordsize = args.wsize
+
+    if wordsize is -1:
+        print "Invalid word size."
+        sys.exit(2)
 
     # Generate the stubs.
+    generate_stub_file(args.arch, wordsize, args.files, args.output, args.buffer)
 
-    generate_stub_file(options.arch, input_files, options.output, options.buffer)
 
-main()
+if __name__ == "__main__":
+    sys.exit(main())