bug 17392: remove trailing whitespace in source files

7 files changed, 78 insertions, 78 deletions

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