bug 17392: remove trailing whitespace in source files

65 files changed, 530 insertions, 530 deletions

diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index 990f207d..a0a4fcc5 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -106,7 +106,7 @@ let memcpy_small_arg sz arg tmp =
       assert false
 
 let expand_builtin_memcpy_small sz al src dst =
-  let (tsrc, tdst) = 
+  let (tsrc, tdst) =
     if dst <> BA (IR IR2) then (IR2, IR3) else (IR3, IR2) in
   let (rsrc, osrc) = memcpy_small_arg sz src tsrc in
   let (rdst, odst) = memcpy_small_arg sz dst tdst in
@@ -142,7 +142,7 @@ let memcpy_big_arg arg tmp =
 let expand_builtin_memcpy_big sz al src dst =
   assert (sz >= al);
   assert (sz mod al = 0);
-  let (s, d) = 
+  let (s, d) =
     if dst <> BA (IR IR2) then (IR2, IR3) else (IR3, IR2) in
   memcpy_big_arg src s;
   memcpy_big_arg dst d;
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index b988f10f..4961f897 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -40,13 +40,13 @@ module type PRINTER_OPTIONS =
 module Target (Opt: PRINTER_OPTIONS) : TARGET =
   struct
 (* Code generation options. *)
-    
+
     let literals_in_code = ref true     (* to be turned into a proper option *)
-    
+
 (* Basic printing functions *)
-        
+
     let print_label oc lbl = elf_label oc (transl_label lbl)
-        
+
     let comment = "@"
 
     let symbol = elf_symbol
@@ -61,34 +61,34 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       | IR4 -> "r4" | IR5 -> "r5" | IR6 -> "r6" | IR7 -> "r7"
       | IR8 -> "r8" | IR9 -> "r9" | IR10 -> "r10" | IR11 -> "r11"
       | IR12 -> "r12" | IR13 -> "sp" | IR14 -> "lr"
-            
+
     let float_reg_name = function
       | FR0 -> "d0"  | FR1 -> "d1"  | FR2 -> "d2"  | FR3 -> "d3"
       | FR4 -> "d4"  | FR5 -> "d5"  | FR6 -> "d6"  | FR7 -> "d7"
       | FR8 -> "d8"  | FR9 -> "d9"  | FR10 -> "d10"  | FR11 -> "d11"
       | FR12 -> "d12"  | FR13 -> "d13"  | FR14 -> "d14"  | FR15 -> "d15"
-            
+
     let single_float_reg_index = function
       | FR0 -> 0  | FR1 -> 2  | FR2 -> 4  | FR3 -> 6
       | FR4 -> 8  | FR5 -> 10  | FR6 -> 12  | FR7 -> 14
       | FR8 -> 16  | FR9 -> 18  | FR10 -> 20  | FR11 -> 22
       | FR12 -> 24  | FR13 -> 26  | FR14 -> 28  | FR15 -> 30
-            
+
     let single_float_reg_name = function
       | FR0 -> "s0"  | FR1 -> "s2"  | FR2 -> "s4"  | FR3 -> "s6"
       | FR4 -> "s8"  | FR5 -> "s10"  | FR6 -> "s12"  | FR7 -> "s14"
       | FR8 -> "s16"  | FR9 -> "s18"  | FR10 -> "s20"  | FR11 -> "s22"
       | FR12 -> "s24"  | FR13 -> "s26"  | FR14 -> "s28"  | FR15 -> "s30"
-            
+
     let ireg oc r = output_string oc (int_reg_name r)
     let freg oc r = output_string oc (float_reg_name r)
     let freg_single oc r = output_string oc (single_float_reg_name r)
-        
+
     let preg oc = function
       | IR r -> ireg oc r
       | FR r -> freg oc r
       | _    -> assert false
-            
+
     let condition_name = function
       | TCeq -> "eq"
       | TCne -> "ne"
@@ -102,7 +102,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       | TClt -> "lt"
       | TCgt -> "gt"
       | TCle -> "le"
-            
+
     let neg_condition_name = function
       | TCeq -> "ne"
       | TCne -> "eq"
@@ -116,7 +116,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       | TClt -> "ge"
       | TCgt -> "le"
       | TCle -> "gt"
-            
+
 (* In Thumb2 mode, some arithmetic instructions have shorter encodings
    if they carry the "S" flag (update condition flags):
        add   (but not sp + imm)
@@ -158,27 +158,27 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       | Section_debug_abbrev -> ".section	.debug_abbrev,\"\",%progbits"
       | Section_debug_line _ -> ".section	.debug_line,\"\",%progbits"
       | Section_debug_str -> ".section	.debug_str,\"MS\",%progbits,1"
-            
+
     let section oc sec =
       fprintf oc "	%s\n" (name_of_section sec)
-        
+
 (* Record current code position and latest position at which to
    emit float and symbol constants. *)
-        
+
     let currpos = ref 0
     let size_constants = ref 0
     let max_pos_constants = ref max_int
-        
+
     let distance_to_emit_constants () =
       if !literals_in_code
       then !max_pos_constants - (!currpos + !size_constants)
       else max_int
-          
+
 (* Associate labels to floating-point constants and to symbols *)
-          
+
     let float_labels = (Hashtbl.create 39 : (int64, int) Hashtbl.t)
     let float32_labels = (Hashtbl.create 39 : (int32, int) Hashtbl.t)
-        
+
     let label_float bf =
       try
         Hashtbl.find float_labels bf
@@ -188,7 +188,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
         size_constants := !size_constants + 8;
         max_pos_constants := min !max_pos_constants (!currpos + 1024);
         lbl'
-          
+
     let label_float32 bf =
       try
         Hashtbl.find float32_labels bf
@@ -198,10 +198,10 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
         size_constants := !size_constants + 4;
         max_pos_constants := min !max_pos_constants (!currpos + 1024);
         lbl'
-          
+
     let symbol_labels =
       (Hashtbl.create 39 : (ident * Integers.Int.int, int) Hashtbl.t)
-        
+
     let label_symbol id ofs =
       try
         Hashtbl.find symbol_labels (id, ofs)
@@ -211,14 +211,14 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
         size_constants := !size_constants + 4;
         max_pos_constants := min !max_pos_constants (!currpos + 4096);
         lbl'
-          
+
     let reset_constants () =
       Hashtbl.clear float_labels;
       Hashtbl.clear float32_labels;
       Hashtbl.clear symbol_labels;
       size_constants := 0;
       max_pos_constants := max_int
-          
+
     let emit_constants oc =
       fprintf oc "	.balign	4\n";
       Hashtbl.iter
@@ -238,9 +238,9 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
             lbl symbol_offset (id, ofs))
         symbol_labels;
       reset_constants ()
-        
+
 (* Generate code to load the address of id + ofs in register r *)
-        
+
     let loadsymbol oc r id ofs =
       if !Clflags.option_mthumb then begin
         fprintf oc "	movw	%a, #:lower16:%a\n"
@@ -249,13 +249,13 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
           ireg r symbol_offset (id, ofs); 2
       end else begin
         let lbl = label_symbol id ofs in
-        fprintf oc "	ldr	%a, .L%d @ %a\n" 
+        fprintf oc "	ldr	%a, .L%d @ %a\n"
           ireg r lbl symbol_offset (id, ofs); 1
       end
-          
+
 (* Emit instruction sequences that set or offset a register by a constant. *)
 (* No S suffix because they are applied to SP most of the time. *)
-          
+
     let movimm oc dst n =
       match Asmgen.decompose_int n with
       | [] -> assert false
@@ -265,7 +265,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
             (fun n -> fprintf oc "	orr	%s, %s, #%a\n" dst dst coqint n)
             tl;
           List.length l
-            
+
     let addimm oc dst src n =
       match Asmgen.decompose_int n with
       | [] -> assert false
@@ -275,7 +275,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
             (fun n -> fprintf oc "	add	%s, %s, #%a\n" dst dst coqint n)
             tl;
           List.length l
-            
+
     let subimm oc dst src n =
       match Asmgen.decompose_int n with
       | [] -> assert false
@@ -285,27 +285,27 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
             (fun n -> fprintf oc "	sub	%s, %s, #%a\n" dst dst coqint n)
             tl;
           List.length l
-            
+
 (* Recognition of float constants appropriate for VMOV.
    a normalized binary floating point encoding with 1 sign bit, 4
    bits of fraction and a 3-bit exponent *)
-   
+
     let is_immediate_float64 bits =
       let exp = (Int64.(to_int (shift_right_logical bits 52)) land 0x7FF) - 1023 in
       let mant = Int64.logand bits 0xF_FFFF_FFFF_FFFFL in
       exp >= -3 && exp <= 4 && Int64.logand mant 0xF_0000_0000_0000L = mant
-        
+
    let is_immediate_float32 bits =
      let exp = (Int32.(to_int (shift_right_logical bits 23)) land 0xFF) - 127 in
      let mant = Int32.logand bits 0x7F_FFFFl in
      exp >= -3 && exp <= 4 && Int32.logand mant 0x78_0000l = mant
-       
+
 
 (* Emit .file / .loc debugging directives *)
-       
+
     let print_file_line oc file line =
       print_file_line oc comment file line
-        
+
     let print_location oc loc =
       if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc)
 
@@ -456,7 +456,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       match Opt.float_abi with
       | Soft -> (FixupEABI.fixup_arguments, FixupEABI.fixup_result)
       | Hard -> (FixupHF.fixup_arguments, FixupHF.fixup_result)
-            
+
 (* Printing of instructions *)
 
     let shift_op oc = function
@@ -494,7 +494,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
           fprintf oc "	b	%a\n" symbol id;
           n + 1
       | Pbreg(r, sg) ->
-          let n = 
+          let n =
             if r = IR14
             then fixup_result oc Outgoing sg
             else fixup_arguments oc Outgoing sg in
@@ -886,7 +886,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
             fprintf oc "	.space	%s\n" (Z.to_string n)
       | Init_addrof(symb, ofs) ->
           fprintf oc "	.word	%a\n" symbol_offset (symb, ofs)
-            
+
     let print_prologue oc =
       fprintf oc "	.syntax	unified\n";
       fprintf oc "	.arch	%s\n"
@@ -908,7 +908,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       end
 
 
-    let print_epilogue oc = 
+    let print_epilogue oc =
       if !Clflags.option_g then begin
         let high_pc = new_label () in
         Debug.add_compilation_section_end ".text" high_pc;
@@ -919,22 +919,22 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
 
 
     let default_falignment = 4
-    
+
     let label = elf_label
-       
+
     let new_label = new_label
   end
 
-let sel_target () = 
+let sel_target () =
   let module S : PRINTER_OPTIONS = struct
-   
+
    let vfpv3 = Configuration.model >= "armv7"
-   
+
    let float_abi = match Configuration.abi with
    | "eabi"      -> Soft
    | "hardfloat" -> Hard
    | _ -> assert false
-   
+
    let hardware_idiv  =
    match  Configuration.model with
    | "armv7r" | "armv7m" -> !Clflags.option_mthumb
diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml
index 3b77f135..3d1dd754 100644
--- a/backend/Asmexpandaux.ml
+++ b/backend/Asmexpandaux.ml
@@ -11,13 +11,13 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(* Util functions used for the expansion of built-ins and some 
+(* Util functions used for the expansion of built-ins and some
    pseudo-instructions *)
 
 open Asm
 open AST
 open Camlcoq
-       
+
 (* Buffering the expanded code *)
 
 let current_code = ref ([]: instruction list)
@@ -25,7 +25,7 @@ let current_code = ref ([]: instruction list)
 let emit i = current_code := i :: !current_code
 
 (* Generation of fresh labels *)
-							  
+
 let dummy_function = { fn_code = []; fn_sig = signature_main }
 let current_function = ref dummy_function
 let next_label = ref (None: label option)
@@ -46,7 +46,7 @@ let new_label () =
     next_label := Some (P.succ lbl);
     lbl
 
-		     
+
 let set_current_function f =
   current_function := f; next_label := None; current_code := []
 
@@ -64,7 +64,7 @@ let expand_scope id lbl oldscopes newscopes =
   List.iter (fun i -> Debug.open_scope id i lbl) opening;
   List.iter (fun i -> Debug.close_scope id i lbl) closing
 
-let translate_annot sp preg_to_dwarf annot = 
+let translate_annot sp preg_to_dwarf annot =
   let rec aux = function
     | BA x -> Some (sp,BA (preg_to_dwarf x))
     | BA_int _
@@ -75,7 +75,7 @@ let translate_annot sp preg_to_dwarf annot =
     | BA_addrglobal _
     | BA_loadstack _ -> None
     | BA_addrstack ofs -> Some (sp,BA_addrstack ofs)
-    | BA_splitlong (hi,lo) -> 
+    | BA_splitlong (hi,lo) ->
         begin
           match (aux hi,aux lo) with
           | Some (_,hi) ,Some (_,lo) -> Some (sp,BA_splitlong (hi,lo))
@@ -84,11 +84,11 @@ let translate_annot sp preg_to_dwarf annot =
   (match annot with
   | [] -> None
   | a::_ -> aux a)
-    
+
 
 let expand_debug id sp preg simple l =
   let get_lbl = function
-    | None -> 
+    | None ->
         let lbl = new_label () in
         emit (Plabel lbl);
         lbl
@@ -99,12 +99,12 @@ let expand_debug id sp preg simple l =
         let kind = (P.to_int kind) in
         begin
           match kind with
-          | 1-> 
+          | 1->
               emit i;aux lbl scopes rest
           | 2 ->
               aux  lbl scopes rest
           | 3 ->
-             begin 
+             begin
                match translate_annot sp preg args with
                | Some a ->
                    let lbl = get_lbl lbl in
@@ -132,7 +132,7 @@ let expand_debug id sp preg simple l =
           | _ ->
               aux None scopes rest
         end
-    | (Plabel lbl)::rest -> simple (Plabel lbl); aux (Some lbl) scopes rest 
+    | (Plabel lbl)::rest -> simple (Plabel lbl); aux (Some lbl) scopes rest
     | i::rest -> simple i; aux None scopes rest in
   (* We need to move all closing debug annotations before the last real statement *)
   let rec move_debug acc bcc = function
diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll
index 7ed5b4ab..6695b6b7 100644
--- a/backend/CMlexer.mll
+++ b/backend/CMlexer.mll
@@ -21,8 +21,8 @@ exception Error of string
 }
 
 let blank = [' ' '\009' '\012' '\010' '\013']
-let floatlit = 
- ("-"? (['0'-'9'] ['0'-'9' '_']* 
+let floatlit =
+ ("-"? (['0'-'9'] ['0'-'9' '_']*
   ('.' ['0'-'9' '_']* )?
   (['e' 'E'] ['+' '-']? ['0'-'9'] ['0'-'9' '_']*)? )) | "inf" | "nan"
 let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '_' '$' '0'-'9']*
@@ -69,7 +69,7 @@ rule token = parse
   | "floatofintu"    { FLOATOFINTU }
   | "floatoflong"  { FLOATOFLONG }
   | "floatoflongu" { FLOATOFLONGU }
-  | "goto"  { GOTO } 
+  | "goto"  { GOTO }
   | ">"    { GREATER }
   | ">f"    { GREATERF }
   | ">l"    { GREATERL }
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index b48a486e..5b79cde8 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -13,7 +13,7 @@
 /*                                                                     */
 /* *********************************************************************/
 
-/* Note that this compiles a superset of the language defined by the AST, 
+/* Note that this compiles a superset of the language defined by the AST,
    including function calls in expressions, matches, while statements, etc. */
 
 %{
@@ -123,7 +123,7 @@ let mkeval e =
       let c1 = convert_rexpr e1 in
       let cl = convert_rexpr_list el in
       prepend_seq !convert_accu (Scall(None, sg, c1, cl))
-  | Rbuiltin(sg, pef, el) -> 
+  | Rbuiltin(sg, pef, el) ->
       let ef = mkef sg pef in
       let cl = convert_rexpr_list el in
       prepend_seq !convert_accu (Sbuiltin(None, ef, cl))
@@ -322,9 +322,9 @@ let mkmatch expr cases =
 %token LESSLESSL
 %token LONG
 %token <int64> LONGLIT
-%token LONGOFINT 
+%token LONGOFINT
 %token LONGOFINTU
-%token LONGOFFLOAT 
+%token LONGOFFLOAT
 %token LONGUOFFLOAT
 %token LOOP
 %token LPAREN
@@ -375,7 +375,7 @@ let mkmatch expr cases =
 %left CARET CARETL
 %left AMPERSAND AMPERSANDL
 %left EQUALEQUAL BANGEQUAL LESS LESSEQUAL GREATER GREATEREQUAL EQUALEQUALU BANGEQUALU LESSU LESSEQUALU GREATERU GREATEREQUALU EQUALEQUALF BANGEQUALF LESSF LESSEQUALF GREATERF GREATEREQUALF EQUALEQUALL BANGEQUALL LESSL LESSEQUALL GREATERL GREATEREQUALL EQUALEQUALLU BANGEQUALLU LESSLU LESSEQUALLU GREATERLU GREATEREQUALLU
-%left LESSLESS GREATERGREATER GREATERGREATERU LESSLESSL GREATERGREATERL GREATERGREATERLU 
+%left LESSLESS GREATERGREATER GREATERGREATERU LESSLESSL GREATERGREATERL GREATERGREATERLU
 %left PLUS PLUSF PLUSL MINUS MINUSF MINUSL
 %left STAR SLASH PERCENT STARF SLASHF SLASHU PERCENTU STARL SLASHL SLASHLU PERCENTL PERCENTLU
 %nonassoc BANG TILDE TILDEL p_uminus ABSF INTOFFLOAT INTUOFFLOAT FLOATOFINT FLOATOFINTU INT8S INT8U INT16S INT16U FLOAT32 INTOFLONG LONGOFINT LONGOFINTU LONGOFFLOAT LONGUOFFLOAT FLOATOFLONG FLOATOFLONGU
@@ -432,12 +432,12 @@ init_data_list:
     /* empty */                                 { [] }
    | init_data_list_1                           { $1 }
  ;
- 
+
 init_data_list_1:
      init_data                                   { [$1] }
    | init_data_list_1 COMMA init_data            { $3 :: $1 }
  ;
- 
+
 init_data:
      INT8 INTLIT                                 { Init_int8 (coqint_of_camlint $2) }
    | INT16 INTLIT                                { Init_int16 (coqint_of_camlint $2) }
@@ -453,7 +453,7 @@ init_data:
    | LBRACKET INTLIT RBRACKET                    { Init_space (Z.of_sint32 $2) }
    | INTLIT LPAREN STRINGLIT RPAREN              { Init_addrof (intern_string $3, coqint_of_camlint $1) }
  ;
- 
+
 /* Procedures */
 
 proc:
@@ -472,14 +472,14 @@ proc:
                         fn_vars = List.rev (tmp @ $9);
                         fn_stackspace = $8;
                         fn_body = $10 })) }
-  | EXTERN STRINGLIT COLON signature 
+  | EXTERN STRINGLIT COLON signature
       { (intern_string $2, Gfun(External(EF_external(intern_string $2,$4)))) }
   | EXTERN STRINGLIT EQUAL eftoks COLON signature
       { (intern_string $2, Gfun(External(mkef $6 $4))) }
 ;
 
 signature:
-    type_ 
+    type_
                { {sig_args = []; sig_res = Some $1; sig_cc = cc_default} }
   | VOID
                { {sig_args = []; sig_res = None; sig_cc = cc_default} }
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml
index aacbf86f..72bf9cb4 100644
--- a/backend/CMtypecheck.ml
+++ b/backend/CMtypecheck.ml
@@ -323,7 +323,7 @@ let rec type_stmt env blk ret s =
   | Sreturn (Some e) ->
       begin match ret with
       | None -> raise (Error "return with argument")
-      | Some tret -> 
+      | Some tret ->
           begin try
             unify (type_expr env [] e) (ty_of_typ tret)
           with Error s ->
diff --git a/backend/IRC.ml b/backend/IRC.ml
index dcd8624a..eb677069 100644
--- a/backend/IRC.ml
+++ b/backend/IRC.ml
@@ -163,7 +163,7 @@ module DLinkMove = struct
   type t = move
   let make state =
     let rec empty =
-      { src = DLinkNode.dummy; dst = DLinkNode.dummy; 
+      { src = DLinkNode.dummy; dst = DLinkNode.dummy;
         mstate = state; mprev = empty; mnext = empty }
     in empty
   let dummy = make CoalescedMoves
@@ -301,7 +301,7 @@ let init costs =
     worklistMoves = DLinkMove.make WorklistMoves;
     activeMoves = DLinkMove.make ActiveMoves
   }
-  
+
 (* Create nodes corresponding to XTL variables *)
 
 let weightedSpillCost st =
@@ -312,7 +312,7 @@ let weightedSpillCost st =
 let newNodeOfReg g r ty =
   let st = g.stats_of_reg r in
   g.nextIdent <- g.nextIdent + 1;
