aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--debug/CtoDwarf.ml49
-rw-r--r--debug/DwarfPrinter.ml12
-rw-r--r--debug/DwarfTypes.mli1
-rw-r--r--driver/Configuration.ml21
-rw-r--r--driver/Driver.ml35
5 files changed, 66 insertions, 52 deletions
diff --git a/debug/CtoDwarf.ml b/debug/CtoDwarf.ml
index 99b77e6f..c5f1142c 100644
--- a/debug/CtoDwarf.ml
+++ b/debug/CtoDwarf.ml
@@ -188,29 +188,33 @@ and fun_to_dwarf_tag rt args =
s.id,((s::others)@et)
(* Generate a dwarf tag for the given array type *)
-and array_to_dwarf_tag child size =
+and array_to_dwarf_tag child size =
+ let append_opt a b =
+ match a with
+ | None -> b
+ | Some a -> a::b in
let size_to_subrange s =
- let b = (match s with
+ match s with
| None -> None
| Some i ->
- let i = Int64.to_int i in
- Some (BoundConst i)) in
- let s = {
- subrange_type = None;
- subrange_upper_bound = b;
- } in
- new_entry (DW_TAG_subrange_type s) in
+ let i = Int64.to_int (Int64.sub i Int64.one) in
+ let s =
+ {
+ subrange_type = None;
+ subrange_upper_bound = Some (BoundConst i);
+ } in
+ Some (new_entry (DW_TAG_subrange_type s)) in
let rec aux t =
(match t with
| TArray (child,size,_) ->
let sub = size_to_subrange size in
let t,c,e = aux child in
- t,sub::c,e
+ t,append_opt sub c,e
| _ -> let t,e = type_to_dwarf t in
t,[],e) in
let t,children,e = aux child in
let sub = size_to_subrange size in
- let children = List.rev (sub::children) in
+ let children = List.rev (append_opt sub children) in
let arr = {
array_type_file_loc = None;
array_type = t;
@@ -272,23 +276,30 @@ and attr_type_to_dwarf typ typ_string =
(* Translate a given type to its dwarf representation *)
and type_to_dwarf (typ: typ): int * dw_entry list =
- let typ = strip_attributes typ in
- let typ_string = typ_to_string typ in
- try
- Hashtbl.find type_table typ_string,[]
- with Not_found ->
- attr_type_to_dwarf typ typ_string
+ match typ with
+ | TStruct (i,_)
+ | TUnion (i,_)
+ | TEnum (i,_) ->
+ let t = get_composite_type i.stamp in
+ t,[]
+ | _ ->
+ let typ = strip_attributes typ in
+ let typ_string = typ_to_string typ in
+ try
+ Hashtbl.find type_table typ_string,[]
+ with Not_found ->
+ attr_type_to_dwarf typ typ_string
(* Translate a typedef to its corresponding dwarf representation *)
let typedef_to_dwarf gloc (name,t) =
let i,t = type_to_dwarf t in
- Hashtbl.add typedef_table name i;
let td = {
typedef_file_loc = gloc;
typedef_name = name;
typedef_type = i;
} in
let td = new_entry (DW_TAG_typedef td) in
+ Hashtbl.add typedef_table name td.id;
td::t
(* Translate a global var to its corresponding dwarf representation *)
@@ -304,7 +315,7 @@ let glob_var_to_dwarf (s,n,t,_) gloc =
variable_file_loc = (Some gloc);
variable_declaration = Some at_decl;
variable_external = Some ext;
- variable_location = if ext then Some (LocSymbol n.name) else None;
+ variable_location = None;
variable_name = n.name;
variable_segment = None;
variable_type = i;
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index 70b68634..7f1caaf6 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -74,7 +74,6 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
| None -> ()
| Some (LocConst _) -> add_abbr_entry (0x2,location_const_type_abbr) buf
| Some (LocBlock _) -> add_abbr_entry (0x2,location_block_type_abbr) buf
- | Some (LocSymbol _) -> add_abbr_entry (0x2,location_block_type_abbr) buf
(* Dwarf entity to string function *)
let abbrev_string_of_entity entity has_sibling =
@@ -125,7 +124,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
add_abbr_entry (0x1c,value_type_abbr) buf;
add_name buf
| DW_TAG_formal_parameter e ->
- prologue 0x34;
+ prologue 0x5;
add_attr_some e.formal_parameter_file_loc add_file_loc;
add_attr_some e.formal_parameter_artificial (add_abbr_entry (0x34,artificial_type_abbr));
add_location e.formal_parameter_location buf;
@@ -295,12 +294,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
fprintf oc " .byte 0x%X\n" b
let print_loc oc loc =
- match loc with
- | LocSymbol s ->
- fprintf oc " .sleb128 5\n";
- fprintf oc " .byte 3\n";
- fprintf oc " .4byte %s\n" s
- | _ -> ()
+ ()
let print_data_location oc dl =
()
@@ -341,8 +335,8 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
let print_compilation_unit oc tag =
let prod_name = sprintf "AbsInt Angewandte Informatik GmbH:CompCert Version %s:%s" Version.version Configuration.arch in
print_string oc (Sys.getcwd ());
- print_addr oc (get_start_addr ());
print_addr oc (get_end_addr ());
+ print_addr oc (get_start_addr ());
print_uleb128 oc 1;
print_string oc tag.compile_unit_name;
print_string oc prod_name;
diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli
index 4852e550..d6592bd9 100644
--- a/debug/DwarfTypes.mli
+++ b/debug/DwarfTypes.mli
@@ -37,7 +37,6 @@ type address = int
type block = string
type location_value =
- | LocSymbol of string
| LocConst of constant
| LocBlock of block
diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index 64f24820..41325368 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -20,17 +20,20 @@ let ini_file_name =
Sys.getenv "COMPCERT_CONFIG"
with Not_found ->
let exe_dir = Filename.dirname Sys.executable_name in
- let exe_ini = Filename.concat exe_dir "compcert.ini" in
let share_dir =
Filename.concat (Filename.concat exe_dir Filename.parent_dir_name)
- "share" in
- let share_ini = Filename.concat share_dir "compcert.ini" in
- if Sys.file_exists exe_ini then exe_ini
- else if Sys.file_exists share_ini then share_ini
- else begin
- eprintf "Cannot find compcert.ini configuration file.\n";
- exit 2
- end
+ "share" in
+ let share_compcert_dir =
+ Filename.concat share_dir "compcert" in
+ let search_path = [exe_dir;share_dir;share_compcert_dir] in
+ let files = List.map (fun s -> Filename.concat s "compcert.ini") search_path in
+ try
+ List.find Sys.file_exists files
+ with Not_found ->
+ begin
+ eprintf "Cannot find compcert.ini configuration file.\n";
+ exit 2
+ end
(* Read in the .ini file *)
diff --git a/driver/Driver.ml b/driver/Driver.ml
index b19ba5cc..f53de821 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -185,7 +185,7 @@ let compile_c_ast sourcename csyntax ofile debug =
| Errors.OK asm ->
asm
| Errors.Error msg ->
- print_error stderr msg;
+ eprintf "%s: %a" sourcename print_error msg;
exit 2 in
(* Dump Asm in binary and JSON format *)
if !option_sdump then
@@ -223,7 +223,7 @@ let compile_cminor_file ifile ofile =
(CMtypecheck.type_program
(CMparser.prog CMlexer.token lb)) with
| Errors.Error msg ->
- print_error stderr msg;
+ eprintf "%s: %a" ifile print_error msg;
exit 2
| Errors.OK p ->
let oc = open_out ofile in
@@ -516,6 +516,8 @@ 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
@@ -568,7 +570,7 @@ let cmdline_actions =
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)
+ push_linker_arg ("-Wm"^s)
else
push_linker_arg ("-T "^s));
Prefix "-Wl,", Self push_linker_arg;
@@ -638,25 +640,25 @@ let cmdline_actions =
eprintf "Unknown option `%s'\n" s; exit 2);
(* File arguments *)
Suffix ".c", Self (fun s ->
- push_action process_c_file s; incr num_source_files);
+ push_action process_c_file s; incr num_source_files; incr num_input_files);
Suffix ".i", Self (fun s ->
- push_action process_i_file s; incr num_source_files);
+ push_action process_i_file s; incr num_source_files; incr num_input_files);
Suffix ".p", Self (fun s ->
- push_action process_i_file s; incr num_source_files);
+ push_action process_i_file s; incr num_source_files; incr num_input_files);
Suffix ".cm", Self (fun s ->
- push_action process_cminor_file s; incr num_source_files);
+ push_action process_cminor_file s; incr num_source_files; incr num_input_files);
Suffix ".s", Self (fun s ->
- push_action process_s_file s; incr num_source_files);
+ push_action process_s_file s; incr num_source_files; incr num_input_files);
Suffix ".S", Self (fun s ->
- push_action process_S_file s; incr num_source_files);
- Suffix ".o", Self push_linker_arg;
- Suffix ".a", Self push_linker_arg;
+ push_action process_S_file s; incr num_source_files; incr num_input_files);
+ Suffix ".o", Self (fun s -> push_linker_arg s; incr num_input_files);
+ Suffix ".a", Self (fun s -> push_linker_arg s; incr num_input_files);
(* GCC compatibility: .o.ext files and .so files are also object files *)
- _Regexp ".*\\.o\\.", Self push_linker_arg;
- Suffix ".so", Self push_linker_arg;
+ _Regexp ".*\\.o\\.", Self (fun s -> push_linker_arg s; incr num_input_files);
+ Suffix ".so", Self (fun s -> push_linker_arg s; incr num_input_files);
(* GCC compatibility: .h files can be preprocessed with -E *)
Suffix ".h", Self (fun s ->
- push_action process_h_file s; incr num_source_files);
+ push_action process_h_file s; incr num_source_files; incr num_input_files);
]
let _ =
@@ -685,6 +687,11 @@ let _ =
eprintf "Ambiguous '-o' option (multiple source files)\n";
exit 2
end;
+ if !num_input_files = 0 then
+ begin
+ eprintf "ccomp: error: no input file\n";
+ exit 2
+ end;
let linker_args = time "Total compilation time" perform_actions () in
if (not nolink) && linker_args <> [] then begin
linker (output_filename_default "a.out") linker_args
generated by cgit (git 2.34.1) at 2024-07-10 07:30:29 +0000