Merge remote-tracking branch 'origin/master' into parser_fix

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);