-  { ident = g.nextIdent; typ = ty; 
+  { ident = g.nextIdent; typ = ty;
     var = V(r, ty);
     regclass = if st.cost >= 0 then class_of_type ty else no_spill_class;
     accesses = st.usedefs;
@@ -328,7 +328,7 @@ let newNodeOfReg g r ty =
 let newNodeOfLoc g l =
   let ty = Loc.coq_type l in
   g.nextIdent <- g.nextIdent + 1;
-  { ident = g.nextIdent; typ = ty; 
+  { ident = g.nextIdent; typ = ty;
     var = L l; regclass = class_of_type ty;
     accesses = 0; spillcost = 0.0;
     adjlist = []; degree = 0; movelist = []; extra_adj = []; extra_pref = [];
@@ -608,9 +608,9 @@ let canCoalesceGeorge g u v =
 -  If [u] is precolored, use George's criterion.
 -  If [u] is not precolored, use Briggs's criterion.
 
-   As noted by Hailperin, for non-precolored nodes, George's criterion 
+   As noted by Hailperin, for non-precolored nodes, George's criterion
    is incomparable with Briggs's: there are cases where G says yes
-   and B says no.  Typically, [u] is a long-lived variable with many 
+   and B says no.  Typically, [u] is a long-lived variable with many
    interferences, and [v] is a short-lived temporary copy of [u]
    that has no more interferences than [u].  Coalescing [u] and [v]
    is "weakly safe" in Hailperin's terminology: [u] is no harder to color,
@@ -690,7 +690,7 @@ let coalesce g =
     combine g u v;
     addWorkList g u
   end else begin
-    DLinkMove.insert m g.activeMoves    
+    DLinkMove.insert m g.activeMoves
   end
 
 (* Freeze moves associated with node [u] *)
diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index ef268562..71ee2e56 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -26,7 +26,7 @@ let enumerate_aux f reach =
     (fun pc nodes ->
       if PMap.get pc reach
       then Coq_cons (pc, nodes)
-      else nodes) 
+      else nodes)
     f.fn_nextpc
 ***)
 
@@ -100,7 +100,7 @@ let basic_blocks f joins =
   (* end_block: record block that we just discovered *)
   and end_block blk minpc =
     blocks := (minpc, List.rev blk) :: !blocks
-  in 
+  in
     start_block f.fn_entrypoint; !blocks
 
 (* Flatten basic blocks in decreasing order of minpc *)
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index 594b43b7..e7c945e3 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -38,7 +38,7 @@ module Printer(Target:TARGET) =
 
     let print_location oc loc =
       if loc <> Cutil.no_loc then Target.print_file_line oc (fst loc) (snd loc)
-          
+
     let print_function oc name fn =
       Hashtbl.clear current_function_labels;
       Target.reset_constants ();
@@ -66,7 +66,7 @@ module Printer(Target:TARGET) =
       Target.print_jumptable oc jmptbl;
       if !Clflags.option_g then
         Hashtbl.iter (fun p i -> Debug.add_label name p i) current_function_labels
-    
+
     let print_init_data oc name id =
       if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0
           && List.for_all (function Init_int8 _ -> true | _ -> false) id
@@ -74,7 +74,7 @@ module Printer(Target:TARGET) =
         fprintf oc "	.ascii	\"%s\"\n" (PrintCsyntax.string_of_init id)
       else
         List.iter (Target.print_init oc) id
- 
+
     let print_var oc name v =
       match v.gvar_init with
       | [] -> ()
@@ -101,7 +101,7 @@ module Printer(Target:TARGET) =
             let sz =
               match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in
             Target.print_comm_symb oc sz name align
-                            
+
     let print_globdef oc (name,gdef) =
       match gdef with
       | Gfun (Internal code) -> print_function oc name code
@@ -116,7 +116,7 @@ module Printer(Target:TARGET) =
         let symbol = Target.symbol
       end
 
-    module DebugPrinter = DwarfPrinter (DwarfTarget)     
+    module DebugPrinter = DwarfPrinter (DwarfTarget)
   end
 
 let print_program oc p db =
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 78399c04..4a612c26 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -98,7 +98,7 @@ let elf_symbol_offset oc (symb, ofs) =
 let elf_print_fun_info oc name =
   fprintf oc "	.type	%a, @function\n" elf_symbol name;
   fprintf oc "	.size	%a, . - %a\n" elf_symbol name elf_symbol name
-   
+
 let elf_print_var_info oc name =
   fprintf oc "	.type	%a, @object\n" elf_symbol name;
   fprintf oc "	.size	%a, . - %a\n" elf_symbol name elf_symbol name
@@ -109,20 +109,20 @@ let cfi_startproc =
     (fun oc -> fprintf oc "	.cfi_startproc\n")
   else
     (fun _ -> ())
-      
+
 let cfi_endproc =
   if Configuration.asm_supports_cfi then
     (fun oc -> fprintf oc "	.cfi_endproc\n")
   else
     (fun _ -> ())
-      
-      
+
+
 let cfi_adjust =
   if Configuration.asm_supports_cfi then
        (fun oc delta -> fprintf oc "	.cfi_adjust_cfa_offset	%ld\n" delta)
   else
     (fun _ _ -> ())
-      
+
 let cfi_rel_offset =
   if Configuration.asm_supports_cfi then
     (fun oc reg ofs -> fprintf oc "	.cfi_rel_offset	%s, %ld\n" reg ofs)
@@ -211,7 +211,7 @@ let print_debug_info comment print_line print_preg sp_name oc kind txt args =
                  comment print_debug_args args;
   | _ ->
       ()
-					    
+
 (** Inline assembly *)
 
 let print_asm_argument print_preg oc modifier = function
@@ -256,7 +256,7 @@ let print_inline_asm print_preg oc txt sg args res =
 (** Print CompCert version and command-line as asm comment *)
 
 let print_version_and_options oc comment =
-  let version_string =  
+  let version_string =
     if Version.buildnr <> "" && Version.tag <> "" then
       sprintf "%s, Build: %s, Tag: %s" Version.version Version.buildnr Version.tag
     else
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index 19f4c839..9b6b1488 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -139,7 +139,7 @@ let rec expr p (prec, e) =
     if assoc = LtoR
     then (prec', prec' + 1)
     else (prec' + 1, prec') in
-  if prec' < prec 
+  if prec' < prec
   then fprintf p "@[<hov 2>("
   else fprintf p "@[<hov 2>";
   begin match e with
@@ -238,14 +238,14 @@ let rec print_stmt p s =
                 print_expr_list (true, el)
 	        print_sig (ef_sig ef)
   | Sbuiltin(Some id, ef, el) ->
-      fprintf p "@[<hv 2>%s =@ builtin %s@,(@[<hov 0>%a@]) : @[<hov 0>%a@];@]" 
+      fprintf p "@[<hv 2>%s =@ builtin %s@,(@[<hov 0>%a@]) : @[<hov 0>%a@];@]"
                 (ident_name id)
                 (name_of_external ef)
                 print_expr_list (true, el)
 	        print_sig (ef_sig ef)
   | Sseq(s1,s2) when just_skips s1 && just_skips s2 ->
       ()
-  | Sseq(s1, s2) when just_skips s1 -> 
+  | Sseq(s1, s2) when just_skips s1 ->
       print_stmt p s2
   | Sseq(s1, s2) when just_skips s2 ->
       print_stmt p s1
@@ -277,7 +277,7 @@ let rec print_stmt p s =
         (if long then "l" else "") print_expr e;
       List.iter
         (fun (n, x) ->
-           fprintf p "@ case %s%s: exit %d;" 
+           fprintf p "@ case %s%s: exit %d;"
                      (Z.to_string n)
                      (if long then "LL" else "")
                      (Nat.to_int x))
@@ -334,12 +334,12 @@ let print_init_data p = function
 let rec print_init_data_list p = function
   | [] -> ()
   | [item] -> print_init_data p item
-  | item::rest -> 
+  | item::rest ->
       (print_init_data p item;
        fprintf p ",";
        print_init_data_list p rest)
 
-let print_globvar p gv = 
+let print_globvar p gv =
   if (gv.gvar_readonly) then
     fprintf p "readonly ";
   if (gv.gvar_volatile) then
diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml
index 78ce1816..f2242c13 100644
--- a/backend/PrintRTL.ml
+++ b/backend/PrintRTL.ml
@@ -99,7 +99,7 @@ let print_function pp id f =
       (List.rev_map
         (fun (pc, i) -> (P.to_int pc, i))
         (PTree.elements f.fn_code)) in
-  print_succ pp f.fn_entrypoint 
+  print_succ pp f.fn_entrypoint
     (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1);
   List.iter (print_instruction pp) instrs;
   fprintf pp "}\n\n"
diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml
index bb67dc96..dd8434da 100644
--- a/backend/PrintXTL.ml
+++ b/backend/PrintXTL.ml
@@ -71,7 +71,7 @@ let liveset pp lv =
   fprintf pp "{";
   VSet.iter (function V(r, ty) -> fprintf pp " x%d" (P.to_int r)
                     | L l -> ())
-    lv;                  
+    lv;
   fprintf pp " }"
 
 let print_succ pp s dfl =
@@ -145,7 +145,7 @@ let print_function pp ?alloc ?live f =
       (List.map
         (fun (pc, i) -> (P.to_int pc, i))
         (PTree.elements f.fn_code)) in
-  print_succ pp f.fn_entrypoint 
+  print_succ pp f.fn_entrypoint
     (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1);
   List.iter (print_block pp) instrs;
   fprintf pp "}\n\n";
diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml
index e3373bf9..045299d4 100644
--- a/backend/RTLgenaux.ml
+++ b/backend/RTLgenaux.ml
@@ -72,7 +72,7 @@ let size_eos = function
 let rec size_stmt = function
   | Sskip -> 0
   | Sassign(id, a) -> size_expr a
-  | Sstore(chunk, addr, args, src) -> 1 + size_exprs args + size_expr src 
+  | Sstore(chunk, addr, args, src) -> 1 + size_exprs args + size_expr src
   | Scall(optid, sg, eos, args) ->
       3 + size_eos eos + size_exprs args + length_exprs args
   | Stailcall(sg, eos, args) ->
@@ -91,6 +91,6 @@ let rec size_stmt = function
   | Slabel(lbl, s) -> size_stmt s
   | Sgoto lbl -> 1
 
-let more_likely (c: condexpr) (ifso: stmt) (ifnot: stmt) = 
+let more_likely (c: condexpr) (ifso: stmt) (ifnot: stmt) =
   size_stmt ifso > size_stmt ifnot
 
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index 76288fb5..a5fa8cd7 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -234,7 +234,7 @@ let block_of_RTL_instr funsig tyenv = function
       and res' = vmregs (loc_result sg) in
       xparmove (expand_regs tyenv args) args'
        (Xcall(sg, sum_left_map (vreg tyenv) ros, args', res') ::
-         xparmove res' (expand_regs tyenv [res]) 
+         xparmove res' (expand_regs tyenv [res])
            [Xbranch s])
   | RTL.Itailcall(sg, ros, args) ->
       let args' = vlocs (loc_arguments sg) in
@@ -273,7 +273,7 @@ let function_of_RTL_function f tyenv =
   let xc = PTree.map1 (block_of_RTL_instr f.RTL.fn_sig tyenv) f.RTL.fn_code in
   (* Add moves for function parameters *)
   let pc_entrypoint = next_pc f in
-  let b_entrypoint = 
+  let b_entrypoint =
      xparmove (vlocs (loc_parameters f.RTL.fn_sig))
               (expand_regs tyenv f.RTL.fn_params)
               [Xbranch f.RTL.fn_entrypoint] in
@@ -465,7 +465,7 @@ let spill_costs f =
           let c1 = st.cost + amount in
           let c2 = if c1 >= 0 then c1 else max_int (* overflow *) in
           st.cost <- c2
-        end;           
+        end;
         st.usedefs <- st.usedefs + uses in
 
   let charge_list amount uses vl =
@@ -624,7 +624,7 @@ let add_interfs_instr g instr live =
       add_interfs_destroyed g (VSet.remove res live) (destroyed_by_op op)
   | Xload(chunk, addr, args, dst) ->
       add_interfs_def g dst live;
-      add_interfs_destroyed g (VSet.remove dst live) 
+      add_interfs_destroyed g (VSet.remove dst live)
                               (destroyed_by_load chunk addr)
   | Xstore(chunk, addr, args, src) ->
       add_interfs_destroyed g live (destroyed_by_store chunk addr)
@@ -655,7 +655,7 @@ let add_interfs_instr g instr live =
             | Some mr ->
                 add_interfs_list_mreg g vargs mr;
                 add_interfs_list_mreg g vres mr)
-            clob          
+            clob
       | _ -> ()
       end
   | Xbranch s ->
@@ -776,7 +776,7 @@ let add v t eqs = (v, t, 0) :: eqs
 
 let kill x eqs =
   List.filter (fun (v, t, date) -> v <> x && t <> x) eqs
-  
+
 let reload_var tospill eqs v =
   if not (VSet.mem v tospill) then
     (v, [], eqs)
@@ -845,7 +845,7 @@ let rec trim count eqs =
   if count <= 0 then [] else
     match eqs with
     | [] -> []
-    | (v, t, date) :: eqs' -> 
+    | (v, t, date) :: eqs' ->
         if date <= !max_age
         then (v, t, date + 1) :: trim (count - 1) eqs'
         else []
@@ -882,7 +882,7 @@ let spill_instr tospill eqs instr =
           | true, false ->
               let tmp = new_temp (typeof res) in
               let (argl', c1, eqs1) = reload_vars tospill eqs argl in
-              (c1 @ [Xmove(arg1, tmp); Xop(op, tmp :: argl', tmp); Xspill(tmp, res)], 
+              (c1 @ [Xmove(arg1, tmp); Xop(op, tmp :: argl', tmp); Xspill(tmp, res)],
                add res tmp (kill res eqs1))
           | false, true ->
               let eqs1 = add arg1 res (kill res eqs) in
@@ -890,13 +890,13 @@ let spill_instr tospill eqs instr =
               (Xreload(arg1, res) :: c1 @ [Xop(op, res :: argl', res)],
                kill res eqs2)
           | true, true ->
-              let tmp = new_temp (typeof res) in              
+              let tmp = new_temp (typeof res) in
               let eqs1 = add arg1 tmp eqs in
               let (argl', c1, eqs2) = reload_vars tospill eqs1 argl in
               (Xreload(arg1, tmp) :: c1 @ [Xop(op, tmp :: argl', tmp); Xspill(tmp, res)],
                add res tmp (kill tmp (kill res eqs2)))
           end
-      end          
+      end
   | Xload(chunk, addr, args, dst) ->
       let (args', c1, eqs1) = reload_vars tospill eqs args in
       let (dst', c2, eqs2) = save_var tospill eqs1 dst in
@@ -1047,7 +1047,7 @@ let transl_instr alloc instr k =
           if rarg1 = rres then
             LTL.Lop(op, rargs, rres) :: k
           else
-            LTL.Lop(Omove, [rarg1], rres) :: 
+            LTL.Lop(Omove, [rarg1], rres) ::
             LTL.Lop(op, rres :: rargl, rres) :: k
       end
   | Xload(chunk, addr, args, dst) ->
@@ -1079,7 +1079,7 @@ let transl_function fn alloc =
   { LTL.fn_sig = fn.fn_sig;
     LTL.fn_stacksize = fn.fn_stacksize;
     LTL.fn_entrypoint = fn.fn_entrypoint;
-    LTL.fn_code = PTree.map1 (transl_block alloc) fn.fn_code 
+    LTL.fn_code = PTree.map1 (transl_block alloc) fn.fn_code
   }
 
 
@@ -1113,7 +1113,7 @@ and more_rounds f ts count =
       fprintf !pp "--- Remain to be spilled:\n";
       VSet.iter (fun v -> fprintf !pp "%a " PrintXTL.var v) ts';
       fprintf !pp "\n\n"
-    end;      
+    end;
     more_rounds f (VSet.union ts ts') (count + 1)
   end
 
@@ -1148,7 +1148,7 @@ let regalloc f =
       | Timeout ->
           Error(msg (coqstring_of_camlstring "Spilling fails to converge"))
       | Type_error_at pc ->
-          Error [MSG(coqstring_of_camlstring "Ill-typed XTL code at PC "); 
+          Error [MSG(coqstring_of_camlstring "Ill-typed XTL code at PC ");
                  POS pc]
       | Bad_LTL ->
           Error(msg (coqstring_of_camlstring "Bad LTL after spilling"))
diff --git a/backend/Splitting.ml b/backend/Splitting.ml
index 97b26a50..17b8098d 100644
--- a/backend/Splitting.ml
+++ b/backend/Splitting.ml
@@ -39,9 +39,9 @@ let rec repr lr =
   | Link lr' -> let lr'' = repr lr' in lr.kind <- Link lr''; lr''
   | _ -> lr
 
-let same_range lr1 lr2 = 
-  lr1 == lr2 || (* quick test for speed *) 
-  repr lr1 == repr lr2 (* the real test *) 
+let same_range lr1 lr2 =
+  lr1 == lr2 || (* quick test for speed *)
+  repr lr1 == repr lr2 (* the real test *)
 
 let unify lr1 lr2 =
   let lr1 = repr lr1 and lr2 = repr lr2 in
diff --git a/backend/XTL.ml b/backend/XTL.ml
index dde9bdb0..2ddbc50a 100644
--- a/backend/XTL.ml
+++ b/backend/XTL.ml
@@ -186,7 +186,7 @@ let type_block blk =
 let type_function f =
   PTree.fold
     (fun () pc blk ->
-       try 
+       try
          type_block blk
        with Type_error ->
          raise (Type_error_at pc))
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 6826804f..61528185 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -141,8 +141,8 @@ let builtins_generic = {
     (* Block copy *)
     "__builtin_memcpy_aligned",
          (TVoid [],
-           [TPtr(TVoid [], []); 
-            TPtr(TVoid [AConst], []); 
+           [TPtr(TVoid [], []);
+            TPtr(TVoid [AConst], []);
             TInt(IUInt, []);
             TInt(IUInt, [])],
           false);
@@ -357,12 +357,12 @@ let make_builtin_memcpy args =
       let sz1 =
         match Initializers.constval !comp_env sz with
         | Errors.OK(Vint n) -> n
-        | _ -> error "ill-formed __builtin_memcpy_aligned (3rd argument must be 
+        | _ -> error "ill-formed __builtin_memcpy_aligned (3rd argument must be
 a constant)"; Integers.Int.zero in
       let al1 =
         match Initializers.constval !comp_env al with
         | Errors.OK(Vint n) -> n
-        | _ -> error "ill-formed __builtin_memcpy_aligned (4th argument must be 
+        | _ -> error "ill-formed __builtin_memcpy_aligned (4th argument must be
 a constant)"; Integers.Int.one in
       (* to check: sz1 > 0, al1 divides sz1, al1 = 1|2|4|8 *)
       (* Issue #28: must decay array types to pointer types *)
@@ -384,7 +384,7 @@ let va_list_ptr e =
 let make_builtin_va_arg_by_val helper ty ty_ret arg =
   let ty_fun =
     Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), ty_ret, cc_default) in
-  Ecast 
+  Ecast
     (Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun),
            Econs(va_list_ptr arg, Enil),
            ty_ret),
@@ -392,13 +392,13 @@ let make_builtin_va_arg_by_val helper ty ty_ret arg =
 
 let make_builtin_va_arg_by_ref helper ty arg =
   let ty_fun =
-    Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), 
+    Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil),
               Tpointer(Tvoid, noattr), cc_default) in
   let ty_ptr =
     Tpointer(ty, noattr) in
   let call =
     Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun),
-          Econs(va_list_ptr arg, 
+          Econs(va_list_ptr arg,
                 Econs(Esizeof(ty, Tint(I32, Unsigned, noattr)), Enil)),
           Tpointer(Tvoid, noattr)) in
   Evalof(Ederef(Ecast(call, ty_ptr), ty), ty)
@@ -406,13 +406,13 @@ let make_builtin_va_arg_by_ref helper ty arg =
 let make_builtin_va_arg env ty e =
   match ty with
   | Tint _ | Tpointer _ ->
-      make_builtin_va_arg_by_val 
+      make_builtin_va_arg_by_val
         "__compcert_va_int32" ty (Tint(I32, Unsigned, noattr)) e
   | Tlong _ ->
-      make_builtin_va_arg_by_val 
+      make_builtin_va_arg_by_val
         "__compcert_va_int64" ty (Tlong(Unsigned, noattr)) e
   | Tfloat _ ->
-      make_builtin_va_arg_by_val 
+      make_builtin_va_arg_by_val
         "__compcert_va_float64" ty (Tfloat(F64, noattr)) e
   | Tstruct _ | Tunion _ ->
       make_builtin_va_arg_by_ref
@@ -433,7 +433,7 @@ let rec log2 n = if n = 1 then 0 else 1 + log2 (n lsr 1)
 
 let convertAttr a =
   { attr_volatile = List.mem AVolatile a;
-    attr_alignas = 
+    attr_alignas =
       let n = Cutil.alignas_attribute a in
       if n > 0 then Some (N.of_int (log2 n)) else None }
 
@@ -463,7 +463,7 @@ let convertFkind = function
   | C.FFloat -> F32
   | C.FDouble -> F64
   | C.FLongDouble ->
-      if not !Clflags.option_flongdouble then unsupported "'long double' type"; 
+      if not !Clflags.option_flongdouble then unsupported "'long double' type";
       F64
 
 let rec convertTyp env t =
@@ -524,11 +524,11 @@ let convertField env f =
   (intern_string f.fld_name, convertTyp env f.fld_typ)
 
 let convertCompositedef env su id attr members =
-  let t = match su with 
-  | C.Struct -> 
+  let t = match su with
+  | C.Struct ->
       let layout = Cutil.struct_layout env members in
       List.iter (fun (a,b) -> Debug.set_member_offset id a b) layout;
-      TStruct (id,attr) 
+      TStruct (id,attr)
   | C.Union -> TUnion (id,attr) in
   Debug.set_composite_size id su (Cutil.sizeof env t);
   Composite(intern_string id.name,
@@ -763,7 +763,7 @@ let rec convertExpr env e =
         EF_debug(P.of_int64 kind, intern_string text,
                  typlist_of_typelist targs2),
         targs2, convertExprList env args2, convertTyp env e.etyp)
- 
+
   | C.ECall({edesc = C.EVar {name = "__builtin_annot"}}, args) ->
       begin match args with
       | {edesc = C.EConst(CStr txt)} :: args1 ->
@@ -774,20 +774,20 @@ let rec convertExpr env e =
       | _ ->
           error "ill-formed __builtin_annot (first argument must be string literal)";
           ezero
-      end          
- 
+      end
+
   | C.ECall({edesc = C.EVar {name = "__builtin_annot_intval"}}, args) ->
       begin match args with
       | [ {edesc = C.EConst(CStr txt)}; arg ] ->
           let targ = convertTyp env
                          (Cutil.default_argument_conversion env arg.etyp) in
           Ebuiltin(EF_annot_val(intern_string txt, typ_of_type targ),
-                   Tcons(targ, Tnil), convertExprList env [arg], 
+                   Tcons(targ, Tnil), convertExprList env [arg],
                    convertTyp env e.etyp)
       | _ ->
           error "ill-formed __builtin_annot_intval (first argument must be string literal)";
           ezero
-      end          
+      end
 
  | C.ECall({edesc = C.EVar {name = "__builtin_memcpy_aligned"}}, args) ->
       make_builtin_memcpy (convertExprList env args)
@@ -822,9 +822,9 @@ let rec convertExpr env e =
       let sg =
         signature_of_type targs tres
            {cc_vararg = true; cc_unproto = false; cc_structret = false} in
-      Ebuiltin(EF_external(intern_string "printf", sg), 
+      Ebuiltin(EF_external(intern_string "printf", sg),
                targs, convertExprList env args, tres)
- 
+
   | C.ECall(fn, args) ->
       if not (supported_return_type env e.etyp) then
         unsupported ("function returning a result of type " ^ string_of_type e.etyp ^ " (consider adding option -fstruct-return)");
@@ -867,17 +867,17 @@ and convertExprList env el =
 (* Extended assembly *)
 
 let convertAsm loc env txt outputs inputs clobber =
-  let (txt', output', inputs') = 
+  let (txt', output', inputs') =
     ExtendedAsm.transf_asm loc env txt outputs inputs clobber in
   let clobber' =
     List.map (fun s -> coqstring_of_camlstring (String.uppercase s)) clobber in
   let ty_res =
     match output' with None -> TVoid [] | Some e -> e.etyp in
   (* Build the Ebuiltin expression *)
-  let e = 
+  let e =
     let tinputs = convertTypArgs env [] inputs' in
     let toutput = convertTyp env ty_res in
-    Ebuiltin(EF_inline_asm(intern_string txt', 
+    Ebuiltin(EF_inline_asm(intern_string txt',
                            signature_of_type tinputs toutput cc_default,
                            clobber'),
              tinputs,
@@ -894,7 +894,7 @@ type switchlabel =
   | Case of C.exp
   | Default
 
-type switchbody = 
+type switchbody =
   | Label of switchlabel
   | Stmt of C.stmt
 
@@ -922,16 +922,16 @@ let rec groupSwitch = function
       (Cutil.sseq s.sloc s fst, cases)
 
 (* Test whether the statement contains case and give an *)
-let rec contains_case s = 
+let rec contains_case s =
   match s.sdesc with
-  | C.Sskip 
-  | C.Sdo _ 
+  | C.Sskip
+  | C.Sdo _
   | C.Sbreak
-  | C.Scontinue 
+  | C.Scontinue
   | C.Sswitch _ (* Stop at a switch *)
-  | C.Sgoto _ 
-  | C.Sreturn _ 
-  | C.Sdecl _ 
+  | C.Sgoto _
+  | C.Sreturn _
+  | C.Sdecl _
   | C.Sasm _ ->  ()
   | C.Sseq (s1,s2)
   | C.Sif(_,s1,s2) -> contains_case s1; contains_case s2
@@ -1021,7 +1021,7 @@ and convertSwitch env is_64 = function
         match lbl with
         | Default ->
             None
-        | Case e ->    
+        | Case e ->
             match Ceval.integer_expr env e with
             | None -> unsupported "'case' label is not a compile-time integer";
                       None
@@ -1127,7 +1127,7 @@ let convertInitializer env ty i =
 let convertGlobvar loc env (sto, id, ty, optinit) =
   let id' = intern_string id.name in
   Debug.atom_global id id';
-  let ty' = convertTyp env ty in 
+  let ty' = convertTyp env ty in
   let sz = Ctypes.sizeof !comp_env ty' in
   let al = Ctypes.alignof !comp_env ty' in
   let attr = Cutil.attributes_of_type env ty in
@@ -1189,7 +1189,7 @@ let rec convertGlobdecls env res gl =
             warning ("'#pragma " ^ s ^ "' directive ignored");
           convertGlobdecls env res gl'
 
-(** Convert struct and union declarations.  
+(** Convert struct and union declarations.
     Result is a list of CompCert C composite declarations. *)
 
 let rec convertCompositedefs env res gl =
@@ -1228,7 +1228,7 @@ let rec translEnv env = function
 module IdentSet = Set.Make(struct type t = C.ident let compare = compare end)
 
 let cleanupGlobals p =
-  
+
   (* First pass: determine what is defined *)
   let strong = ref IdentSet.empty (* def functions or variables with inits *)
   and weak = ref IdentSet.empty (* variables without inits *)
@@ -1251,7 +1251,7 @@ let cleanupGlobals p =
     | _ -> () in
   List.iter classify_def p;
 
-  (* Second pass: keep "best" definition for each identifier *)  
+  (* Second pass: keep "best" definition for each identifier *)
   let rec clean defs accu = function
     | [] -> accu
     | g :: gl ->
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index f1c3ef18..ed19e178 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -67,7 +67,7 @@ let rec expr p (prec, e) =
     if assoc = LtoR
     then (prec', prec' + 1)
     else (prec' + 1, prec') in
-  if prec' < prec 
+  if prec' < prec
   then fprintf p "@[<hov 2>("
   else fprintf p "@[<hov 2>";
   begin match e with
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index d890c820..d7f098c2 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -80,7 +80,7 @@ let attributes a =
       sprintf " _Alignas(%Ld)%s" (Int64.shift_left 1L (N.to_int l)) s1
 
 let attributes_space a =
-  let s = attributes a in 
+  let s = attributes a in
   if String.length s = 0 then s else s ^ " "
 
 let name_optid id =
@@ -202,7 +202,7 @@ let rec expr p (prec, e) =
     if assoc = LtoR
     then (prec', prec' + 1)
     else (prec' + 1, prec') in
-  if prec' < prec 
+  if prec' < prec
   then fprintf p "@[<hov 2>("
   else fprintf p "@[<hov 2>";
   begin match e with
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index aea8ff0f..d1825def 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -57,17 +57,17 @@ let rec print_builtin_arg px oc = function
   | BA_long n -> fprintf oc "long %Ld" (camlint64_of_coqint n)
   | BA_float n -> fprintf oc "float %F" (camlfloat_of_coqfloat n)
   | BA_single n -> fprintf oc "single %F" (camlfloat_of_coqfloat32 n)
-  | BA_loadstack(chunk, ofs) -> 
+  | BA_loadstack(chunk, ofs) ->
       fprintf oc "%s[sp + %ld]" (name_of_chunk chunk) (camlint_of_coqint ofs)
   | BA_addrstack(ofs) ->
       fprintf oc "sp + %ld" (camlint_of_coqint ofs)
-  | BA_loadglobal(chunk, id, ofs) -> 
+  | BA_loadglobal(chunk, id, ofs) ->
       fprintf oc "%s[&%s + %ld]"
               (name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs)
   | BA_addrglobal(id, ofs) ->
       fprintf oc "&%s + %ld" (extern_atom id) (camlint_of_coqint ofs)
   | BA_splitlong(hi, lo) ->
-      fprintf oc "splitlong(%a, %a)" 
+      fprintf oc "splitlong(%a, %a)"
                  (print_builtin_arg px) hi (print_builtin_arg px) lo
 
 let rec print_builtin_args px oc = function
@@ -80,6 +80,6 @@ let rec print_builtin_res px oc = function
   | BR x -> px oc x
   | BR_none -> fprintf oc "_"
   | BR_splitlong(hi, lo) ->
-      fprintf oc "splitlong(%a, %a)" 
+      fprintf oc "splitlong(%a, %a)"
                  (print_builtin_res px) hi (print_builtin_res px) lo
 
diff --git a/common/Sections.ml b/common/Sections.ml
index 0910f2dc..93783155 100644
--- a/common/Sections.ml
+++ b/common/Sections.ml
@@ -58,7 +58,7 @@ let default_section_info = {
 
 let builtin_sections = [
   "CODE",
-     {sec_name_init = Section_text; 
+     {sec_name_init = Section_text;
       sec_name_uninit = Section_text;
       sec_writable = false; sec_executable = true;
       sec_access = Access_default};
@@ -119,7 +119,7 @@ let initialize () =
 (* Define or update a given section. *)
 
 let define_section name ?iname ?uname ?writable ?executable ?access () =
-  let si = 
+  let si =
     try Hashtbl.find current_section_table name
     with Not_found -> default_section_info in
   let writable =
@@ -218,7 +218,7 @@ let for_function env id ty_res =
     with Not_found ->
       assert false in
   [si_code.sec_name_init; si_literal.sec_name_init; si_jumptbl.sec_name_init]
- 
+
 (* Determine section for a string literal *)
 
 let for_stringlit() =
diff --git a/common/Switchaux.ml b/common/Switchaux.ml
index 39b484c7..0d4901bf 100644
--- a/common/Switchaux.ml
+++ b/common/Switchaux.ml
@@ -50,7 +50,7 @@ let compile_switch_as_tree modulus default tbl =
        let (key1, act1) = sw.(lo)
        and (key2, act2) = sw.(lo+1)
        and (key3, act3) = sw.(lo+2) in
-       CTifeq(key1, act1, 
+       CTifeq(key1, act1,
         CTifeq(key2, act2,
           if Z.sub maxval minval = Z.of_uint 2
           then CTaction act3
diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
index d064f4b1..223ee3ca 100644
--- a/cparser/Bitfields.ml
+++ b/cparser/Bitfields.ml
@@ -191,12 +191,12 @@ let transf_composite env su id attr ml =
 (* Bitfield manipulation expressions *)
 
 let left_shift_count bf =
-  intconst 
+  intconst
     (Int64.of_int (8 * !config.sizeof_int - (bf.bf_pos + bf.bf_size)))
     IInt
 
 let right_shift_count bf =
-  intconst 
+  intconst
     (Int64.of_int (8 * !config.sizeof_int - bf.bf_size))
     IInt
 
@@ -303,7 +303,7 @@ let bitfield_initializer bf i =
 (* Associate to the left so that it prints more nicely *)
 
 let or_expr_list = function
-  | [] -> intconst 0L IUInt 
+  | [] -> intconst 0L IUInt
   | [e] -> e
   | e1 :: el ->
       List.fold_left
@@ -409,7 +409,7 @@ let rec transf_exp env ctx e =
       | Some(ex, bf) ->
           transf_post env ctx (op_for_incr_decr op) ex bf e1.etyp
       end
-  | EUnop(op, e1) -> 
+  | EUnop(op, e1) ->
       {edesc = EUnop(op, transf_exp env Val e1); etyp = e.etyp}
 
   | EBinop(Oassign, e1, e2, ty) ->
@@ -433,7 +433,7 @@ let rec transf_exp env ctx e =
           transf_assignop env ctx (op_for_assignop op) ex bf e2 ty
       end
   | EBinop(Ocomma, e1, e2, ty) ->
-      {edesc = EBinop(Ocomma, transf_exp env Effects e1, 
+      {edesc = EBinop(Ocomma, transf_exp env Effects e1,
                               transf_exp env Val e2, ty);
        etyp = e.etyp}
   | EBinop(op, e1, e2, ty) ->
@@ -534,5 +534,5 @@ let program p =
   Transform.program
     ~composite:transf_composite
     ~decl: transf_decl
-    ~fundef:transf_fundef 
+    ~fundef:transf_fundef
     p
diff --git a/cparser/C.mli b/cparser/C.mli
index 72e1f787..8d8f2805 100644
--- a/cparser/C.mli
+++ b/cparser/C.mli
@@ -27,7 +27,7 @@ type ident =
 
 (* Kinds of integers *)
 
-type ikind = 
+type ikind =
   | IBool       (** [_Bool] *)
   | IChar       (** [char] *)
   | ISChar      (** [signed char] *)
@@ -39,12 +39,12 @@ type ikind =
   | ILong       (** [long] *)
   | IULong      (** [unsigned long] *)
   | ILongLong   (** [long long] (or [_int64] on Microsoft Visual C) *)
-  | IULongLong  (** [unsigned long long] (or [unsigned _int64] on Microsoft 
+  | IULongLong  (** [unsigned long long] (or [unsigned _int64] on Microsoft
                     Visual C) *)
 
 (** Kinds of floating-point numbers*)
 
-type fkind = 
+type fkind =
     FFloat      (** [float] *)
   | FDouble     (** [double] *)
   | FLongDouble (** [long double] *)
@@ -73,7 +73,7 @@ type attr_arg =
   | AInt of int64
   | AString of string
 
-type attribute = 
+type attribute =
   | AConst
   | AVolatile
   | ARestrict
@@ -216,7 +216,7 @@ and stmt_desc =
   | Sdecl of decl
   | Sasm of attributes * string * asm_operand list * asm_operand list * string list
 
-and slabel = 
+and slabel =
   | Slabel of string
   | Scase of exp
   | Sdefault
diff --git a/cparser/Cabshelper.ml b/cparser/Cabshelper.ml
index 5e6a19d0..890679b4 100644
--- a/cparser/Cabshelper.ml
+++ b/cparser/Cabshelper.ml
@@ -16,8 +16,8 @@
 
 open Cabs
 
-let cabslu = {lineno = -10; 
-	      filename = "cabs loc unknown"; 
+let cabslu = {lineno = -10;
+	      filename = "cabs loc unknown";
 	      byteno = -10;
               ident = 0}
 
diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml
index ba7cdabc..74b535d4 100644
--- a/cparser/Ceval.ml
+++ b/cparser/Ceval.ml
@@ -124,7 +124,7 @@ let comparison env direction ptraction tyop ty1 v1 ty2 v2 =
   (* tyop = type at which the comparison is done *)
   let b =
     match cast env tyop ty1 v1, cast env tyop ty2 v2 with
-    | I n1, I n2 -> 
+    | I n1, I n2 ->
         if is_signed env tyop
         then direction (compare n1 n2) 0
         else direction (int64_unsigned_compare n1 n2) 0 (* including pointers *)
@@ -162,7 +162,7 @@ let binop env op tyop tyres ty1 v1 ty2 v2 =
         end
     | Odiv ->
         begin match cast env tyop ty1 v1, cast env tyop ty2 v2 with
-          | I n1, I n2 -> 
+          | I n1, I n2 ->
               if n2 = 0L then raise Notconst else
               if is_signed env tyop then I (Int64.div n1 n2)
               else I (int64_unsigned_div n1 n2)
@@ -170,7 +170,7 @@ let binop env op tyop tyres ty1 v1 ty2 v2 =
         end
     | Omod ->
         begin match v1, v2 with
-          | I n1, I n2 -> 
+          | I n1, I n2 ->
               if n2 = 0L then raise Notconst else
               if is_signed env tyop then I (Int64.rem n1 n2)
               else I (int64_unsigned_mod n1 n2)
@@ -220,11 +220,11 @@ let binop env op tyop tyres ty1 v1 ty2 v2 =
     | Ocomma ->
         v2
     | Ologand ->
-        if boolean_value v1 
+        if boolean_value v1
         then if boolean_value v2 then I 1L else I 0L
         else I 0L
     | Ologor ->
-        if boolean_value v1 
+        if boolean_value v1
         then I 1L
         else if boolean_value v2 then I 1L else I 0L
     | _ -> raise Notconst
diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml
index c81fd498..c8a900d5 100644
--- a/cparser/Cleanup.ml
+++ b/cparser/Cleanup.ml
@@ -92,7 +92,7 @@ let rec add_stmt s =
   | Sbreak -> ()
   | Scontinue -> ()
   | Sswitch(e, s1) -> add_exp e; add_stmt s1
-  | Slabeled(lbl, s) -> 
+  | Slabeled(lbl, s) ->
       begin match lbl with Scase e -> add_exp e | _ -> () end;
       add_stmt s
   | Sgoto lbl -> ()
@@ -187,7 +187,7 @@ let saturate p =
 let remove_unused_debug =  function
   | Gdecl (_,id,_,_) ->  Debug.remove_unused id
   | Gfundef f -> Debug.remove_unused f.fd_name
-  | _ -> ()    
+  | _ -> ()
 
 let rec simpl_globdecls accu = function
   | [] -> accu
@@ -212,6 +212,6 @@ let program p =
   let p' = simpl_globdecls [] p in
   referenced := IdentSet.empty;
   p'
-  
+
 
 
diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
index 1af5af1e..e80a4c8e 100644
--- a/cparser/Cprint.ml
+++ b/cparser/Cprint.ml
@@ -81,7 +81,7 @@ let const pp = function
           if c >= 32L && c <= 126L && c <> 34L && c <>92L
           then fprintf pp "%c" (Char.chr (Int64.to_int c))
           else fprintf pp "\" \"\\x%02Lx\" \"" c)
-        l;      
+        l;
       fprintf pp "\""
   | CEnum(id, v) ->
       ident pp id
@@ -216,7 +216,7 @@ let rec exp pp (prec, a) =
     if assoc = LtoR
     then (prec', prec' + 1)
     else (prec' + 1, prec') in
-  if prec' < prec 
+  if prec' < prec
   then fprintf pp "@[<hov 2>("
   else fprintf pp "@[<hov 2>";
   begin match a.edesc with
@@ -329,7 +329,7 @@ let rec exp pp (prec, a) =
       begin match al with
       | [] -> ()
       | a1 :: al ->
-          fprintf pp "%a" exp (2, a1); 
+          fprintf pp "%a" exp (2, a1);
           List.iter (fun a -> fprintf pp ",@ %a" exp (2, a)) al
       end;
       fprintf pp ")@]"
@@ -394,7 +394,7 @@ exception Not_expr
 let rec exp_of_stmt s =
   match s.sdesc with
   | Sdo e -> e
-  | Sseq(s1, s2) -> 
+  | Sseq(s1, s2) ->
       {edesc = EBinop(Ocomma, exp_of_stmt s1, exp_of_stmt s2, TVoid []);
        etyp = TVoid []}
   | Sif(e, s1, s2) ->
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 60bcc1a7..a86c779f 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -44,7 +44,7 @@ let rec add_attributes (al1: attributes) (al2: attributes) =
       else if a1 > a2 then a2 :: add_attributes al1 al2'
       else a1 :: add_attributes al1' al2'
 
-let rec remove_attributes (al1: attributes) (al2: attributes) = 
+let rec remove_attributes (al1: attributes) (al2: attributes) =
   (* viewed as sets: al1 \ al2 *)
   match al1, al2 with
   | [], _ -> []
@@ -91,7 +91,7 @@ let attr_is_type_related = function
   | Attr(("packed" | "__packed__"), _) -> true
   | _ -> false
 
-(* Is an attribute applicable to a whole array (true) or only to 
+(* Is an attribute applicable to a whole array (true) or only to
    array elements (false)? *)
 
 let attr_array_applicable = function
@@ -114,10 +114,10 @@ let rec add_attributes_type attr t =
   | TInt(ik, a) -> TInt(ik, add_attributes attr a)
   | TFloat(fk, a) -> TFloat(fk, add_attributes attr a)
   | TPtr(ty, a) -> TPtr(ty, add_attributes attr a)
-  | TArray(ty, sz, a) -> 
+  | TArray(ty, sz, a) ->
       let (attr_arr, attr_elt) = List.partition attr_array_applicable attr in
       TArray(add_attributes_type attr_elt ty, sz, add_attributes attr_arr a)
-  | TFun(ty, params, vararg, a) -> TFun(ty, params, vararg, add_attributes attr 
+  | TFun(ty, params, vararg, a) -> TFun(ty, params, vararg, add_attributes attr
 a)
   | TNamed(s, a) -> TNamed(s, add_attributes attr a)
   | TStruct(s, a) -> TStruct(s, add_attributes attr a)
@@ -144,7 +144,7 @@ let rec attributes_of_type env t =
   | TArray(ty, sz, a) -> add_attributes a (attributes_of_type env ty)
   | TFun(ty, params, vararg, a) -> a
   | TNamed(s, a) -> attributes_of_type env (unroll env t)
-  | TStruct(s, a) -> 
+  | TStruct(s, a) ->
       let ci = Env.find_struct env s in add_attributes ci.ci_attr a
   | TUnion(s, a) ->
       let ci = Env.find_union env s in add_attributes ci.ci_attr a
@@ -179,7 +179,7 @@ let erase_attributes_type env t =
 
 (* Remove all attributes from type that are not contained in attr *)
 let strip_attributes_type t attr =
-  let strip =  List.filter (fun a -> List.mem a attr) in 
+  let strip =  List.filter (fun a -> List.mem a attr) in
   match t with
   | TVoid at -> TVoid (strip at)
   | TInt (k,at) ->  TInt (k,strip at)
@@ -193,7 +193,7 @@ let strip_attributes_type t attr =
   | TEnum (n,at) -> TEnum(n,strip at)
 
 (* Remove the last attribute from the toplevel and return the changed type *)
-let strip_last_attribute typ  = 
+let strip_last_attribute typ  =
   let rec hd_opt l = match l with
     [] -> None,[]
   | a::rest -> Some a,rest in
@@ -306,9 +306,9 @@ let combine_types mode env t1 t2 =
     | _, TNamed _ -> comp m t1 (unroll env t2)
     | TStruct(s1, a1), TStruct(s2, a2) ->
         TStruct(comp_base s1 s2, comp_attr m a1 a2)
-    | TUnion(s1, a1), TUnion(s2, a2) -> 
+    | TUnion(s1, a1), TUnion(s2, a2) ->
         TUnion(comp_base s1 s2, comp_attr m a1 a2)
-    | TEnum(s1, a1), TEnum(s2, a2) -> 
+    | TEnum(s1, a1), TEnum(s2, a2) ->
         TEnum(comp_base s1 s2, comp_attr m a1 a2)
     | _, _ ->
         raise Incompat
@@ -376,7 +376,7 @@ let pack_bitfields ml =
   in
   let (nbits, ml') = pack 0 ml in
   let (sz, al) =
-    (* A lone bitfield of width 0 consumes no space and aligns to 1 *) 
+    (* A lone bitfield of width 0 consumes no space and aligns to 1 *)
     if nbits = 0 then (0, 1) else
     if nbits <= 8 then (1, 1) else
     if nbits <= 16 then (2, 2) else
@@ -487,7 +487,7 @@ let rec sizeof env t =
   | TEnum(_, _) -> Some(sizeof_ikind enum_ikind)
 
 (* Compute the size of a union.
-   It is the size is the max of the sizes of fields.    
+   It is the size is the max of the sizes of fields.
    Not done here but in composite_info_decl: rounding size to alignment. *)
 
 let sizeof_union env members =
@@ -539,7 +539,7 @@ let struct_layout env members =
       end
     | m :: rem ->
         match alignof env m.fld_typ, sizeof env m.fld_typ with
-        | Some a, Some s -> 
+        | Some a, Some s ->
             let offset = align ofs a in
             struct_layout_rec ((m.fld_name,offset)::mem) (offset + s) rem
         | _, _ -> []
@@ -580,11 +580,11 @@ let composite_info_def env su attr m =
 
 let int_representable v nbits sgn =
   if nbits >= 64 then true else
-  if sgn then 
+  if sgn then
     let p = Int64.shift_left 1L (nbits - 1) in Int64.neg p <= v && v < p
   else
     0L <= v && v < Int64.shift_left 1L nbits
-  
+
 (* Type of a function definition *)
 
 let fundef_typ fd =
@@ -709,9 +709,9 @@ let pointer_decay env t =
   | TFun _ as ty -> TPtr(ty, [])
   | t -> t
 
-(* The usual unary conversions (H&S 6.3.3) *) 
+(* The usual unary conversions (H&S 6.3.3) *)
 
-let unary_conversion env t = 
+let unary_conversion env t =
   match unroll env t with
   (* Promotion of small integer types *)
   | TInt(kind, attr) ->
@@ -774,7 +774,7 @@ let binary_conversion env t1 t2 =
 
 (* Conversion on function arguments (with protoypes) *)
 
-let argument_conversion env t = 
+let argument_conversion env t =
   (* Arrays and functions degrade automatically to pointers *)
   (* Other types are not changed *)
   match unroll env t with
@@ -970,7 +970,7 @@ let rec eaddrof e =
   match e.edesc with
   | EUnop(Oderef, e1) -> e1
   | EBinop(Ocomma, e1, e2, _) -> ecomma e1 (eaddrof e2)
-  | EConditional(e1, e2, e3) -> 
+  | EConditional(e1, e2, e3) ->
       { edesc = EConditional(e1, eaddrof e2, eaddrof e3); etyp = TPtr(e.etyp, []) }
   | _ -> { edesc = EUnop(Oaddrof, e); etyp = TPtr(e.etyp, []) }
 
@@ -1092,7 +1092,7 @@ let rec subst_stmt phi s =
       | Sblock sl -> Sblock (List.map (subst_stmt phi) sl)
       | Sdecl d -> Sdecl (subst_decl phi d)
       | Sasm(attr, template, outputs, inputs, clob) ->
-          let subst_asm_operand (lbl, cstr, e) = 
+          let subst_asm_operand (lbl, cstr, e) =
             (lbl, cstr, subst_expr phi e) in
           Sasm(attr, template,
                List.map subst_asm_operand outputs,
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index a09316ad..8b6c609b 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -69,7 +69,7 @@ type attr_handling =
   | AttrIgnoreAll
 
 val compatible_types : attr_handling -> Env.t -> typ -> typ -> bool
-  (* Check that the two given types are compatible.  
+  (* Check that the two given types are compatible.
      The attributes in the types are compared according to the first argument:
 - [AttrCompat]: the types must have the same standard attributes
     ([const], [volatile], [restrict]) but may differ on custom attributes.
@@ -229,7 +229,7 @@ val ecommalist :  exp list -> exp -> exp
 val sskip: stmt
   (* The [skip] statement.  No location. *)
 val sseq : location -> stmt -> stmt -> stmt
-  (* Return the statement [s1; s2], optimizing the cases 
+  (* Return the statement [s1; s2], optimizing the cases
      where [s1] or [s2] is [skip], or [s2] is a block. *)
 val sassign : location -> exp -> exp -> stmt
   (* Return the statement [exp1 = exp2;] *)
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 4d3d1d02..0e445b9d 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -103,7 +103,7 @@ let elab_funbody_f : (C.typ -> Env.t -> statement -> C.stmt) ref
 
 (** * Elaboration of constants - C99 section 6.4.4 *)
 
-let has_suffix s suff = 
+let has_suffix s suff =
   let ls = String.length s and lsuff = String.length suff in
   ls >= lsuff && String.sub s (ls - lsuff) lsuff = suff
 
@@ -111,7 +111,7 @@ let chop_last s n =
   assert (String.length s >= n);
   String.sub s 0 (String.length s - n)
 
-let has_prefix s pref = 
+let has_prefix s pref =
   let ls = String.length s and lpref = String.length pref in
   ls >= lpref && String.sub s 0 lpref = pref
 
@@ -195,7 +195,7 @@ let elab_int_constant loc s0 =
   in
   (* Find smallest allowable type that fits *)
   let ty =
-    try List.find (fun ty -> integer_representable v ty) 
+    try List.find (fun ty -> integer_representable v ty)
                   (if base = 10 then dec_kinds else hex_kinds)
     with Not_found ->
       error loc "integer literal '%s' cannot be represented" s0;
@@ -224,7 +224,7 @@ let elab_char_constant loc wide chars =
   let max_digit = Int64.shift_left 1L nbits in
   let max_val = Int64.shift_left 1L (64 - nbits) in
   let v =
-    List.fold_left 
+    List.fold_left
       (fun acc d ->
         if acc < 0L || acc >= max_val then
           error loc "character constant overflows";
@@ -243,7 +243,7 @@ let elab_char_constant loc wide chars =
        IInt)
 
 let elab_string_literal loc wide chars =
-  let nbits = if wide then 8 * !config.sizeof_wchar else 8 in 
+  let nbits = if wide then 8 * !config.sizeof_wchar else 8 in
   let char_max = Int64.shift_left 1L nbits in
   List.iter
     (fun c ->
@@ -390,7 +390,7 @@ let rec elab_specifier ?(only = false) loc env specifier =
   let sto = ref Storage_default
   and inline = ref false
   and attr = ref []
-  and tyspecs = ref [] 
+  and tyspecs = ref []
   and typedef = ref false in
 
   let do_specifier = function
@@ -404,7 +404,7 @@ let rec elab_specifier ?(only = false) loc env specifier =
       | STATIC -> sto := Storage_static
       | EXTERN -> sto := Storage_extern
       | REGISTER -> sto := Storage_register
-      | TYPEDEF -> 
+      | TYPEDEF ->
           if !typedef then
             error loc "multiple uses of 'typedef'";
           typedef := true
@@ -590,7 +590,7 @@ and elab_name env spec (Name (id, decl, attr, loc)) =
   let (sto, inl, tydef, bty, env') = elab_specifier loc env spec in
   if tydef then
     error loc "'typedef' is forbidden here";
-  let (ty, env'') = elab_type_declarator loc env' bty decl in 
+  let (ty, env'') = elab_type_declarator loc env' bty decl in
   let a = elab_attributes env attr in
   (id, sto, inl, add_attributes_type a ty, env'')
 
@@ -605,7 +605,7 @@ and elab_name_group loc env (spec, namelist) =
     error loc "'inline' is forbidden here";
   let elab_one_name env (Name (id, decl, attr, loc)) =
     let (ty, env1) =
-      elab_type_declarator loc env bty decl in 
+      elab_type_declarator loc env bty decl in
     let a = elab_attributes env attr in
     ((id, add_attributes_type a ty), env1) in
   (mmap elab_one_name env' namelist, sto)
@@ -617,7 +617,7 @@ and elab_init_name_group loc env (spec, namelist) =
     elab_specifier ~only:(namelist=[]) loc env spec in
   let elab_one_name env (Init_name (Name (id, decl, attr, loc), init)) =
     let (ty, env1) =
-      elab_type_declarator loc env bty decl in 
+      elab_type_declarator loc env bty decl in
     let a = elab_attributes env attr in
     if inl && not (is_function_type env ty) then
       error loc "'inline' can only appear on functions";
@@ -681,7 +681,7 @@ and elab_field_group env (Field_group (spec, fieldlist, loc)) =
                 error loc "bit size of '%s' is not a compile-time constant" id;
                 None
           end in
-    { fld_name = id; fld_typ = ty; fld_bitfield = optbitsize' } 
+    { fld_name = id; fld_typ = ty; fld_bitfield = optbitsize' }
   in
   (List.map2 elab_bitfield fieldlist names, env')
 
@@ -818,7 +818,7 @@ and elab_enum only loc tag optmembers attrs env =
 
 let elab_type loc env spec decl =
   let (sto, inl, tydef, bty, env') = elab_specifier loc env spec in
-  let (ty, env'') = elab_type_declarator loc env' bty decl in 
+  let (ty, env'') = elab_type_declarator loc env' bty decl in
   if sto <> Storage_default || inl || tydef then
     error loc "'typedef', 'extern', 'static', 'register' and 'inline' are meaningless in cast";
   (ty, env'')
@@ -977,7 +977,7 @@ module I = struct
                  if fld.fld_name = fld1.fld_name
                  then i
                  else default_init env fld1.fld_typ)
-        end 
+        end
     | (TStruct _ | TUnion _), Init_single a ->
         (* This is a previous whole-struct initialization that we
            are going to overwrite.  Revert to the default initializer. *)
@@ -990,7 +990,7 @@ module I = struct
   let index env (z, i as zi) n =
     match unroll env (typeof zi), i with
     | TArray(ty, sz, _), Init_array il ->
-        if n >= 0L && index_below n sz then begin 
+        if n >= 0L && index_below n sz then begin
           let dfl = default_init env ty in
           let rec loop p before after =
             if p = n then
@@ -1044,7 +1044,7 @@ end
 
 let rec elab_designator loc env zi desig =
   match desig with
-  | [] -> 
+  | [] ->
       zi
   | INFIELD_INIT name :: desig' ->
       begin match I.member env zi name with
@@ -1103,7 +1103,7 @@ let rec elab_list zi il first =
 and elab_item zi item il =
   let ty = I.typeof zi in
   match item, unroll env ty with
-  (* Special case char array = "string literal" 
+  (* Special case char array = "string literal"
                or wchar array = L"wide string literal" *)
   | (SINGLE_INIT (CONSTANT (CONST_STRING(w, s)))
      | COMPOUND_INIT [_, SINGLE_INIT(CONSTANT (CONST_STRING(w, s)))]),
@@ -1737,8 +1737,8 @@ let elab_expr loc env a =
     match args, params with
     | [], [] -> []
     | [], _::_ -> err "not enough arguments in function call"; []
-    | _::_, [] -> 
-        if vararg 
+    | _::_, [] ->
+        if vararg
         then args
         else (err "too many arguments in function call"; args)
     | arg1 :: argl, (_, ty_p) :: paraml ->
@@ -1773,7 +1773,7 @@ let elab_for_expr loc env = function
 
 (* Handling of __func__ (section 6.4.2.2) *)
 
-let __func__type_and_init s = 
+let __func__type_and_init s =
   (TArray(TInt(IChar, [AConst]), Some(Int64.of_int (String.length s + 1)), []),
    init_char_array_string None s)
 
@@ -1894,7 +1894,7 @@ let elab_fundef env spec name body loc =
   (* Extract info from type *)
   let (ty_ret, params, vararg, attr) =
     match ty with
-    | TFun(ty_ret, Some params, vararg, attr) -> 
+    | TFun(ty_ret, Some params, vararg, attr) ->
          if wrap incomplete_type loc env1 ty_ret && not (is_void_type env ty_ret) then
            fatal_error loc "return type is an incomplete type";
         (ty_ret, params, vararg, attr)
@@ -1997,7 +1997,7 @@ let rec elab_definition (local: bool) (env: Env.t) (def: Cabs.definition)
 
   (* "int x = 12, y[10], *z" *)
   | DECDEF(init_name_group, loc) ->
-      let ((dl, env1), sto, tydef) = 
+      let ((dl, env1), sto, tydef) =
         elab_init_name_group loc env init_name_group in
       if tydef then
         let env2 = enter_typedefs loc env1 sto dl
@@ -2101,7 +2101,7 @@ let rec elab_stmt env ctx s =
       if not (is_scalar_type env a'.etyp) then
         error loc "the condition of 'if' does not have scalar type";
       let s1' = elab_stmt env ctx s1 in
-      let s2' = 
+      let s2' =
         match s2 with
           | None -> sskip
           | Some s2 -> elab_stmt env ctx s2
@@ -2134,12 +2134,12 @@ let rec elab_stmt env ctx s =
         | Some (FC_DECL def) ->
             let (dcl, env') = elab_definition true (Env.new_scope env) def in
             let loc = elab_loc (get_definitionloc def) in
-            (sskip, env', 
+            (sskip, env',
              Some(List.map (fun d -> {sdesc = Sdecl d; sloc = loc}) dcl)) in
       let a2' =
         match a2 with
           | None -> intconst 1L IInt
-          | Some a2 -> elab_expr loc env' a2 
+          | Some a2 -> elab_expr loc env' a2
       in
       if not (is_scalar_type env' a2'.etyp) then
         error loc "the condition of 'for' does not have scalar type";
diff --git a/cparser/Env.ml b/cparser/Env.ml
index 6610c159..65df6cb9 100644
--- a/cparser/Env.ml
+++ b/cparser/Env.ml
@@ -132,7 +132,7 @@ let lookup_struct env s =
     res
   with Not_found ->
     raise(Error(Unbound_tag(s, "struct")))
- 
+
 let lookup_union env s =
   try
     let (id, ci as res) = IdentMap.lookup s env.env_tag in
@@ -141,7 +141,7 @@ let lookup_union env s =
     res
   with Not_found ->
     raise(Error(Unbound_tag(s, "union")))
- 
+
 let lookup_composite env s =
   try Some (IdentMap.lookup s env.env_tag)
   with Not_found -> None
@@ -191,7 +191,7 @@ let find_union env id =
     ci
   with Not_found ->
     raise(Error(Unbound_tag(id.name, "union")))
- 
+
 let find_member ci m =
   List.find (fun f -> f.fld_name = m) ci
 
@@ -258,7 +258,7 @@ let add_typedef env id info =
 let add_enum env id info =
   let add_enum_item env (id, v, exp) =
     { env with env_ident = IdentMap.add id (II_enum v) env.env_ident } in
-  List.fold_left add_enum_item 
+  List.fold_left add_enum_item
     { env with env_enum = IdentMap.add id info env.env_enum }
     info.ei_members
 
@@ -270,12 +270,12 @@ let composite_tag_name name =
   if name = "" then "<anonymous>" else name
 
 let error_message = function
-  | Unbound_identifier name -> 
+  | Unbound_identifier name ->
       sprintf "Unbound identifier '%s'" name
   | Unbound_tag(name, kind) ->
       sprintf "Unbound %s '%s'" kind (composite_tag_name name)
   | Tag_mismatch(name, expected, actual) ->
-      sprintf "'%s' was declared as a %s but is used as a %s" 
+      sprintf "'%s' was declared as a %s but is used as a %s"
               (composite_tag_name name) actual expected
   | Unbound_typedef name ->
       sprintf "Unbound typedef '%s'" name
diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml
index 05084561..94fcda31 100644
--- a/cparser/ExtendedAsm.ml
+++ b/cparser/ExtendedAsm.ml
@@ -18,7 +18,7 @@
 (* The [transf_asm] function in this module takes a full GCC-style
    extended asm statement and puts it in the form supported by
    CompCert, namely:
-   - 0 or 1 output of kind "r" 
+   - 0 or 1 output of kind "r"
    - 0, 1 or several inputs of kind "r".
    Inputs and outputs of kind "m" (memory location) are emulated
    by taking the address of the operand and treating it as
@@ -116,7 +116,7 @@ let rec transf_inputs loc env accu pos pos' subst = function
         transf_inputs loc env (e :: accu) (pos + 1) (pos' + 1)
                     (set_label_reg lbl pos pos' subst) inputs
       end
-  
+
 (* Transform the output operands:
      - outputs of kind "=m" become an input (equal to the address of the output)
 *)
@@ -147,7 +147,7 @@ let transf_outputs loc env = function
   | outputs ->
       error "%aUnsupported feature: asm statement with 2 or more outputs"
             formatloc loc;
-      (* Bind the outputs so that we don't get another error 
+      (* Bind the outputs so that we don't get another error
          when substituting the text *)
       let rec bind_outputs pos subst = function
       | [] -> (None, [], subst, pos, pos)
@@ -165,7 +165,7 @@ let check_clobbers loc clob =
       || List.mem c' Machregsaux.scratch_register_names
       || c' = "MEMORY" || c' = "CC"
       then ()
-      else error "%aError: unrecognized asm register clobber '%s'" 
+      else error "%aError: unrecognized asm register clobber '%s'"
                  formatloc loc c)
     clob
 
@@ -174,7 +174,7 @@ let check_clobbers loc clob =
 let re_asm_placeholder =
   Str.regexp "\\(%[QR]?\\([0-9]+\\|\\[[a-zA-Z_][a-zA-Z_0-9]*\\]\\)\\|%%\\)"
 
-let rename_placeholders loc template subst =       
+let rename_placeholders loc template subst =
   let rename p =
     if p = "%%" then p else
       try
diff --git a/cparser/GCC.ml b/cparser/GCC.ml
index 030f300b..f7f64a4e 100644
--- a/cparser/GCC.ml
+++ b/cparser/GCC.ml
@@ -65,7 +65,7 @@ let builtins = {
   "__builtin_acosl",  (longDoubleType, [ longDoubleType ], false);
 
   "__builtin_alloca",  (voidPtrType, [ uintType ], false);
-  
+
   "__builtin_asin",  (doubleType, [ doubleType ], false);
   "__builtin_asinf",  (floatType, [ floatType ], false);
   "__builtin_asinl",  (longDoubleType, [ longDoubleType ], false);
@@ -76,7 +76,7 @@ let builtins = {
 
   "__builtin_atan2",  (doubleType, [ doubleType; doubleType ], false);
   "__builtin_atan2f",  (floatType, [ floatType; floatType ], false);
-  "__builtin_atan2l",  (longDoubleType, [ longDoubleType; 
+  "__builtin_atan2l",  (longDoubleType, [ longDoubleType;
                                                 longDoubleType ], false);
 
   "__builtin_ceil",  (doubleType, [ doubleType ], false);
@@ -133,12 +133,12 @@ let builtins = {
 
   "__builtin_frexp",  (doubleType, [ doubleType; intPtrType ], false);
   "__builtin_frexpf",  (floatType, [ floatType; intPtrType  ], false);
-  "__builtin_frexpl",  (longDoubleType, [ longDoubleType; 
+  "__builtin_frexpl",  (longDoubleType, [ longDoubleType;
                                                 intPtrType  ], false);
 
   "__builtin_ldexp",  (doubleType, [ doubleType; intType ], false);
   "__builtin_ldexpf",  (floatType, [ floatType; intType  ], false);
-  "__builtin_ldexpl",  (longDoubleType, [ longDoubleType; 
+  "__builtin_ldexpl",  (longDoubleType, [ longDoubleType;
                                                 intType  ], false);
 
   "__builtin_log",  (doubleType, [ doubleType ], false);
@@ -149,10 +149,10 @@ let builtins = {
   "__builtin_log10f",  (floatType, [ floatType ], false);
   "__builtin_log10l",  (longDoubleType, [ longDoubleType ], false);
 
-  "__builtin_modff",  (floatType, [ floatType; 
+  "__builtin_modff",  (floatType, [ floatType;
                                           TPtr(floatType,[]) ], false);
-  "__builtin_modfl",  (longDoubleType, [ longDoubleType; 
-                                               TPtr(longDoubleType, []) ], 
+  "__builtin_modfl",  (longDoubleType, [ longDoubleType;
+                                               TPtr(longDoubleType, []) ],
                              false);
 
   "__builtin_nan",  (doubleType, [ charConstPtrType ], false);
@@ -210,7 +210,7 @@ let builtins = {
   "__builtin_tanhl",  (longDoubleType, [ longDoubleType ], false);
 
   "__builtin_va_end",  (voidType, [ voidPtrType ], false);
-  "__builtin_varargs_start",  
+  "__builtin_varargs_start",
     (voidType, [ voidPtrType ], false);
   (* When we elaborate builtin_stdarg_start/builtin_va_start,
      second argument is passed by address *)
diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml
index ca6c9da5..c163989e 100644
--- a/cparser/PackedStructs.ml
+++ b/cparser/PackedStructs.ml
@@ -190,7 +190,7 @@ let bswap_write loc env lhs rhs =
       let (id, fty) =
         lookup_function loc env (sprintf "__builtin_write%d_reversed" bsize) in
       let fn = {edesc = EVar id; etyp = fty} in
-      let args = [ecast_opt env (TPtr(aty,[])) (eaddrof lhs); 
+      let args = [ecast_opt env (TPtr(aty,[])) (eaddrof lhs);
                   ecast_opt env aty rhs] in
       {edesc = ECall(fn, args); etyp = TVoid[]}
     end else begin
@@ -216,7 +216,7 @@ let transf_expr loc env ctx e =
   let is_byteswapped_ptr ty fieldname =
     match unroll env ty with
     | TPtr(ty', _) -> is_byteswapped ty' fieldname
-    | _ -> false in 
+    | _ -> false in
 
   (* Transformation of l-values.  Return transformed expr plus
      [true] if l-value is a byte-swapped field and [false] otherwise. *)
@@ -232,7 +232,7 @@ let transf_expr loc env ctx e =
         let (e1', swap) = lvalue e1 in
         ({edesc = EBinop(Oindex, e1', e2, tyres); etyp = e.etyp}, swap)
     | _ ->
-        (texp Val e, false) 
+        (texp Val e, false)
 
   and texp ctx e =
     match e.edesc with
@@ -401,7 +401,7 @@ let rec transf_globdecls env accu = function
           let attr' =
             match su with
             | Union -> attr
-            | Struct -> remove_custom_attributes  ["packed";"__packed__"] attr in 
+            | Struct -> remove_custom_attributes  ["packed";"__packed__"] attr in
           transf_globdecls
             (Env.add_composite env id (composite_info_decl env su attr'))
             ({g with gdesc = Gcompositedecl(su, id, attr')} :: accu)
diff --git a/cparser/Rename.ml b/cparser/Rename.ml
index b0dc120f..4b387b0d 100644
--- a/cparser/Rename.ml
+++ b/cparser/Rename.ml
@@ -42,20 +42,20 @@ let enter_public env id =
     { re_id = IdentMap.add id id env.re_id;
       re_public = StringMap.add id.name id env.re_public;
       re_used = StringSet.add id.name env.re_used }
-      
+
 let enter_static env id file =
   try
     let id' = StringMap.find id.name env.re_public in
     { env with re_id = IdentMap.add id id' env.re_id }
   with Not_found ->
     let file = String.map (fun a -> match a with 'a'..'z' | 'A'..'Z' | '0'..'9' -> a | _ -> '_') file in
-    let id' = {id with name = Printf.sprintf "_%s_%s" file id.name} in 
+    let id' = {id with name = Printf.sprintf "_%s_%s" file id.name} in
     { re_id = IdentMap.add id id' env.re_id;
       re_public = env.re_public;
       re_used = StringSet.add id'.name env.re_used }
 
 (* For static or local identifiers, we make up a new name if needed *)
-(* If the same identifier has already been declared, 
+(* If the same identifier has already been declared,
    don't rename a second time *)
 
 let rename env id =
@@ -94,7 +94,7 @@ let ident env id =
   try
     IdentMap.find id env.re_id
   with Not_found ->
-    Cerrors.fatal_error "Internal error: Rename: %s__%d unbound" 
+    Cerrors.fatal_error "Internal error: Rename: %s__%d unbound"
                         id.name id.stamp
 
 let rec typ env = function
@@ -111,7 +111,7 @@ let rec typ env = function
   | ty -> ty
 
 and param env (id, ty) =
-  if id.name = "" then 
+  if id.name = "" then
     ((id, typ env ty), env)
   else
     let (id', env') = rename env id in ((id', typ env' ty), env')
@@ -216,7 +216,7 @@ let fundef env f =
       fd_body = stmt env2 f.fd_body },
     env0 )
 
-let enum env (id, v, opte) = 
+let enum env (id, v, opte) =
   let (id', env') = rename env id in
   ((id', v, optexp env' opte), env')
 
@@ -269,7 +269,7 @@ let rec reserve_public env file = function
             begin match sto with
             | Storage_default | Storage_extern -> enter_public env id
             | Storage_static -> if !Clflags.option_rename_static then
-                enter_static env id file 
+                enter_static env id file
                   else
                 env
             | _ -> assert false
@@ -292,4 +292,4 @@ let program p file =
   globdecls
     (reserve_public (reserve_builtins()) file p)
     [] p
-  
+
diff --git a/cparser/StructReturn.ml b/cparser/StructReturn.ml
index 5e5602f3..2c6fd1d2 100644
--- a/cparser/StructReturn.ml
+++ b/cparser/StructReturn.ml
@@ -71,7 +71,7 @@ let classify_param env ty =
     | SP_ref_caller -> Param_ref_caller
     | _ ->
       match sizeof env ty, alignof env ty with
-      | Some sz, Some al -> 
+      | Some sz, Some al ->
           Param_flattened ((sz + 3) / 4, sz, al)
       | _, _ ->
           Param_unchanged  (* should not happen *)
@@ -306,7 +306,7 @@ let rec transf_expr env ctx e =
 
    We used to do a copy optimization:
      ctx = Effects:   lv = f(...)     -> f(&lv, ...)
-   but it is not correct in case of overlap (see test/regression/struct12.c) 
+   but it is not correct in case of overlap (see test/regression/struct12.c)
 
    Function calls returning a composite by value:
     ctx = Effects:   lv = f(...)     -> newtemp = f(...), lv = newtemp
@@ -521,8 +521,8 @@ let rec transf_funparams loc env params =
           let tpx = TPtr(tx', []) in
           let ex = { edesc = EVar x; etyp = tpx } in
           let estarx = { edesc = EUnop(Oderef, ex); etyp = tx' } in
-          ((x, tpx) :: params', 
-           actions, 
+          ((x, tpx) :: params',
+           actions,
            IdentMap.add x estarx subst)
       | Param_flattened(n, sz, al) ->
           let y = new_temp ~name:x.name (ty_buffer n) in
@@ -562,7 +562,7 @@ let transf_fundef env f =
     | Ret_value(ty, sz, al) ->
         (f.fd_attrib,
          ty,
-         params, 
+         params,
          transf_funbody env (subst_stmt subst f.fd_body) None) in
   let temps = get_temps() in
   {f with fd_attrib = attr1;
diff --git a/cparser/Transform.ml b/cparser/Transform.ml
index 6cdd8a6b..840234b8 100644
--- a/cparser/Transform.ml
+++ b/cparser/Transform.ml
@@ -81,7 +81,7 @@ let op_for_assignop = function
   | Odiv_assign -> Odiv
   | Omod_assign -> Omod
   | Oand_assign -> Oand
-  | Oor_assign -> Oor 
+  | Oor_assign -> Oor
   | Oxor_assign -> Oxor
   | Oshl_assign -> Oshl
   | Oshr_assign -> Oshr
@@ -118,7 +118,7 @@ let expand_assignop ~read ~write env ctx op l r ty =
         ecomma (eassign tmp res) (ecomma (write l tmp) tmp))
 
 let expand_preincrdecr ~read ~write env ctx op l =
-  expand_assignop ~read ~write env ctx (assignop_for_incr_decr op) 
+  expand_assignop ~read ~write env ctx (assignop_for_incr_decr op)
               l (intconst 1L IInt) (unary_conversion env l.etyp)
 
 let expand_postincrdecr ~read ~write env ctx op l =
@@ -147,7 +147,7 @@ let stmt ~expr ?(decl = fun env decl -> assert false) env s =
   | Sskip -> s
   | Sdo e ->
       {s with sdesc = Sdo(expr s.sloc env Effects e)}
-  | Sseq(s1, s2) -> 
+  | Sseq(s1, s2) ->
       {s with sdesc = Sseq(stm s1, stm s2)}
   | Sif(e, s1, s2) ->
       {s with sdesc = Sif(expr s.sloc env Val e, stm s1, stm s2)}
diff --git a/cparser/Transform.mli b/cparser/Transform.mli
index 57a4737b..a04896a9 100644
--- a/cparser/Transform.mli
+++ b/cparser/Transform.mli
@@ -64,11 +64,11 @@ val fundef : (Env.t -> C.stmt -> C.stmt) -> Env.t -> C.fundef -> C.fundef
 val program :
   ?decl:(Env.t -> C.decl -> C.decl) ->
   ?fundef:(Env.t -> C.fundef -> C.fundef) ->
-  ?composite:(Env.t -> C.struct_or_union -> 
-                C.ident -> C.attributes -> C.field list -> 
+  ?composite:(Env.t -> C.struct_or_union ->
+                C.ident -> C.attributes -> C.field list ->
                   C.attributes * C.field list) ->
   ?typedef:(Env.t -> C.ident -> C.typ -> C.typ) ->
-  ?enum:(Env.t -> C.ident -> C.attributes -> C.enumerator list -> 
+  ?enum:(Env.t -> C.ident -> C.attributes -> C.enumerator list ->
                   C.attributes * C.enumerator list) ->
   ?pragma:(Env.t -> string -> string) ->
   C.program ->
diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index c6646b5c..405cf755 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -49,7 +49,7 @@ let rec local_initializer env path init k =
   | Init_struct(id, fil) ->
       let field_init (fld, i) k =
         local_initializer env
-          { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ } 
+          { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ }
           i k in
       List.fold_right field_init fil k
   | Init_union(id, fld, i) ->
@@ -80,7 +80,7 @@ let add_inits_expr inits e =
 let local_variables = ref ([]: decl list)
 let global_variables = ref ([]: decl list)
 
-(* Note: "const int x = y - 1;" is legal, but we turn it into 
+(* Note: "const int x = y - 1;" is legal, but we turn it into
    "const int x; x = y - 1;", which is not.  Therefore, remove
    top-level 'const' attribute.  Also remove it on element type of
    array type. *)
@@ -128,7 +128,7 @@ let rec expand_expr islocal env e =
         let e2' =
           match op with
           | Ocomma | Ologand | Ologor -> expand_expr islocal env e2
-              (* Make sure the initializers of [e2] are performed in 
+              (* Make sure the initializers of [e2] are performed in
                  sequential order, i.e. just before [e2] but after [e1]. *)
           | _ -> expand e2 in
         {edesc = EBinop(op, e1', e2', ty); etyp = e.etyp}
@@ -148,7 +148,7 @@ let rec expand_expr islocal env e =
         e'
     | ECall(e1, el) ->
         {edesc = ECall(expand e1, List.map expand el); etyp = e.etyp}
-  in 
+  in
     let e' = expand e in ecommalist !inits e'
 
 (* Elimination of compound literals within an initializer. *)
@@ -185,7 +185,7 @@ let debug_ty =
 
 let debug_annot kind args =
   { sloc = no_loc;
-    sdesc = Sdo { 
+    sdesc = Sdo {
       etyp = TVoid [];
       edesc = ECall({edesc = EVar debug_id; etyp = debug_ty},
                     intconst kind IInt :: args)
@@ -276,12 +276,12 @@ let rec unblock_stmt env ctx ploc s =
   | Sseq(s1, s2) ->
       {s with sdesc = Sseq(unblock_stmt env ctx ploc s1,
                            unblock_stmt env ctx s1.sloc s2)}
-  | Sif(e, s1, s2) -> 
+  | Sif(e, s1, s2) ->
       add_lineno ctx ploc s.sloc
         {s with sdesc = Sif(expand_expr true env e,
                             unblock_stmt env ctx s.sloc s1,
                             unblock_stmt env ctx s.sloc s2)}
-  | Swhile(e, s1) -> 
+  | Swhile(e, s1) ->
       add_lineno ctx ploc s.sloc
         {s with sdesc = Swhile(expand_expr true env e,
                                unblock_stmt env ctx s.sloc s1)}
@@ -301,7 +301,7 @@ let rec unblock_stmt env ctx ploc s =
       add_lineno ctx ploc s.sloc
         {s with sdesc = Sswitch(expand_expr true env e,
                                 unblock_stmt env ctx s.sloc s1)}
-  | Slabeled(lbl, s1) -> 
+  | Slabeled(lbl, s1) ->
       add_lineno ctx ploc s.sloc
         {s with sdesc = Slabeled(lbl, unblock_stmt env ctx s.sloc s1)}
   | Sgoto lbl ->
@@ -309,7 +309,7 @@ let rec unblock_stmt env ctx ploc s =
   | Sreturn None ->
       add_lineno ctx ploc s.sloc s
   | Sreturn (Some e) ->
-      add_lineno ctx ploc s.sloc 
+      add_lineno ctx ploc s.sloc
         {s with sdesc = Sreturn(Some (expand_expr true env e))}
   | Sblock sl ->
       let ctx' =
@@ -327,7 +327,7 @@ let rec unblock_stmt env ctx ploc s =
   | Sasm(attr, template, outputs, inputs, clob) ->
       let expand_asm_operand (lbl, cstr, e) =
         (lbl, cstr, expand_expr true env e) in
-      add_lineno ctx ploc s.sloc 
+      add_lineno ctx ploc s.sloc
         {s with sdesc = Sasm(attr, template,
                              List.map expand_asm_operand outputs,
                              List.map expand_asm_operand inputs, clob)}
diff --git a/debug/Debug.ml b/debug/Debug.ml
index 25517eee..806ebb08 100644
--- a/debug/Debug.ml
+++ b/debug/Debug.ml
@@ -20,7 +20,7 @@ open DwarfTypes
 (* Interface for generating and printing debug information *)
 
 (* Record used for stroring references to the actual implementation functions *)
-type implem = 
+type implem =
     {
       init: string -> unit;
       atom_global: ident -> atom -> unit;
diff --git a/debug/Debug.mli b/debug/Debug.mli
index 553e1412..145927f4 100644
--- a/debug/Debug.mli
+++ b/debug/Debug.mli
@@ -18,7 +18,7 @@ open BinNums
 
 
 (* Record used for stroring references to the actual implementation functions *)
-type implem = 
+type implem =
     {
      init: string -> unit;
      atom_global: ident -> atom -> unit;
diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml
index 96f55f40..55d49e72 100644
--- a/debug/DebugInformation.ml
+++ b/debug/DebugInformation.ml
@@ -17,7 +17,7 @@ open Camlcoq
 open Cutil
 open DebugTypes
 
-(* This implements an interface for the collection of debugging 
+(* This implements an interface for the collection of debugging
    information. *)
 
 (* Simple id generator *)
@@ -71,20 +71,20 @@ let find_type (ty: typ) =
 (* Add type and information *)
 let insert_type (ty: typ) =
   let insert d_ty ty =
-    let id = next_id () 
+    let id = next_id ()
     and name = typ_to_string ty in
     Hashtbl.add types id d_ty;
     Hashtbl.add lookup_types name id;
     id in
   (* We are only interrested in Const and Volatile *)
   let ty = strip_attributes ty in
-  let rec typ_aux ty = 
+  let rec typ_aux ty =
     try find_type ty with
     | Not_found ->
         let d_ty =
           match ty with
           | TVoid _ -> Void
-          | TInt (k,_) -> 
+          | TInt (k,_) ->
               IntegerType ({int_kind = k })
           | TFloat (k,_) ->
               FloatType ({float_kind = k})
@@ -104,14 +104,14 @@ let insert_type (ty: typ) =
               } in
               ArrayType arr
           | TFun (t,param,va,_) ->
-              let param,prot = (match param with 
+              let param,prot = (match param with
               | None -> [],false
-              | Some p -> List.map (fun (i,t) -> let t = attr_aux t in 
+              | Some p -> List.map (fun (i,t) -> let t = attr_aux t in
                 {
                  param_type = t;
-                 param_name = i.name;               
+                 param_name = i.name;
                }) p,true) in
-              let ret = (match t with 
+              let ret = (match t with
               | TVoid _ -> None
               | _ -> Some (attr_aux t)) in
               let ftype = {
@@ -155,7 +155,7 @@ let insert_type (ty: typ) =
                } in
               CompositeType union
           | TEnum (id,_) ->
-              let enum = 
+              let enum =
                 {
                  enum_name = id.name;
                  enum_byte_size = None;
@@ -164,13 +164,13 @@ let insert_type (ty: typ) =
                } in
               EnumType enum in
         insert d_ty ty
-  and attr_aux ty = 
+  and attr_aux ty =
     try
       find_type ty
     with
       Not_found ->
         match strip_last_attribute ty with
-        | Some AConst,t -> 
+        | Some AConst,t ->
             let id = attr_aux t in
             let const = { cst_type = id} in
             insert (ConstType const) ty
@@ -285,7 +285,7 @@ let replace_scope id var =
   let var = Scope var in
   Hashtbl.replace local_variables id var
 
-let gen_comp_typ sou id at = 
+let gen_comp_typ sou id at =
   if sou = Struct then
     TStruct (id,at)
   else
@@ -329,11 +329,11 @@ let insert_global_declaration env dec=
         end
       end else begin
         (* Implict declarations need special handling *)
-        let id' = try Hashtbl.find name_to_definition id.name with Not_found -> 
+        let id' = try Hashtbl.find name_to_definition id.name with Not_found ->
           let id' = next_id () in
           Hashtbl.add name_to_definition id.name id';id' in
         Hashtbl.add stamp_to_definition id.stamp id'
-      end       
+      end
   | Gfundef f ->
       let ret =  (match f.fd_ret with
       | TVoid _ -> None
@@ -350,7 +350,7 @@ let insert_global_declaration env dec=
          parameter_type = ty;
        }) f.fd_params in
       let fd =
-      { 
+      {
         fun_name = f.fd_name.name;
         fun_atom = None;
         fun_file_loc = dec.gloc;
@@ -363,19 +363,19 @@ let insert_global_declaration env dec=
         fun_scope = None;
       } in
       begin
-        let id' = try Hashtbl.find name_to_definition f.fd_name.name with Not_found -> 
+        let id' = try Hashtbl.find name_to_definition f.fd_name.name with Not_found ->
           let id' = next_id () in
           Hashtbl.add name_to_definition f.fd_name.name id';id' in
         Hashtbl.add stamp_to_definition f.fd_name.stamp id';
         Hashtbl.add definitions id' (Function fd)
       end
-  | Gcompositedecl (sou,id,at) -> 
+  | Gcompositedecl (sou,id,at) ->
       ignore (insert_type (gen_comp_typ sou id at));
       let id = find_type (gen_comp_typ sou id []) in
       replace_composite id (fun comp -> if comp.ct_file_loc = None then
         {comp with ct_file_loc = Some (dec.gloc);}
       else comp)
-  | Gcompositedef (sou,id,at,fi) -> 
+  | Gcompositedef (sou,id,at,fi) ->
       ignore (insert_type (gen_comp_typ sou id at));
       let id = find_type (gen_comp_typ sou id []) in
       let fi = List.filter (fun f -> f.fld_name <> "") fi in (* Fields without names need no info *)
@@ -392,15 +392,15 @@ let insert_global_declaration env dec=
       replace_composite id (fun comp ->
         let loc = if comp.ct_file_loc = None then Some dec.gloc else comp.ct_file_loc in
         {comp with ct_file_loc = loc; ct_members = fields; ct_declaration = false;})
-  | Gtypedef (id,t) -> 
+  | Gtypedef (id,t) ->
       let id = insert_type (TNamed (id,[])) in
       let tid = insert_type t in
       replace_typedef id (fun typ -> {typ with typedef_file_loc = Some dec.gloc; typ = Some tid;});
-  | Genumdef (n,at,e) -> 
+  | Genumdef (n,at,e) ->
       ignore(insert_type (TEnum (n,at)));
       let id = find_type (TEnum (n,[])) in
       let enumerator = List.map (fun (i,c,_) ->
-        {    
+        {
              enumerator_name = i.name;
              enumerator_const = c;
        }) e in
@@ -411,19 +411,19 @@ let insert_global_declaration env dec=
 let set_member_offset str field offset =
   let id = find_type (TStruct (str,[])) in
   replace_composite id (fun comp ->
-    let name f = f.cfd_name = field || match f.cfd_bitfield with Some n -> n = field | _ -> false in 
+    let name f = f.cfd_name = field || match f.cfd_bitfield with Some n -> n = field | _ -> false in
     let members = list_replace name (fun a -> {a with cfd_byte_offset = Some offset;}) comp.ct_members in
     {comp with ct_members = members;})
 
 let set_composite_size comp sou size =
   let id = find_type (gen_comp_typ sou comp []) in
-  replace_composite id (fun comp -> {comp with ct_sizeof = size;}) 
+  replace_composite id (fun comp -> {comp with ct_sizeof = size;})
 
 let set_bitfield_offset str field offset underlying size =
   let id = find_type (TStruct (str,[])) in
   replace_composite id (fun comp ->
     let name f = f.cfd_name = field in
-    let members = list_replace name (fun a -> 
+    let members = list_replace name (fun a ->
       {a with cfd_bit_offset = Some offset; cfd_bitfield = Some underlying; cfd_byte_size = Some size})
         comp.ct_members in
     {comp with ct_members = members;})
@@ -433,10 +433,10 @@ let atom_global id atom =
     let id' = (Hashtbl.find stamp_to_definition id.stamp) in
     let g = Hashtbl.find definitions id' in
     match g with
-    | Function f ->    
+    | Function f ->
         replace_fun id' ({f with fun_atom = Some atom;});
         Hashtbl.add atom_to_definition atom id';
-        Hashtbl.iter (fun (fid,sid) tid -> if fid = id.stamp then 
+        Hashtbl.iter (fun (fid,sid) tid -> if fid = id.stamp then
           Hashtbl.add atom_to_scope (atom,sid) tid) scope_to_local
     | GlobalVariable var ->
         replace_var id' ({var with gvar_atom = Some atom;})
@@ -449,7 +449,7 @@ let atom_parameter fid id atom =
     let params = list_replace name (fun p -> {p with parameter_atom = Some atom;}) f.fun_parameter in
     replace_fun fid' ({f with fun_parameter = params;})
   with Not_found -> ()
-    
+
 let add_fun_addr atom (high,low) =
   try
     let id,f = find_fun_atom atom in
@@ -465,7 +465,7 @@ let atom_local_variable id atom =
 let add_lvar_scope f_id var_id s_id =
   try
     let s_id',scope = find_scope_id f_id s_id in
-    let var_id,_ = find_lvar_stamp var_id.stamp in 
+    let var_id,_ = find_lvar_stamp var_id.stamp in
     replace_scope s_id' ({scope_variables = var_id::scope.scope_variables;})
   with Not_found -> ()
 
@@ -543,7 +543,7 @@ let close_scope atom s_id lbl =
   try
     let s_id = Hashtbl.find atom_to_scope (atom,s_id) in
     let old_r = try Hashtbl.find scope_ranges s_id with Not_found -> [] in
-    let last_r,rest = 
+    let last_r,rest =
       begin
         match old_r with
         | a::rest -> a,rest
diff --git a/debug/DebugTypes.mli b/debug/DebugTypes.mli
index 6a4f619c..b2f19f7a 100644
--- a/debug/DebugTypes.mli
+++ b/debug/DebugTypes.mli
@@ -68,7 +68,7 @@ type enum_type = {
     enum_name:        string;
     enum_byte_size:   int option;
     enum_file_loc:    location option;
-    enum_enumerators: enumerator list; 
+    enum_enumerators: enumerator list;
   }
 
 type int_type = {
@@ -115,7 +115,7 @@ type global_variable_information = {
     gvar_type:        int;
   }
 
-type parameter_information = 
+type parameter_information =
  {
   parameter_name:     string;
   parameter_ident:    int;
@@ -150,7 +150,7 @@ type local_variable_information = {
     lvar_static:  bool;  (* Static variable are mapped to symbols *)
   }
 
-type scope_information = 
+type scope_information =
   {
    scope_variables: int list; (* Variable and Scope ids *)
  }
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index 12ad16bf..b7ecb62c 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -85,7 +85,7 @@ module DwarfPrinter(Target: DWARF_TARGET):
       | Some (LocSymbol _)
       | Some (LocSimple _) -> add_abbr_entry (0x2,location_block_type_abbr) buf
 
-   
+
 
     (* Dwarf entity to string function *)
     let abbrev_string_of_entity entity has_sibling =
@@ -326,7 +326,7 @@ module DwarfPrinter(Target: DWARF_TARGET):
           print_uleb128 oc col
       | Some (Gnu_file_loc (file,col)) ->
           fprintf oc "	.4byte		%l\n" file;
-          print_uleb128 oc col 
+          print_uleb128 oc col
      | None -> ()
 
     let print_loc_expr oc = function
@@ -472,7 +472,7 @@ module DwarfPrinter(Target: DWARF_TARGET):
     let print_subprogram_addr oc (s,e) =
       fprintf oc "	.4byte		%a\n" label e;
       fprintf oc "	.4byte		%a\n" label s
-     
+
     let print_subprogram oc sp =
       print_file_loc oc (Some sp.subprogram_file_loc);
       print_opt_value oc sp.subprogram_external print_flag;
@@ -603,7 +603,7 @@ module DwarfPrinter(Target: DWARF_TARGET):
       print_abbrev oc;
       List.iter (fun e ->
         let name = if e.section_name <> ".text" then Some e.section_name else None in
-        section oc (Section_debug_info name);      
+        section oc (Section_debug_info name);
         print_debug_info oc e.start_label e.line_label e.entry) entries;
       section oc Section_debug_loc;
       List.iter (fun e -> print_location_list oc e.locs) entries
diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli
index c7e5dce1..7048d8d3 100644
--- a/debug/DwarfTypes.mli
+++ b/debug/DwarfTypes.mli
@@ -47,7 +47,7 @@ type location_value =
   | LocRef of address
   | LocSimple of location_expression
   | LocList of location_expression list
-        
+
 type data_location_value =
   | DataLocBlock of location_expression
   | DataLocRef of reference
@@ -62,10 +62,10 @@ type string_const =
 
 (* Types representing the attribute information per tag value *)
 
-type file_loc = 
+type file_loc =
   | Diab_file_loc of constant * constant
   | Gnu_file_loc of constant * constant
-     
+
 type dw_tag_array_type =
     {
      array_type:          reference;
diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml
index 78c4fffb..1ef3938a 100644
--- a/debug/Dwarfgen.ml
+++ b/debug/Dwarfgen.ml
@@ -58,20 +58,20 @@ module type TARGET =
 
 module Dwarfgenaux (Target: TARGET) =
   struct
-    
+
     include Target
 
     let name_opt n = if n <> "" then Some (string_entry n) else None
-    
+
     (* Functions to translate the basetypes. *)
     let int_type_to_entry id i =
       let encoding =
         (match i.int_kind with
         | IBool -> DW_ATE_boolean
         | IChar ->
-            if !Machine.config.Machine.char_signed then 
-              DW_ATE_signed_char 
-            else 
+            if !Machine.config.Machine.char_signed then
+              DW_ATE_signed_char
+            else
               DW_ATE_unsigned_char
         | IInt | ILong | ILongLong | IShort | ISChar -> DW_ATE_signed
         | _ -> DW_ATE_unsigned)in
@@ -82,7 +82,7 @@ module Dwarfgenaux (Target: TARGET) =
       } in
       new_entry id (DW_TAG_base_type int)
 
-    let float_type_to_entry id f = 
+    let float_type_to_entry id f =
       let byte_size = sizeof_fkind f.float_kind in
       let float = {
         base_type_byte_size = byte_size;
@@ -102,7 +102,7 @@ module Dwarfgenaux (Target: TARGET) =
     let file_loc_opt = function
       | None -> None
       | Some (f,l) ->
-          try 
+          try
             Some (file_loc (f,l))
           with Not_found -> None
 
@@ -113,7 +113,7 @@ module Dwarfgenaux (Target: TARGET) =
         typedef_name = string_entry t.typedef_name;
         typedef_type = i;
       } in
-      new_entry id (DW_TAG_typedef td) 
+      new_entry id (DW_TAG_typedef td)
 
     let pointer_to_entry id p =
       let p = {pointer_type = p.pts} in
@@ -192,8 +192,8 @@ module Dwarfgenaux (Target: TARGET) =
         member_bit_offset = mem.cfd_bit_offset;
         member_bit_size = mem.cfd_bit_size;
         member_data_member_location =
-        (match mem.cfd_byte_offset with 
-        | None -> None 
+        (match mem.cfd_byte_offset with
+        | None -> None
         | Some s -> Some (DataLocBlock (DW_OP_plus_uconst s)));
         member_declaration = None;
         member_name = string_entry mem.cfd_name;
@@ -245,19 +245,19 @@ module Dwarfgenaux (Target: TARGET) =
       let add_type id d =
         if not (IntSet.mem id d) then
           IntSet.add id d,true
-        else 
+        else
           d,false in
       let t = Hashtbl.find types id in
       match t with
-      | IntegerType _ 
+      | IntegerType _
       | FloatType _
       | Void
       | EnumType _ -> d,false
       | Typedef t ->
           add_type (get_opt_val t.typ) d
-      | PointerType p -> 
+      | PointerType p ->
           add_type p.pts d
-      | ArrayType arr -> 
+      | ArrayType arr ->
           add_type arr.arr_type d
       | ConstType c ->
           add_type c.cst_type d
@@ -265,12 +265,12 @@ module Dwarfgenaux (Target: TARGET) =
           add_type v.vol_type d
       | FunctionType f ->
           let d,c = match f.fun_return_type with
-          | Some t -> add_type t d 
+          | Some t -> add_type t d
           | None -> d,false in
           List.fold_left (fun (d,c) p ->
             let d,c' = add_type p.param_type d in
             d,c||c') (d,c) f.fun_params
-      | CompositeType c -> 
+      | CompositeType c ->
           List.fold_left (fun (d,c) f ->
             let d,c' = add_type f.cfd_typ d in
             d,c||c') (d,false) c.ct_members
@@ -285,10 +285,10 @@ module Dwarfgenaux (Target: TARGET) =
         else
           d in
       let typs = aux needed in
-      List.rev (Hashtbl.fold (fun id t acc -> 
+      List.rev (Hashtbl.fold (fun id t acc ->
         if IntSet.mem id typs then
           (infotype_to_entry id t)::acc
-        else 
+        else
           acc) types [])
 
     let global_variable_to_entry acc id v =
@@ -309,13 +309,13 @@ module Dwarfgenaux (Target: TARGET) =
     let gen_splitlong op_hi op_lo =
       let op_piece = DW_OP_piece 4 in
       op_piece::op_hi@(op_piece::op_lo)
-                         
-    let translate_function_loc a = function 
+
+    let translate_function_loc a = function
       | BA_addrstack (ofs) ->
           let ofs = camlint_of_coqint ofs in
           Some (LocSimple (DW_OP_bregx (a,ofs))),[]
       | BA_splitlong (BA_addrstack hi,BA_addrstack lo)->
-          let hi = camlint_of_coqint hi 
+          let hi = camlint_of_coqint hi
           and lo = camlint_of_coqint lo in
           if lo = Int32.add hi 4l then
             Some (LocSimple (DW_OP_bregx (a,hi))),[]
@@ -324,11 +324,11 @@ module Dwarfgenaux (Target: TARGET) =
             and op_lo = [DW_OP_bregx (a,lo)] in
             Some (LocList (gen_splitlong op_hi op_lo)),[]
       | _ -> None,[]
-            
+
     let range_entry_loc (sp,l) =
       let rec aux = function
         | BA i ->  [DW_OP_reg i]
-        | BA_addrstack ofs -> 
+        | BA_addrstack ofs ->
             let ofs = camlint_of_coqint ofs in
             [DW_OP_bregx (sp,ofs)]
         | BA_splitlong (hi,lo) ->
@@ -343,12 +343,12 @@ module Dwarfgenaux (Target: TARGET) =
 
     let location_entry f_id atom =
       try
-        begin 
+        begin
           match (Hashtbl.find var_locations (f_id,atom)) with
           | FunctionLoc (a,r) ->
               translate_function_loc a r
           | RangeLoc l ->
-              let l = List.rev_map (fun i -> 
+              let l = List.rev_map (fun i ->
                 let hi = get_opt_val i.range_start
                 and lo = get_opt_val i.range_end in
                 let hi = Hashtbl.find label_translation (f_id,hi)
@@ -388,8 +388,8 @@ module Dwarfgenaux (Target: TARGET) =
     and scope_to_entry  f_id acc sc id =
       let l_pc,h_pc = try
         let r = Hashtbl.find scope_ranges id in
-        let lbl l = match l with 
-        | Some l -> Some (Hashtbl.find label_translation (f_id,l)) 
+        let lbl l = match l with
+        | Some l -> Some (Hashtbl.find label_translation (f_id,l))
         | None -> None in
         begin
           match r with
@@ -409,8 +409,8 @@ module Dwarfgenaux (Target: TARGET) =
     and local_to_entry f_id acc id =
       match Hashtbl.find local_variables id with
       | LocalVariable v -> local_variable_to_entry f_id acc v id
-      | Scope v -> let s,acc = 
-          (scope_to_entry f_id acc v id) in 
+      | Scope v -> let s,acc =
+          (scope_to_entry f_id acc v id) in
         Some s,acc
 
     let fun_scope_to_entries f_id acc id =
@@ -438,7 +438,7 @@ module Dwarfgenaux (Target: TARGET) =
       let params,(acc,bcc) = mmap (function_parameter_to_entry f_id) (acc,bcc) f.fun_parameter in
       let vars,(acc,bcc) = fun_scope_to_entries f_id (acc,bcc) f.fun_scope in
       add_children f_entry (params@vars),(acc,bcc)
-        
+
     let definition_to_entry (acc,bcc) id t =
       match t with
       | GlobalVariable g -> let e,acc = global_variable_to_entry acc id g in
@@ -453,19 +453,19 @@ let diab_file_loc sec (f,l)  =
   Diab_file_loc (Hashtbl.find filenum (sec,f),l)
 
 let prod_name =
-  let version_string =  
+  let version_string =
     if Version.buildnr <> "" && Version.tag <> "" then
       Printf.sprintf "%s, Build: %s, Tag: %s" Version.version Version.buildnr Version.tag
     else
       Version.version in
-  Printf.sprintf "AbsInt Angewandte Informatik GmbH:CompCert Version %s:(%s,%s,%s,%s)" 
+  Printf.sprintf "AbsInt Angewandte Informatik GmbH:CompCert Version %s:(%s,%s,%s,%s)"
     version_string Configuration.arch Configuration.system Configuration.abi Configuration.model
 
 let diab_gen_compilation_section s defs acc =
   let module Gen = Dwarfgenaux(struct
     let file_loc = diab_file_loc s
     let string_entry s =  Simple_string s end) in
-  let defs,(ty,locs) = List.fold_left (fun (acc,bcc) (id,t) -> 
+  let defs,(ty,locs) = List.fold_left (fun (acc,bcc) (id,t) ->
     let t,bcc = Gen.definition_to_entry  bcc id t in
     t::acc,bcc) ([],(IntSet.empty,[])) defs in
   let low_pc = Hashtbl.find compilation_section_start s
@@ -487,7 +487,7 @@ let diab_gen_compilation_section s defs acc =
     entry = cp;
     locs = Some low_pc,locs;
   }::acc
- 
+
 let gen_diab_debug_info sec_name var_section : debug_entries =
   let defs = Hashtbl.fold (fun id t acc ->
     let s = match t with
@@ -513,15 +513,15 @@ let gnu_string_entry s =
       let id = next_id () in
       Hashtbl.add string_table s id;
       Offset_string id
-        
+
 let gen_gnu_debug_info sec_name var_section : debug_entries =
   let low_pc = Hashtbl.find compilation_section_start ".text"
   and high_pc = Hashtbl.find compilation_section_end ".text" in
-  let module Gen = Dwarfgenaux (struct 
+  let module Gen = Dwarfgenaux (struct
     let file_loc = gnu_file_loc
     let string_entry = gnu_string_entry
   end) in
-  let defs,(ty,locs),sec = Hashtbl.fold (fun  id t (acc,bcc,sec) -> 
+  let defs,(ty,locs),sec = Hashtbl.fold (fun  id t (acc,bcc,sec) ->
     let s = match t with
     | GlobalVariable _ -> var_section
     | Function f -> sec_name (get_opt_val f.fun_atom) in
diff --git a/doc/coq2html.mll b/doc/coq2html.mll
index 2f1bfdbc..7dd93842 100644
--- a/doc/coq2html.mll
+++ b/doc/coq2html.mll
@@ -157,7 +157,7 @@ let rec set_enum_depth d =
     fprintf !oc "<ul>\n";
     fprintf !oc "<li>\n";
     incr enum_depth;
-  end 
+  end
   else if !enum_depth > d then begin
     fprintf !oc "</li>\n";
     fprintf !oc "</ul>\n";
@@ -290,7 +290,7 @@ rule coq_bol = parse
   | eof
       { () }
   | space* as s
-      { space s; 
+      { space s;
         coq lexbuf }
 
 and skip_newline = parse
@@ -337,7 +337,7 @@ and comment = parse
   | "*)"
       { if !in_proof then end_comment() }
   | "(*"
-      { if !in_proof then start_comment(); 
+      { if !in_proof then start_comment();
         comment lexbuf; comment lexbuf }
   | eof
       { () }
@@ -345,7 +345,7 @@ and comment = parse
       { if !in_proof then newline();
         comment lexbuf }
   | space* as s
-      { if !in_proof then space s; 
+      { if !in_proof then space s;
         comment lexbuf }
   | eof
       { () }
@@ -422,7 +422,7 @@ let process_file f =
   if Filename.check_suffix f ".v" then begin
     let pref_f = Filename.chop_suffix f ".v" in
     let base_f = Filename.basename pref_f in
-    current_module := 
+    current_module :=
       "compcert." ^ Str.global_replace (Str.regexp "/") "." pref_f;
     let ic = open_in f in
     if !output_name = "-" then
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index d9c21a9c..9d3697bd 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -52,7 +52,7 @@ let option_S = ref false
 let option_c = ref false
 let option_v = ref false
 let option_interp = ref false
-let option_small_data = 
+let option_small_data =
   ref (if Configuration.arch = "powerpc"
        && Configuration.abi = "eabi"
        && Configuration.system = "diab"
diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index 41325368..1f05afd8 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -30,7 +30,7 @@ let ini_file_name =
     try
       List.find  Sys.file_exists files
     with Not_found ->
-      begin 
+      begin
         eprintf "Cannot find compcert.ini configuration file.\n";
         exit 2
       end
@@ -73,19 +73,19 @@ let get_config_list key =
 let prepro = get_config_list "prepro"
 let asm = get_config_list "asm"
 let linker = get_config_list "linker"
-let arch = 
+let arch =
   match get_config_string "arch" with
   | "powerpc"|"arm"|"ia32" as a -> a
   | v -> bad_config "arch" [v]
 let model = get_config_string "model"
 let abi = get_config_string "abi"
 let system = get_config_string "system"
-let has_runtime_lib = 
+let has_runtime_lib =
   match get_config_string "has_runtime_lib" with
   | "true" -> true
   | "false" -> false
   | v -> bad_config "has_runtime_lib" [v]
-let has_standard_headers = 
+let has_standard_headers =
   match get_config_string "has_standard_headers" with
   | "true" -> true
   | "false" -> false
@@ -95,7 +95,7 @@ let stdlib_path =
     get_config_string "stdlib_path"
   else
     ""
-let asm_supports_cfi = 
+let asm_supports_cfi =
   match get_config_string "asm_supports_cfi" with
   | "true" -> true
   | "false" -> false
@@ -117,7 +117,7 @@ type struct_return_style =
   | SR_int1248      (* return by content if size is 1, 2, 4 or 8 bytes *)
   | SR_int1to4      (* return by content if size is <= 4 *)
   | SR_int1to8      (* return by content if size is <= 8 *)
-  | SR_ref          (* always return by assignment to a reference 
+  | SR_ref          (* always return by assignment to a reference
                        given as extra argument *)
 
 let struct_passing_style =
diff --git a/driver/Configuration.mli b/driver/Configuration.mli
index f82ce213..1d048ac4 100644
--- a/driver/Configuration.mli
+++ b/driver/Configuration.mli
@@ -46,7 +46,7 @@ type struct_return_style =
   | SR_int1248      (* return by content if size is 1, 2, 4 or 8 bytes *)
   | SR_int1to4      (* return by content if size is <= 4 *)
   | SR_int1to8      (* return by content if size is <= 8 *)
-  | SR_ref          (* always return by assignment to a reference 
+  | SR_ref          (* always return by assignment to a reference
                        given as extra argument *)
 
 val struct_passing_style: struct_passing_style
diff --git a/driver/Driver.ml b/driver/Driver.ml
index c7d9984e..4b58fb4d 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -188,7 +188,7 @@ let compile_c_ast sourcename csyntax ofile debug =
     | Errors.Error msg ->
         eprintf "%s: %a" sourcename print_error msg;
         exit 2 in
-  (* Dump Asm in binary and JSON format *)  
+  (* Dump Asm in binary and JSON format *)
   if !option_sdump then
     begin
       dump_asm asm (output_filename sourcename ".c" ".sdump");
@@ -518,7 +518,7 @@ let unset_all opts = List.iter (fun r -> r := false) opts
 let num_source_files = ref 0
 
 let num_input_files = ref 0
-    
+
 let cmdline_actions =
   let f_opt name ref =
     [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in
@@ -570,8 +570,8 @@ let cmdline_actions =
 (* Linking options *)
   Prefix "-l", Self push_linker_arg;
   Prefix "-L", Self push_linker_arg;
-  Exact "-T", String (fun s -> if Configuration.system = "diab" then 
-    push_linker_arg ("-Wm"^s) 
+  Exact "-T", String (fun s -> if Configuration.system = "diab" then
+    push_linker_arg ("-Wm"^s)
   else begin
       push_linker_arg ("-T");
       push_linker_arg(s)
diff --git a/driver/Interp.ml b/driver/Interp.ml
index f453af95..b3bdc883 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -98,7 +98,7 @@ let name_of_function prog fn =
   in find_name prog.prog_defs
 
 let invert_local_variable e b =
-  Maps.PTree.fold 
+  Maps.PTree.fold
     (fun res id (b', _) -> if b = b' then Some id else res)
     e None
 
@@ -176,7 +176,7 @@ let rec compare_cont k1 k2 =
   match k1, k2 with
   | Kstop, Kstop -> 0
   | Kdo k1, Kdo k2 -> compare_cont k1 k2
-  | Kseq(s1, k1), Kseq(s2, k2) ->  
+  | Kseq(s1, k1), Kseq(s2, k2) ->
       let c = compare s1 s2 in if c <> 0 then c else compare_cont k1 k2
   | Kifthenelse(s1, s1', k1), Kifthenelse(s2, s2', k2) ->
       let c = compare (s1,s1') (s2,s2') in
@@ -273,7 +273,7 @@ let extract_string m blk ofs =
         if c = '\000' then begin
           Some(Buffer.contents b)
         end else begin
-          Buffer.add_char b c; 
+          Buffer.add_char b c;
           extract blk (Z.succ ofs)
         end
     | _ ->
@@ -325,7 +325,7 @@ let format_value m flags length conv arg =
   | 'p', "", _ ->
       "<int or pointer argument expected>"
   | _, _, _ ->
-      "<unrecognized format>"      
+      "<unrecognized format>"
 
 let do_printf m fmt args =
 
@@ -374,7 +374,7 @@ let convert_external_arg ge v t =
   | Vfloat f, AST.Tfloat -> Some (EVfloat f)
   | Vsingle f, AST.Tsingle -> Some (EVsingle f)
   | Vlong n, AST.Tlong -> Some (EVlong n)
-  | Vptr(b, ofs), AST.Tint -> 
+  | Vptr(b, ofs), AST.Tint ->
       Senv.invert_symbol ge b >>= fun id -> Some (EVptr_global(id, ofs))
   | _, _ -> None
 
@@ -565,7 +565,7 @@ let rec explore_all p prog ge time states =
     if nextstates <> [] then explore_all p prog ge (time + 1) nextstates
 
 (* The variant of the source program used to build the world for
-   executing events.  
+   executing events.
    Volatile variables are turned into non-volatile ones, so that
      reads and writes can be performed.
    Other variables are turned into empty vars, so that
diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml
index a1dba2d9..7b75f6be 100644
--- a/exportclight/Clightgen.ml
+++ b/exportclight/Clightgen.ml
@@ -75,7 +75,7 @@ let print_error oc msg =
 let output_filename ?(final = false) source_file source_suffix output_suffix =
   match !option_o with
   | Some file when final -> file
-  | _ -> 
+  | _ ->
     Filename.basename (Filename.chop_suffix source_file source_suffix)
     ^ output_suffix
 
@@ -253,7 +253,7 @@ let cmdline_actions =
   Exact "-dparse", Set option_dparse;
   Exact "-dc", Set option_dcmedium;
   Exact "-dclight", Set option_dclight;
-(* General options *) 
+(* General options *)
   Exact "-v", Set option_v;
   Exact "-stdlib", String(fun s -> stdlib_path := s);
   ]
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index 82066cc9..115a761e 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -234,9 +234,9 @@ let name_of_chunk = function
   | Many64 -> "Many64"
 
 let signatur p sg =
-  fprintf p "@[<hov 2>(mksignature@ %a@ %a@ %a)@]" 
+  fprintf p "@[<hov 2>(mksignature@ %a@ %a@ %a)@]"
      (print_list asttype) sg.sig_args
-     (print_option asttype) sg.sig_res 
+     (print_option asttype) sg.sig_res
      callconv sg.sig_cc
 
 let assertions = ref ([]: (ident * typ list) list)
@@ -254,13 +254,13 @@ let external_function p = function
   | EF_free -> fprintf p "EF_free"
   | EF_memcpy(sz, al) ->
       fprintf p "(EF_memcpy %ld %ld)" (Z.to_int32 sz) (Z.to_int32 al)
-  | EF_annot(text, targs) -> 
+  | EF_annot(text, targs) ->
       assertions := (text, targs) :: !assertions;
       fprintf p "(EF_annot %ld%%positive %a)" (P.to_int32 text) (print_list asttype) targs
   | EF_annot_val(text, targ) ->
       assertions := (text, [targ]) :: !assertions;
       fprintf p "(EF_annot_val %ld%%positive %a)" (P.to_int32 text) asttype targ
-  | EF_debug(kind, text, targs) -> 
+  | EF_debug(kind, text, targs) ->
       fprintf p "(EF_debug %ld%%positive %ld%%positive %a)" (P.to_int32 kind) (P.to_int32 text) (print_list asttype) targs
   | EF_inline_asm(text, sg, clob) ->
       fprintf p "@[<hov 2>(EF_inline_asm %ld%%positive@ %a@ %a)@]"
@@ -340,7 +340,7 @@ let rec stmt p = function
         (print_option ident) optid expr e1 (print_list expr) el
   | Sbuiltin(optid, ef, tyl, el) ->
       fprintf p "@[<hov 2>(Sbuiltin %a@ %a@ %a@ %a)@]"
-        (print_option ident) optid 
+        (print_option ident) optid
         external_function ef
         typlist tyl
         (print_list expr) el
@@ -414,7 +414,7 @@ let print_globdef p (id, gd) =
   | Gvar v -> print_variable p (id, v)
 
 let print_ident_globdef p = function
-  | (id, Gfun(Internal f)) -> 
+  | (id, Gfun(Internal f)) ->
       fprintf p "(%a, Gfun(Internal f_%s))" ident id (extern_atom id)
   | (id, Gfun(External(ef, targs, tres, cc))) ->
       fprintf p "@[<hov 2>(%a,@ @[<hov 2>Gfun(External %a@ %a@ %a@ %a))@]@]"
diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml
index 4f02e633..871599d1 100644
--- a/ia32/Asmexpand.ml
+++ b/ia32/Asmexpand.ml
@@ -21,7 +21,7 @@ open AST
 open Camlcoq
 open Datatypes
 open Integers
-       
+
 exception Error of string
 
 (* Useful constants and helper functions *)
@@ -35,14 +35,14 @@ let _8 = coqint_of_camlint 8l
 let stack_alignment () =
   if Configuration.system = "macoxs" then 16
   else 8
-	 
+
 (* SP adjustment to allocate or free a stack frame *)
-			   
+
 let int32_align n a =
   if n >= 0l
   then Int32.logand (Int32.add n (Int32.of_int (a-1))) (Int32.of_int (-a))
   else Int32.logand n (Int32.of_int (-a))
-		    
+
 let sp_adjustment sz =
   let sz = camlint_of_coqint sz in
   (* Preserve proper alignment of the stack *)
@@ -50,9 +50,9 @@ let sp_adjustment sz =
   (* The top 4 bytes have already been allocated by the "call" instruction. *)
   let sz = Int32.sub sz 4l in
   sz
-			   
-			   
-(* Built-ins.  They come in two flavors: 
+
+
+(* Built-ins.  They come in two flavors:
    - annotation statements: take their arguments in registers or stack
    locations; generate no code;
    - inlined by the compiler: take their arguments in arbitrary
@@ -88,7 +88,7 @@ let offset_addressing (Addrmode(base, ofs, cst)) delta =
 
 let linear_addr reg ofs = Addrmode(Some reg, None, Coq_inl ofs)
 let global_addr id ofs = Addrmode(None, None, Coq_inr(id, ofs))
-			   
+
 (* Handling of memcpy *)
 
 (* Unaligned memory accesses are quite fast on IA32, so use large
@@ -128,7 +128,7 @@ let expand_builtin_memcpy sz al args =
   if sz <= 32
   then expand_builtin_memcpy_small sz al src dst
   else expand_builtin_memcpy_big sz al src dst
- 	   
+
 (* Handling of volatile reads and writes *)
 
 let expand_builtin_vload_common chunk addr res =
@@ -197,9 +197,9 @@ let expand_builtin_vstore chunk args =
      expand_builtin_vstore_common chunk addr src
        (if Asmgen.addressing_mentions addr EAX then ECX else EAX)
   | _ -> assert false
-		 
+
 (* Handling of varargs *)
-		 
+
 let expand_builtin_va_start r =
   if not !current_function.fn_sig.sig_cc.cc_vararg then
     invalid_arg "Fatal error: va_start used in non-vararg function";
@@ -231,7 +231,7 @@ let expand_fma args res i132 i213 i231 =
       end
   | _ ->
      invalid_arg ("ill-formed fma builtin")
-	   
+
 (* Handling of compiler-inlined builtins *)
 
 let expand_builtin_inline name args res =
@@ -348,7 +348,7 @@ let expand_builtin_inline name args res =
      raise (Error ("unrecognized builtin " ^ name))
 
 (* Expansion of instructions *)
-       
+
 let expand_instruction instr =
   match instr with
   | Pallocframe (sz, ofs_ra, ofs_link) ->
@@ -379,14 +379,14 @@ let expand_instruction instr =
 	    (Int32.to_int (camlint_of_coqint al))
             args
        | EF_annot_val(txt, targ) ->
-          expand_annot_val txt targ args res      
+          expand_annot_val txt targ args res
        | EF_annot _ | EF_debug _ | EF_inline_asm _ ->
           emit instr
        | _ ->
           assert false
      end
   | _ -> emit instr
-       
+
 let int_reg_to_dwarf = function
   | EAX -> 0
   | EBX -> 3
diff --git a/ia32/CBuiltins.ml b/ia32/CBuiltins.ml
index b1be612b..125e71d5 100644
--- a/ia32/CBuiltins.ml
+++ b/ia32/CBuiltins.ml
@@ -41,19 +41,19 @@ let builtins = {
     "__builtin_fmin",
       (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);
     "__builtin_fmadd",
-      (TFloat(FDouble, []), 
+      (TFloat(FDouble, []),
        [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
        false);
     "__builtin_fmsub",
-      (TFloat(FDouble, []), 
+      (TFloat(FDouble, []),
        [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
        false);
     "__builtin_fnmadd",
-      (TFloat(FDouble, []), 
+      (TFloat(FDouble, []),
        [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
        false);
     "__builtin_fnmsub",
-      (TFloat(FDouble, []), 
+      (TFloat(FDouble, []),
        [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
        false);
     (* Memory accesses *)
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index 32e55ec1..1ccfdcba 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -83,13 +83,13 @@ module Cygwin_System : SYSTEM =
 
     let raw_symbol oc s =
        fprintf oc "_%s" s
-        
+
     let symbol oc symb =
       raw_symbol oc (extern_atom symb)
 
     let label oc lbl =
        fprintf oc "L%d" lbl
-        
+
     let name_of_section = function
       | Section_text -> ".text"
       | Section_data i | Section_small_data i ->
@@ -106,18 +106,18 @@ module Cygwin_System : SYSTEM =
       | Section_debug_loc ->  ".section	.debug_loc,\"dr\""
       | Section_debug_line _ -> ".section	.debug_line,\"dr\""
       | Section_debug_abbrev -> ".section	.debug_abbrev,\"dr\""
-      | Section_debug_str-> assert false (* Should not be used *) 
-    
+      | Section_debug_str-> assert false (* Should not be used *)
+
     let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *)
 
     let print_align oc n =
       fprintf oc "	.align	%d\n" n
-    
-    let print_mov_ra oc rd id =   
+
+    let print_mov_ra oc rd id =
       fprintf oc "	movl	$%a, %a\n" symbol id ireg rd
 
     let print_fun_info _ _  = ()
-        
+
     let print_var_info _ _ = ()
 
     let print_epilogue _ = ()
@@ -134,10 +134,10 @@ module Cygwin_System : SYSTEM =
 (* Printer functions for ELF *)
 module ELF_System : SYSTEM =
   struct
-    
+
     let raw_symbol oc s =
       fprintf oc "%s" s
-  
+
     let symbol = elf_symbol
 
     let label = elf_label
@@ -159,19 +159,19 @@ module ELF_System : SYSTEM =
       | Section_debug_line _ -> ".section	.debug_line,\"\",@progbits"
       | Section_debug_abbrev -> ".section	.debug_abbrev,\"\",@progbits"
       | Section_debug_str -> ".section	.debug_str,\"MS\",@progbits,1"
-            
+
     let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *)
-                    
+
     let print_align oc n =
       fprintf oc "	.align	%d\n" n
-        
-    let print_mov_ra  oc rd id = 
+
+    let print_mov_ra  oc rd id =
          fprintf oc "	movl	$%a, %a\n" symbol id ireg rd
 
     let print_fun_info = elf_print_fun_info
-      
+
     let print_var_info = elf_print_var_info
-      
+
     let print_epilogue _ = ()
 
     let print_comm_decl oc name sz al =
@@ -186,7 +186,7 @@ module ELF_System : SYSTEM =
 (* Printer functions for MacOS *)
 module MacOS_System : SYSTEM =
   struct
-    
+
     let raw_symbol oc s =
      fprintf oc "_%s" s
 
@@ -214,30 +214,30 @@ module MacOS_System : SYSTEM =
       | Section_debug_line _ -> ".section	__DWARF,__debug_line,regular,debug"
       | Section_debug_str -> ".section	__DWARF,__debug_str,regular,debug"
       | Section_debug_abbrev -> ".section	__DWARF,__debug_abbrev,regular,debug" (* Dummy value *)
-    
-    
+
+
     let stack_alignment =  16 (* mandatory *)
-         
-    (* Base-2 log of a Caml integer *)           
+
+    (* Base-2 log of a Caml integer *)
     let rec log2 n =
       assert (n > 0);
       if n = 1 then 0 else 1 + log2 (n lsr 1)
 
     let print_align oc n =
       fprintf oc "	.align	%d\n" (log2 n)
-        
+
     let indirect_symbols : StringSet.t ref = ref StringSet.empty
 
-    let print_mov_ra oc rd id = 
+    let print_mov_ra oc rd id =
       let id = extern_atom id in
       indirect_symbols := StringSet.add id !indirect_symbols;
       fprintf oc "	movl	L%a$non_lazy_ptr, %a\n" raw_symbol id ireg rd
 
     let print_fun_info _ _ = ()
- 
+
     let print_var_info _ _ = ()
-    
-    let print_epilogue oc = 
+
+    let print_epilogue oc =
       fprintf oc "	.section __IMPORT,__pointers,non_lazy_symbol_pointers\n";
       StringSet.iter
         (fun s ->
@@ -275,7 +275,7 @@ module Target(System: SYSTEM):TARGET =
       | Coq_inl n ->
           let n = camlint_of_coqint n in
           fprintf oc "%ld" n
-      | Coq_inr(id, ofs) -> 
+      | Coq_inr(id, ofs) ->
           let ofs = camlint_of_coqint ofs in
           if ofs = 0l
           then symbol oc id
@@ -292,13 +292,13 @@ module Target(System: SYSTEM):TARGET =
       | Cond_e -> "e" | Cond_ne -> "ne"
       | Cond_b -> "b" | Cond_be -> "be" | Cond_ae -> "ae" | Cond_a -> "a"
       | Cond_l -> "l" | Cond_le -> "le" | Cond_ge -> "ge" | Cond_g -> "g"
-      | Cond_p -> "p" | Cond_np -> "np" 
+      | Cond_p -> "p" | Cond_np -> "np"
 
     let name_of_neg_condition = function
       | Cond_e -> "ne" | Cond_ne -> "e"
       | Cond_b -> "ae" | Cond_be -> "a" | Cond_ae -> "b" | Cond_a -> "be"
       | Cond_l -> "ge" | Cond_le -> "g" | Cond_ge -> "l" | Cond_g -> "le"
-      | Cond_p -> "np" | Cond_np -> "p" 
+      | Cond_p -> "np" | Cond_np -> "p"
 
 
 (* Names of sections *)
@@ -342,7 +342,7 @@ module Target(System: SYSTEM):TARGET =
 
 (* Built-in functions *)
 
-(* Built-ins.  They come in two flavors: 
+(* Built-ins.  They come in two flavors:
    - annotation statements: take their arguments in registers or stack
    locations; generate no code;
    - inlined by the compiler: take their arguments in arbitrary
@@ -652,7 +652,7 @@ module Target(System: SYSTEM):TARGET =
       (** Pseudo-instructions *)
       | Plabel(l) ->
           fprintf oc "%a:\n" label (transl_label l)
-      | Pallocframe(sz, ofs_ra, ofs_link) 
+      | Pallocframe(sz, ofs_ra, ofs_link)
       | Pfreeframe(sz, ofs_ra, ofs_link) ->
 	 assert false
       | Pbuiltin(ef, args, res) ->
@@ -670,13 +670,13 @@ module Target(System: SYSTEM):TARGET =
           | _ ->
               assert false
           end
-            
+
     let print_literal64 oc (lbl, n) =
       fprintf oc "%a:	.quad	0x%Lx\n" label lbl n
     let print_literal32 oc (lbl, n) =
       fprintf oc "%a:	.long	0x%lx\n" label lbl n
-        
-    let print_jumptable oc jmptbl = 
+
+    let print_jumptable oc jmptbl =
       let print_jumptable oc (lbl, tbl) =
         fprintf oc "%a:" label lbl;
         List.iter
@@ -688,7 +688,7 @@ module Target(System: SYSTEM):TARGET =
         List.iter (print_jumptable oc) !jumptables;
         jumptables := []
       end
-          
+
     let print_init oc = function
       | Init_int8 n ->
           fprintf oc "	.byte	%ld\n" (camlint_of_coqint n)
@@ -710,7 +710,7 @@ module Target(System: SYSTEM):TARGET =
           if Z.gt n Z.zero then
             fprintf oc "	.space	%s\n" (Z.to_string n)
       | Init_addrof(symb, ofs) ->
-          fprintf oc "	.long	%a\n" 
+          fprintf oc "	.long	%a\n"
             symbol_offset (symb, camlint_of_coqint ofs)
 
     let print_align = print_align
@@ -741,7 +741,7 @@ module Target(System: SYSTEM):TARGET =
 
     let print_optional_fun_info _ = ()
 
-    let get_section_names name = 
+    let get_section_names name =
       match C2C.atom_sections name with
       | [t;l;j] -> (t, l, j)
       |    _    -> (Section_text, Section_literal, Section_jumptable)
@@ -749,10 +749,10 @@ module Target(System: SYSTEM):TARGET =
     let reset_constants = reset_constants
 
     let print_fun_info = print_fun_info
-        
+
     let print_var_info = print_var_info
 
-    let print_prologue oc = 
+    let print_prologue oc =
       need_masks := false;
       if !Clflags.option_g then begin
         section oc Section_text;
@@ -762,7 +762,7 @@ module Target(System: SYSTEM):TARGET =
         fprintf oc "	.cfi_sections	.debug_frame\n"
       end
 
-    let print_epilogue oc = 
+    let print_epilogue oc =
       if !need_masks then begin
         section oc (Section_const true);
         (* not Section_literal because not 8-bytes *)
@@ -784,13 +784,13 @@ module Target(System: SYSTEM):TARGET =
         section oc Section_text;
         fprintf oc "%a:\n" elf_label high_pc
       end
-      
+
     let comment = comment
 
     let default_falignment = 16
 
     let label = label
-       
+
     let new_label = new_label
 
 end
@@ -798,7 +798,7 @@ end
 let sel_target () =
  let module S = (val (match Configuration.system with
   | "macosx" -> (module MacOS_System:SYSTEM)
-  | "linux" 
+  | "linux"
   | "bsd" -> (module ELF_System:SYSTEM)
   | "cygwin" -> (module Cygwin_System:SYSTEM)
   | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported")  ):SYSTEM) in
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index c50b3230..c5fb2e55 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -86,7 +86,7 @@ module P = struct
       if n = 0l
       then assert false
       else Coq_xO (of_int32 (Int32.shift_right_logical n 1))
-    else 
+    else
       if n = 1l
       then Coq_xH
       else Coq_xI (of_int32 (Int32.shift_right_logical n 1))
@@ -101,7 +101,7 @@ module P = struct
       if n = 0L
       then assert false
       else Coq_xO (of_int64 (Int64.shift_right_logical n 1))
-    else 
+    else
       if n = 1L
       then Coq_xH
       else Coq_xI (of_int64 (Int64.shift_right_logical n 1))
@@ -295,7 +295,7 @@ let intern_string s =
     next_atom := Pos.succ !next_atom;
     Hashtbl.add atom_of_string s a;
     Hashtbl.add string_of_atom a s;
-    a 
+    a
 let extern_atom a =
   try
     Hashtbl.find string_of_atom a
diff --git a/lib/Readconfig.mll b/lib/Readconfig.mll
index 27ef32cf..ec2f6bb0 100644
--- a/lib/Readconfig.mll
+++ b/lib/Readconfig.mll
@@ -28,7 +28,7 @@ let error msg lexbuf =
                        lexbuf.lex_curr_p.pos_lnum,
                        msg)))
 
-let ill_formed_line lexbuf = error "Ill-formed line" lexbuf 
+let ill_formed_line lexbuf = error "Ill-formed line" lexbuf
 let unterminated_quote lexbuf = error "Unterminated quote" lexbuf
 let lone_backslash lexbuf = error "Lone \\ (backslash) at end of file" lexbuf
 
@@ -41,7 +41,7 @@ let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_' '.']*
 rule begline = parse
   | '#' [^ '\n']* ('\n' | eof)
       { Lexing.new_line lexbuf; begline lexbuf }
-  | whitespace* (ident as key) whitespace* '=' 
+  | whitespace* (ident as key) whitespace* '='
       { let words = unquoted false [] lexbuf in
         Hashtbl.add key_val_tbl key (List.rev words);
         begline lexbuf }
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index 7c52bb40..bc99be7a 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -106,17 +106,17 @@ let p_z oc z = fprintf oc "%s" (Z.to_string z)
 let p_int_constant oc i = fprintf oc "{\"Integer\":%a}" p_int i
 let p_float64_constant oc f = fprintf oc "{\"Float\":%a}" p_float64 f
 let p_float32_constant oc f = fprintf oc "{\"Float\":%a}" p_float32 f
-let p_z_constant oc z = fprintf oc "{\"Integer\":%s}" (Z.to_string z) 
+let p_z_constant oc z = fprintf oc "{\"Integer\":%s}" (Z.to_string z)
 
 let p_constant oc  = function
   | Cint i ->  p_int_constant oc i
   | Csymbol_low (i,c) -> fprintf oc "{\"Symbol_low\":{\"Name\":%a,\"Offset\":%a}}" p_atom i p_int c
-  | Csymbol_high (i,c) -> fprintf oc "{\"Symbol_high\":{\"Name\":%a,\"Offset\":%a}}" p_atom i p_int c 
-  | Csymbol_sda (i,c) -> fprintf oc "{\"Symbol_sda\":{\"Name\":%a,\"Offset\":%a}}" p_atom i p_int c 
-  | Csymbol_rel_low (i,c) -> fprintf oc "{\"Symbol_rel_low\":{\"Name\":%a,\"Offset\":%a}}" p_atom i p_int c 
-  | Csymbol_rel_high (i,c) -> fprintf oc "{\"Symbol_rel_high\":{\"Name\":%a,\"Offset\":%a}}" p_atom i p_int c 
+  | Csymbol_high (i,c) -> fprintf oc "{\"Symbol_high\":{\"Name\":%a,\"Offset\":%a}}" p_atom i p_int c
+  | Csymbol_sda (i,c) -> fprintf oc "{\"Symbol_sda\":{\"Name\":%a,\"Offset\":%a}}" p_atom i p_int c
+  | Csymbol_rel_low (i,c) -> fprintf oc "{\"Symbol_rel_low\":{\"Name\":%a,\"Offset\":%a}}" p_atom i p_int c
+  | Csymbol_rel_high (i,c) -> fprintf oc "{\"Symbol_rel_high\":{\"Name\":%a,\"Offset\":%a}}" p_atom i p_int c
 
-let p_crbit oc c = 
+let p_crbit oc c =
   let number = match c with
   | CRbit_0 -> 0
   | CRbit_1 -> 1
@@ -160,7 +160,7 @@ let p_instruction oc ic =
   | Pb l -> fprintf oc "{\"Instruction Name\":\"Pb\",\"Args\":[%a]}" p_label l
   | Pbctr s -> fprintf oc  "{\"Instruction Name\":\"Pbctr\",\"Args\":[]}"
   | Pbctrl s -> fprintf oc "{\"Instruction Name\":\"Pbctrl\",\"Args\":[]}"
-  | Pbdnz l -> fprintf oc "{\"Instruction Name\":\"Pbdnz\",\"Args\":[%a]}" p_label l 
+  | Pbdnz l -> fprintf oc "{\"Instruction Name\":\"Pbdnz\",\"Args\":[%a]}" p_label l
   | Pbf (c,l) -> fprintf oc "{\"Instruction Name\":\"Pbf\",\"Args\":[%a,%a]}" p_crbit c p_label l
   | Pbl (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbl\",\"Args\":[%a]}"  p_atom_constant i
   | Pbs (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbs\",\"Args\":[%a]}"  p_atom_constant i
@@ -171,7 +171,7 @@ let p_instruction oc ic =
   | Pcmplw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcmplw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
   | Pcmplwi (ir,c) -> fprintf oc "{\"Instruction Name\":\"Pcmplwi\",\"Args\":[%a,%a]}" p_ireg ir p_constant c
   | Pcmpw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcmpw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
-  | Pcmpwi (ir,c) -> fprintf oc "{\"Instruction Name\":\"Pcmpwi\",\"Args\":[%a,%a]}" p_ireg ir p_constant c 
+  | Pcmpwi (ir,c) -> fprintf oc "{\"Instruction Name\":\"Pcmpwi\",\"Args\":[%a,%a]}" p_ireg ir p_constant c
   | Pcntlzw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcntlzw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
   | Pcreqv (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcreqv\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3
   | Pcror (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcror\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3
@@ -190,7 +190,7 @@ let p_instruction oc ic =
   | Pextsh (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pextsh\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
   | Pextsw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pextsw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
   | Pfreeframe (c,i) -> assert false (* Should not occur *)
-  | Pfabs (fr1,fr2) 
+  | Pfabs (fr1,fr2)
   | Pfabss (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfabs\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2
   | Pfadd (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfadd\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3
   | Pfadds (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfadds\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3
@@ -246,7 +246,7 @@ let p_instruction oc ic =
   | Plwz (ir1,ic,ir2) -> fprintf oc "{\"Instruction Name\":\"Plwz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant ic p_ireg ir2
   | Plwz_a (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plwz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2
   | Plwzu (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plwzu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2
-  | Plwzx (ir1,ir2,ir3) 
+  | Plwzx (ir1,ir2,ir3)
   | Plwzx_a (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwzx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Plwarx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwarx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Plwbrx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwbrx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
@@ -339,7 +339,7 @@ let p_section oc = function
   | Section_jumptable -> fprintf oc "{\"Section Name\":\"Jumptable\"}"
   | Section_user (s,w,e) -> fprintf oc "{\"Section Name\":\"%s\",\"Writable\":%B,\"Executable\":%B}" s w e
   | Section_debug_info _
-  | Section_debug_abbrev 
+  | Section_debug_abbrev
   | Section_debug_line _
   | Section_debug_loc
   | Section_debug_str -> () (* There should be no info in the debug sections *)
@@ -349,17 +349,17 @@ let p_int_opt oc = function
   | Some i -> fprintf oc "%d" i
 
 
-let p_fundef oc (name,f) = 
+let p_fundef oc (name,f) =
   let alignment = atom_alignof name
   and inline = atom_is_inline name
   and static = atom_is_static name
   and instr = List.filter (function Pbuiltin _| Pcfi_adjust _ | Pcfi_rel_offset _ -> false | _ -> true) f.fn_code in
   let c_section,l_section,j_section = match (atom_sections name) with [a;b;c] -> a,b,c | _ -> assert false in
   fprintf oc "{\"Fun Name\":%a,\n\"Fun Storage Class\":%a,\n\"Fun Alignment\":%a,\n\"Fun Section Code\":%a,\"Fun Section Literals\":%a,\"Fun Section Jumptable\":%a,\n\"Fun Inline\":%B,\n\"Fun Code\":%a}\n"
-    p_atom name  p_storage static p_int_opt alignment  
+    p_atom name  p_storage static p_int_opt alignment
     p_section c_section p_section l_section p_section j_section inline
     (p_list p_instruction) instr
- 
+
 let p_init_data oc = function
   | Init_int8 ic -> fprintf oc "{\"Init_int8\":%a}" p_int ic
   | Init_int16 ic -> fprintf oc "{\"Init_int16\":%a}" p_int ic
@@ -372,10 +372,10 @@ let p_init_data oc = function
 
 let p_vardef oc (name,v) =
   let alignment = atom_alignof name
-  and static = atom_is_static name 
+  and static = atom_is_static name
   and section = match  (atom_sections name) with [s] -> s | _ -> assert false (* Should only have one section *) in
   fprintf oc "{\"Var Name\":%a,\"Var Readonly\":%B,\"Var Volatile\":%B,\n\"Var Storage Class\":%a,\n\"Var Alignment\":%a,\n\"Var Section\":%a,\n\"Var Init\":%a}\n"
-    p_atom name v.gvar_readonly v.gvar_volatile 
+    p_atom name v.gvar_readonly v.gvar_volatile
     p_storage static p_int_opt alignment p_section section
     (p_list p_init_data) v.gvar_init
 
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index a9e4f5e3..106ba4d0 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -19,7 +19,7 @@ open C
 
 let builtins = {
   Builtins.typedefs = [
-    "__builtin_va_list", 
+    "__builtin_va_list",
     TArray(TInt(IUInt, []), Some 3L, [])
   ];
   Builtins.functions = [
@@ -40,19 +40,19 @@ let builtins = {
       (TInt (IUInt, []),  [TInt(IUInt, []);TInt(IUInt, [])], false);
     (* Float arithmetic *)
     "__builtin_fmadd",
-      (TFloat(FDouble, []), 
+      (TFloat(FDouble, []),
        [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
        false);
     "__builtin_fmsub",
-      (TFloat(FDouble, []), 
+      (TFloat(FDouble, []),
        [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
        false);
     "__builtin_fnmadd",
-      (TFloat(FDouble, []), 
+      (TFloat(FDouble, []),
        [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
        false);
     "__builtin_fnmsub",
-      (TFloat(FDouble, []), 
+      (TFloat(FDouble, []),
        [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
        false);
     "__builtin_fsqrt",
@@ -62,7 +62,7 @@ let builtins = {
     "__builtin_fres",
       (TFloat(FFloat, []), [TFloat(FFloat, [])], false);
     "__builtin_fsel",
-      (TFloat(FDouble, []), 
+      (TFloat(FDouble, []),
        [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
        false);
     "__builtin_fcti",
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index a596e587..10d89d54 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -103,15 +103,15 @@ module Linux_System : SYSTEM =
 
     let freg oc r =
       output_string oc (float_reg_name r)
-        
-    let creg oc r = 
+
+    let creg oc r =
       fprintf oc "%d" r
- 
+
     let name_of_section = function
       | Section_text -> ".text"
       | Section_data i ->
           if i then ".data" else "COMM"
-      | Section_small_data i -> 
+      | Section_small_data i ->
           if i then ".section	.sdata,\"aw\",@progbits" else "COMM"
       | Section_const i ->
           if i then ".rodata" else "COMM"
@@ -138,17 +138,17 @@ module Linux_System : SYSTEM =
 
     let print_file_line oc file line =
       print_file_line oc comment file line
-    
-    (* Emit .cfi directives *)      
+
+    (* Emit .cfi directives *)
     let cfi_startproc = cfi_startproc
 
     let cfi_endproc = cfi_endproc
-              
+
     let cfi_adjust = cfi_adjust
-              
+
     let cfi_rel_offset = cfi_rel_offset
 
-    let print_prologue oc = 
+    let print_prologue oc =
       if !Clflags.option_g then  begin
           section oc Section_text;
           let low_pc = new_label () in
@@ -169,7 +169,7 @@ module Linux_System : SYSTEM =
 
     let debug_section _ _ = ()
   end
-    
+
 module Diab_System : SYSTEM =
   struct
 
@@ -189,7 +189,7 @@ module Diab_System : SYSTEM =
           symbol_fragment oc s n "@sdax@l"
       | Csymbol_rel_high(s, n) ->
           symbol_fragment oc s n "@sdarx@ha"
- 
+
     let ireg oc r =
       output_char oc 'r';
       output_string oc (int_reg_name r)
@@ -197,10 +197,10 @@ module Diab_System : SYSTEM =
     let freg oc r =
       output_char oc 'f';
       output_string oc (float_reg_name r)
-        
+
     let creg oc r =
       fprintf oc "cr%d" r
-        
+
     let name_of_section = function
       | Section_text -> ".text"
       | Section_data i -> if i then ".data" else "COMM"
@@ -254,20 +254,20 @@ module Diab_System : SYSTEM =
 
     let debug_section oc sec =
       match sec with
-      | Section_debug_abbrev 
+      | Section_debug_abbrev
       | Section_debug_info _
       | Section_debug_loc -> ()
       | sec ->
           let name = match sec with
           | Section_user (name,_,_) -> name
           | _ -> name_of_section sec in
-          if not (Debug.exists_section name) then 
+          if not (Debug.exists_section name) then
             let line_start = new_label ()
             and low_pc = new_label ()
             and debug_info = new_label () in
             Debug.add_diab_info name (line_start,debug_info,name_of_section sec);
             Debug.add_compilation_section_start name low_pc;
-            let line_name = ".debug_line" ^(if name <> ".text" then name else "") in 
+            let line_name = ".debug_line" ^(if name <> ".text" then name else "") in
             section oc (Section_debug_line (if name <> ".text" then Some name else None));
             fprintf oc "	.section	%s,,n\n" line_name;
             if name <> ".text" then
@@ -279,18 +279,18 @@ module Diab_System : SYSTEM =
             fprintf oc "	.d2_line_start	%s\n" line_name
           else
             ()
-        
+
     let print_prologue oc =
       fprintf oc "	.xopt	align-fill-text=0x60000000\n";
       debug_section oc Section_text
 
     let print_epilogue oc =
-      let end_label sec = 
+      let end_label sec =
         fprintf oc "\n";
         fprintf oc "	%s\n" sec;
         let label_end = new_label () in
         fprintf oc "%a:\n" label label_end;
-        label_end 
+        label_end
       and entry_label f =
         let label = new_label () in
         fprintf oc ".L%d:	.d2filenum \"%s\"\n" label f;
@@ -306,7 +306,7 @@ module Target (System : SYSTEM):TARGET =
 
     (* Basic printing functions *)
     let symbol = symbol
-        
+
     let raw_symbol oc s =
       fprintf oc "%s" s
 
@@ -371,7 +371,7 @@ module Target (System : SYSTEM):TARGET =
     let short_cond_branch tbl pc lbl_dest =
       match PTree.get lbl_dest tbl with
       | None -> assert false
-      | Some pc_dest -> 
+      | Some pc_dest ->
           let disp = pc_dest - pc in -0x2000 <= disp && disp < 0x2000
 
     (* Printing of instructions *)
@@ -551,11 +551,11 @@ module Target (System : SYSTEM):TARGET =
       | Pfnmsub(r1, r2, r3, r4) ->
           fprintf oc "	fnmsub	%a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4
       | Pfsqrt(r1, r2) ->
-          fprintf oc "	fsqrt	%a, %a\n" freg r1 freg r2    
+          fprintf oc "	fsqrt	%a, %a\n" freg r1 freg r2
       | Pfrsqrte(r1, r2) ->
-          fprintf oc "	frsqrte	%a, %a\n" freg r1 freg r2    
+          fprintf oc "	frsqrte	%a, %a\n" freg r1 freg r2
       | Pfres(r1, r2) ->
-          fprintf oc "	fres	%a, %a\n" freg r1 freg r2    
+          fprintf oc "	fres	%a, %a\n" freg r1 freg r2
       | Pfsel(r1, r2, r3, r4) ->
           fprintf oc "	fsel	%a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4
       | Pisel (r1,r2,r3,cr) ->
@@ -793,7 +793,7 @@ module Target (System : SYSTEM):TARGET =
       let nlo = Int64.to_int32 n
       and nhi = Int64.to_int32(Int64.shift_right_logical n 32) in
       fprintf oc "%a:	.long	0x%lx, 0x%lx\n" label lbl nhi nlo
-        
+
     let print_literal32 oc (lbl, n) =
       fprintf oc "%a:	.long	0x%lx\n" label lbl n
 
@@ -823,10 +823,10 @@ module Target (System : SYSTEM):TARGET =
           if Z.gt n Z.zero then
             fprintf oc "	.space	%s\n" (Z.to_string n)
       | Init_addrof(symb, ofs) ->
-          fprintf oc "	.long	%a\n" 
+          fprintf oc "	.long	%a\n"
             symbol_offset (symb, ofs)
 
-  
+
     let print_fun_info = elf_print_fun_info
 
     let emit_constants oc lit =
@@ -840,26 +840,26 @@ module Target (System : SYSTEM):TARGET =
 
     let print_optional_fun_info _ = ()
 
-    let get_section_names name = 
+    let get_section_names name =
       match C2C.atom_sections name with
       | [t;l;j] -> (t, l, j)
       |    _    -> (Section_text, Section_literal, Section_jumptable)
-            
+
     let reset_constants = reset_constants
- 
+
     let print_var_info = elf_print_var_info
 
-    let print_comm_symb oc sz name align = 
+    let print_comm_symb oc sz name align =
       fprintf oc "	%s	%a, %s, %d\n"
         (if C2C.atom_is_static name then ".lcomm" else ".comm")
         symbol name
         (Z.to_string sz)
         align
-    
+
     let print_align oc align  =
       fprintf oc "	.balign	%d\n" align
 
-    let print_jumptable oc jmptbl = 
+    let print_jumptable oc jmptbl =
       let print_jumptable oc (lbl, tbl) =
         fprintf oc "%a:" label lbl;
         List.iter
@@ -874,7 +874,7 @@ module Target (System : SYSTEM):TARGET =
 
     let default_falignment = 4
 
-    let new_label = new_label            
+    let new_label = new_label
 
     let section oc sec =
       section oc sec;
@@ -882,7 +882,7 @@ module Target (System : SYSTEM):TARGET =
   end
 
 let sel_target () =
-  let module S  = (val 
+  let module S  = (val
     (match Configuration.system with
     | "linux"  -> (module Linux_System:SYSTEM)
     | "diab"   -> (module Diab_System:SYSTEM)
diff --git a/tools/ndfun.ml b/tools/ndfun.ml
index 4ee07e54..2b8bcb19 100644
--- a/tools/ndfun.ml
+++ b/tools/ndfun.ml
@@ -33,7 +33,7 @@ let oneline s =
 let re_trim_1 = Str.regexp "^[ \t]+\\|[ \t]+$"
 let re_trim_2 = Str.regexp "  +"
 
-let trim s = 
+let trim s =
   Str.global_replace re_trim_2 " " (Str.global_replace re_trim_1 "" s)
 
 (* A nicer interface to Str.match_string, with automatic trimming *)
@@ -70,7 +70,7 @@ let re_arg = Str.regexp "\\([a-z][a-z0-9_]*\\)"
 
 let match_args args =
   let n = ref 0 in
-  let subst s = 
+  let subst s =
     incr n; sprintf "%s as zz%d" (Str.matched_group 1 s) !n in
   Str.global_substitute re_arg subst args
 
@@ -78,7 +78,7 @@ let match_args args =
 
 let match_temps args =
   let n = ref 0 in
-  let subst s = 
+  let subst s =
     incr n; sprintf "zz%d" !n in
   Str.global_substitute re_arg subst (remove_commas args)