From 60ab550a952c3d9719b2a91ec90c9b58769f6717 Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 14 Oct 2015 15:07:48 +0200 Subject: bug 17392: remove trailing whitespace in source files --- debug/Debug.ml | 2 +- debug/Debug.mli | 2 +- debug/DebugInformation.ml | 58 ++++++++++++++++++------------------- debug/DebugTypes.mli | 6 ++-- debug/DwarfPrinter.ml | 8 ++--- debug/DwarfTypes.mli | 6 ++-- debug/Dwarfgen.ml | 74 +++++++++++++++++++++++------------------------ 7 files changed, 78 insertions(+), 78 deletions(-) (limited to 'debug') 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 -- cgit