diff options
-rw-r--r-- | cfrontend/C2C.ml | 8 | ||||
-rw-r--r-- | cfrontend/PrintCsyntax.ml | 3 | ||||
-rw-r--r-- | cparser/Cutil.ml | 16 | ||||
-rw-r--r-- | cparser/Cutil.mli | 2 | ||||
-rw-r--r-- | cparser/ErrorReports.ml | 10 | ||||
-rw-r--r-- | debug/Debug.ml | 2 | ||||
-rw-r--r-- | debug/Debug.mli | 2 | ||||
-rw-r--r-- | debug/DebugInformation.ml | 14 | ||||
-rw-r--r-- | debug/DebugTypes.mli | 2 | ||||
-rw-r--r-- | debug/DwarfPrinter.ml | 6 | ||||
-rw-r--r-- | debug/DwarfTypes.mli | 2 | ||||
-rw-r--r-- | debug/DwarfUtil.ml | 6 | ||||
-rw-r--r-- | debug/Dwarfgen.ml | 19 | ||||
-rw-r--r-- | driver/Clflags.ml | 1 | ||||
-rw-r--r-- | driver/Driver.ml | 2 |
15 files changed, 65 insertions, 30 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index a2db0915..6b3426b2 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -983,7 +983,12 @@ let rec convertStmt env s = Scontinue | C.Sswitch(e, s1) -> let (init, cases) = groupSwitch (flattenSwitch s1) in - if init.sdesc <> C.Sskip then + let rec init_debug s = + match s.sdesc with + | Sseq (a,b) -> init_debug a && init_debug b + | C.Sskip -> true + | _ -> Cutil.is_debug_stmt s in + if init.sdesc <> C.Sskip && not (init_debug init) then begin warning "ignored code at beginning of 'switch'"; contains_case init @@ -1313,4 +1318,3 @@ let convertProgram p = if Cerrors.check_errors () then None else Some p' with Env.Error msg -> error (Env.error_message msg); None - diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 4f2a8d0c..bb6576aa 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -266,6 +266,9 @@ let rec expr p (prec, e) = fprintf p "%s@[<hov 1>(%a)@]" (camlstring_of_coqstring id) exprlist (true, args) | Ebuiltin(EF_inline_asm(txt, sg, clob), _, args, _) -> extended_asm p txt None args clob + | Ebuiltin(EF_debug(kind,txt,_),_,args,_) -> + fprintf p "__builtin_debug@[<hov 1>(%d,%S%a)@]" + (P.to_int kind) (extern_atom txt) exprlist (false,args) | Ebuiltin(_, _, args, _) -> fprintf p "<unknown builtin>@[<hov 1>(%a)@]" exprlist (true, args) | Eparen(a1, tycast, ty) -> diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index a86c779f..1b0bf65d 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -880,6 +880,18 @@ let is_literal_0 e = | EConst(CInt(0L, _, _)) -> true | _ -> false +(* Check that a C statement is a debug annotation *) + +let is_debug_stmt s = + let is_debug_call = function + | (ECall ({edesc = EVar id; _},_)) -> id.name = "__builtin_debug" + | _ -> false in + match s.sdesc with + | Sdo {edesc = e;_} -> + is_debug_call e + | _ -> false + + (* Assignment compatibility check over attributes. Standard attributes ("const", "volatile", "restrict") can safely be added (to the rhs type to get the lhs type) but must not be dropped. @@ -1099,7 +1111,3 @@ let rec subst_stmt phi s = List.map subst_asm_operand inputs, clob) } - - - - diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 8b6c609b..b353cba3 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -187,6 +187,8 @@ val type_of_member : Env.t -> field -> typ (* Return the type of accessing the given field [fld]. Normally it's [fld.fld_type] but there is a special case for small unsigned bitfields. *) +val is_debug_stmt : stmt -> bool + (* Is the given statement a call to debug builtin? *) val is_literal_0 : exp -> bool (* Is the given expression the integer literal "0"? *) val is_lvalue : exp -> bool diff --git a/cparser/ErrorReports.ml b/cparser/ErrorReports.ml index 4bbf3ded..a8976e42 100644 --- a/cparser/ErrorReports.ml +++ b/cparser/ErrorReports.ml @@ -92,6 +92,14 @@ let extract text (pos1, pos2) : string = (* -------------------------------------------------------------------------- *) +(* [compress text] replaces every run of at least one whitespace character + with exactly one space character. *) + +let compress text = + Str.global_replace (Str.regexp "[ \t\n\r]+") " " text + +(* -------------------------------------------------------------------------- *) + (* [sanitize text] eliminates any special characters from the text [text]. They are (arbitrarily) replaced with a single dot character. *) @@ -182,7 +190,7 @@ let range text (e : element) : string = (* Get the underlying source text fragment. *) let fragment = extract text (pos1, pos2) in (* Sanitize it and limit its length. Enclose it in single quotes. *) - "'" ^ shorten width (sanitize fragment) ^ "'" + "'" ^ shorten width (sanitize (compress fragment)) ^ "'" (* -------------------------------------------------------------------------- *) diff --git a/debug/Debug.ml b/debug/Debug.ml index 87d04ad7..789ecb70 100644 --- a/debug/Debug.ml +++ b/debug/Debug.ml @@ -20,7 +20,7 @@ open Sections (* Interface for generating and printing debug information *) -(* Record used for stroring references to the actual implementation functions *) +(* Record used for storing references to the actual implementation functions *) type implem = { init: string -> unit; diff --git a/debug/Debug.mli b/debug/Debug.mli index 1585e7e4..614fe84b 100644 --- a/debug/Debug.mli +++ b/debug/Debug.mli @@ -18,7 +18,7 @@ open BinNums open Sections -(* Record used for stroring references to the actual implementation functions *) +(* Record used for storing references to the actual implementation functions *) type implem = { init: string -> unit; diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml index 51fbfde9..ed00ea0d 100644 --- a/debug/DebugInformation.ml +++ b/debug/DebugInformation.ml @@ -65,7 +65,7 @@ let strip_attributes typ = strip_attributes_type typ [AConst; AVolatile] (* Find the type id to an type *) let find_type (ty: typ) = - (* We are only interrested in Const and Volatile *) + (* We are only interested in Const and Volatile *) let ty = strip_attributes ty in Hashtbl.find lookup_types (typ_to_string ty) @@ -77,7 +77,7 @@ let insert_type (ty: typ) = Hashtbl.add types id d_ty; Hashtbl.add lookup_types name id; id in - (* We are only interrested in Const and Volatile *) + (* We are only interested in Const and Volatile *) let ty = strip_attributes ty in let rec typ_aux ty = try find_type ty with @@ -255,14 +255,14 @@ let replace_fun id f = (* All local variables *) let local_variables: (int, local_information) Hashtbl.t = Hashtbl.create 7 -(* Mapping from stampt to the debug id of the local variable *) +(* Mapping from stamp to the debug id of the local variable *) let stamp_to_local: (int,int) Hashtbl.t = Hashtbl.create 7 -(* Map from scope id + function id to debug id *) +(* Map from function id + scope id to debug id *) let scope_to_local: (int * int,int) Hashtbl.t = Hashtbl.create 7 -(* Map from scope id + function atom to debug id *) -let atom_to_scope: (atom * int, int) Hashtbl.t = Hashtbl.create 7 +(* Map from function atom + scope id atom to debug id *) +let atom_to_scope: (atom * int,int) Hashtbl.t = Hashtbl.create 7 let find_lvar_stamp id = let id = (Hashtbl.find stamp_to_local id) in @@ -299,7 +299,7 @@ let remove_unused id = Hashtbl.remove stamp_to_definition id.stamp with Not_found -> () -let insert_global_declaration env dec= +let insert_global_declaration env dec = add_file (fst dec.gloc); let insert d_dec stamp = let id = next_id () in diff --git a/debug/DebugTypes.mli b/debug/DebugTypes.mli index b2f19f7a..e885fc59 100644 --- a/debug/DebugTypes.mli +++ b/debug/DebugTypes.mli @@ -147,7 +147,7 @@ type local_variable_information = { lvar_atom: atom option; lvar_file_loc:location; lvar_type: int; - lvar_static: bool; (* Static variable are mapped to symbols *) + lvar_static: bool; (* Static variables are mapped to symbols *) } type scope_information = diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml index 3e85ecfc..7469c4af 100644 --- a/debug/DwarfPrinter.ml +++ b/debug/DwarfPrinter.ml @@ -623,8 +623,10 @@ module DwarfPrinter(Target: DWARF_TARGET): let name = if e.section_name <> ".text" then Some e.section_name else None in 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 + if List.exists (fun e -> match e.locs with _,[] -> false | _,_ -> true) entries then begin + section oc Section_debug_loc; + List.iter (fun e -> print_location_list oc e.locs) entries + end let print_ranges oc r = section oc Section_debug_ranges; diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli index a4c75201..2af64c0b 100644 --- a/debug/DwarfTypes.mli +++ b/debug/DwarfTypes.mli @@ -297,7 +297,7 @@ type debug_entries = | Gnu of gnu_entries (* The target specific functions for printing the debug information *) -module type DWARF_TARGET= +module type DWARF_TARGET = sig val label: out_channel -> int -> unit val section: out_channel -> section_name -> unit diff --git a/debug/DwarfUtil.ml b/debug/DwarfUtil.ml index 3e252dd2..8db80fca 100644 --- a/debug/DwarfUtil.ml +++ b/debug/DwarfUtil.ml @@ -10,7 +10,7 @@ (* *) (* *********************************************************************) -(* Utility functions for the dwarf debuging type *) +(* Utility functions for the dwarf debugging type *) open DwarfTypes @@ -22,12 +22,12 @@ let new_entry id tag = id = id; } -(* Add an entry as child to another entry *) +(* Add an entry as child to another entry *) let add_child entry child = {entry with children = child::entry.children;} -(* Add entries as children to another entry *) +(* Add entries as children to another entry *) let add_children entry children = {entry with children = entry.children@children;} diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml index 56a318fe..f62fac26 100644 --- a/debug/Dwarfgen.ml +++ b/debug/Dwarfgen.ml @@ -182,11 +182,11 @@ module Dwarfgenaux (Target: TARGET) = enumeration_name = string_entry e.enum_name; } in let enum = new_entry id (DW_TAG_enumeration_type enum) in - let child = List.map enumerator_to_entry e.enum_enumerators in - add_children enum child + let children = List.map enumerator_to_entry e.enum_enumerators in + add_children enum children let fun_type_to_entry id f = - let children = if f.fun_prototyped then + let children = if not f.fun_prototyped then let u = { unspecified_parameter_artificial = None; } in @@ -195,7 +195,7 @@ module Dwarfgenaux (Target: TARGET) = List.map (fun p -> let fp = { formal_parameter_artificial = None; - formal_parameter_name = name_opt p.param_name; + formal_parameter_name = None; formal_parameter_type = p.param_type; formal_parameter_variable_parameter = None; formal_parameter_location = None; @@ -475,9 +475,14 @@ module Dwarfgenaux (Target: TARGET) = let f_id = get_opt_val f.fun_atom in let acc = match f.fun_return_type with Some s -> acc =<< s | None -> acc in let f_entry = new_entry id (DW_TAG_subprogram f_tag) in - let params,acc = mmap (function_parameter_to_entry f_id) acc f.fun_parameter in - let vars,acc = fun_scope_to_entries f_id acc f.fun_scope in - add_children f_entry (params@vars),acc + let children,acc = + if not !Clflags.option_gglobal then + let params,acc = mmap (function_parameter_to_entry f_id) acc f.fun_parameter in + let vars,acc = fun_scope_to_entries f_id acc f.fun_scope in + params@vars,acc + else + [],acc in + add_children f_entry (children),acc let definition_to_entry acc id t = match t with diff --git a/driver/Clflags.ml b/driver/Clflags.ml index b0c24f08..1eaa5449 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -47,6 +47,7 @@ let option_dasm = ref false let option_sdump = ref false let option_g = ref false let option_gdwarf = ref 2 +let option_gglobal = ref false let option_o = ref (None: string option) let option_E = ref false let option_S = ref false diff --git a/driver/Driver.ml b/driver/Driver.ml index a0d742c2..59e3fa3b 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -435,6 +435,7 @@ Language support options (use -fno-<opt> to turn off -f<opt>) : Debugging options: -g Generate debugging information -gdwarf- (GCC only) Generate debug information in DWARF v2 or DWARF v3 + -gonly-global Generate debugging information only for globals -frename-static Rename static functions and declarations Optimization options: (use -fno-<opt> to turn off -f<opt>) -O Optimize the compiled code [on by default] @@ -547,6 +548,7 @@ let cmdline_actions = Exact "-gdwarf-3", Self (fun s -> option_g := true; option_gdwarf := 3); Exact "-frename-static", Self (fun s -> option_rename_static:= true); + Exact "-gonly-global", Self (fun s -> option_gglobal := true); (* Code generation options -- more below *) Exact "-O0", Self (fun _ -> unset_all optimization_options); Exact "-O", Self (fun _ -> set_all optimization_options); |