aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backend/PrintAsm.ml12
-rw-r--r--cfrontend/C2C.ml11
-rw-r--r--cparser/Bitfields.ml1
-rw-r--r--cparser/Cutil.ml21
-rw-r--r--cparser/Cutil.mli2
-rw-r--r--cparser/Elab.ml28
-rw-r--r--cparser/Parse.ml13
-rw-r--r--cparser/Parse.mli2
-rw-r--r--debug/Debug.ml38
-rw-r--r--debug/Debug.mli8
-rw-r--r--debug/DebugInformation.ml35
-rw-r--r--debug/DwarfPrinter.ml4
-rw-r--r--debug/DwarfTypes.mli1
-rw-r--r--driver/Driver.ml9
-rw-r--r--lib/Camlcoq.ml10
15 files changed, 120 insertions, 75 deletions
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index 29409b32..ea3d985a 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -27,11 +27,10 @@ module Printer(Target:TARGET) =
let addr_mapping: (string, (int * int)) Hashtbl.t = Hashtbl.create 7
let get_fun_addr name =
- let name = extern_atom name in
- let start_addr = new_label ()
- and end_addr = new_label () in
- Hashtbl.add addr_mapping name (start_addr,end_addr);
- start_addr,end_addr
+ let s = new_label ()
+ and e = new_label () in
+ Debug.add_fun_addr name (s,e);
+ s,e
let print_debug_label oc l =
if !Clflags.option_g && Configuration.advanced_debug then
@@ -120,8 +119,7 @@ module Printer(Target:TARGET) =
let get_stmt_list_addr = Target.get_stmt_list_addr
let name_of_section = Target.name_of_section
let get_fun_addr s = try Some (Hashtbl.find addr_mapping s) with Not_found -> None
- let get_location a = try (Target.get_location (stamp_atom a)) with Not_found -> None
- let get_segment_location a = try (Target.get_segment_location (stamp_atom a)) with Not_found -> None
+ let get_location a = None
let get_frame_base a = None
let symbol = Target.symbol
end
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 1a6abb6e..e31da76b 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -524,6 +524,11 @@ let convertField env f =
(intern_string f.fld_name, convertTyp env f.fld_typ)
let convertCompositedef env su id attr members =
+ let t = match su with C.Struct ->
+ let layout = Cutil.struct_layout env members in
+ List.iter (fun (a,b) -> Debug.set_member_offset id a b) layout;
+ TStruct (id,attr) | C.Union -> TUnion (id,attr) in
+ Debug.set_composite_size id su (Cutil.sizeof env t);
Composite(intern_string id.name,
begin match su with C.Struct -> Struct | C.Union -> Union end,
List.map (convertField env) members,
@@ -1039,7 +1044,6 @@ let convertFundef loc env fd =
List.map
(fun (id, ty) ->
let id' = intern_string id.name in
- add_stamp id.stamp id';
(id', convertTyp env ty))
fd.fd_params in
let vars =
@@ -1050,7 +1054,6 @@ let convertFundef loc env fd =
if init <> None then
unsupported "initialized local variable";
let id' = intern_string id.name in
- add_stamp id.stamp id';
(id', convertTyp env ty))
fd.fd_locals in
let body' = convertStmt loc env fd.fd_body in
@@ -1079,7 +1082,7 @@ let convertFundecl env (sto, id, ty, optinit) =
| Tfunction(args, res, cconv) -> (args, res, cconv)
| _ -> assert false in
let id' = intern_string id.name in
- add_stamp id.stamp id';
+ Debug.atom_function id id';
let sg = signature_of_type args res cconv in
let ef =
if id.name = "malloc" then EF_malloc else
@@ -1121,7 +1124,7 @@ let convertInitializer env ty i =
let convertGlobvar loc env (sto, id, ty, optinit) =
let id' = intern_string id.name in
- add_stamp id.stamp id';
+ Debug.atom_global_variable id id';
let ty' = convertTyp env ty in
let sz = Ctypes.sizeof !comp_env ty' in
let al = Ctypes.alignof !comp_env ty' in
diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
index 6569bb4c..8d43e689 100644
--- a/cparser/Bitfields.ml
+++ b/cparser/Bitfields.ml
@@ -134,6 +134,7 @@ let rec transf_members env id count = function
if !config.bitfields_msb_first
then sizeof_ikind carrier_ikind * 8 - pos - sz
else pos in
+ Debug.set_bitfield_offset id name pos' carrier (sizeof_ikind carrier_ikind);
Hashtbl.add bitfield_table
(id, name)
{bf_carrier = carrier; bf_carrier_typ = carrier_typ;
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index a3c05c34..90bbfe5a 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -427,7 +427,6 @@ let sizeof_union env members =
We lay out fields consecutively, inserting padding to preserve
their alignment.
Not done here but in composite_info_decl: rounding size to alignment. *)
-
let sizeof_struct env members =
let rec sizeof_rec ofs = function
| [] ->
@@ -449,6 +448,26 @@ let sizeof_struct env members =
end
in sizeof_rec 0 members
+(* Simplified version to compute offsets on structs without bitfields *)
+let struct_layout env members =
+ let rec struct_layout_rec mem ofs = function
+ | [] ->
+ mem
+ | [ { fld_typ = TArray(_, None, _) } as m ] ->
+ (* C99: ty[] allowed as last field *)
+ begin match alignof env m.fld_typ with
+ | Some a -> ( m.fld_name,align ofs a)::mem
+ | None -> []
+ end
+ | m :: rem ->
+ match alignof env m.fld_typ, sizeof env m.fld_typ with
+ | Some a, Some s ->
+ let offset = align ofs a in
+ struct_layout_rec ((m.fld_name,offset)::mem) (offset + s) rem
+ | _, _ -> []
+ in struct_layout_rec [] 0 members
+
+
(* Determine whether a type is incomplete *)
let incomplete_type env t =
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index b1f77944..b9879339 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -105,6 +105,8 @@ val composite_info_decl:
Env.t -> struct_or_union -> attributes -> Env.composite_info
val composite_info_def:
Env.t -> struct_or_union -> attributes -> field list -> Env.composite_info
+val struct_layout:
+ Env.t -> field list -> (string * int) list
(* Type classification functions *)
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index de24871f..ca5865dd 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -56,9 +56,11 @@ let elab_loc l = (l.filename, l.lineno)
let top_declarations = ref ([] : globdecl list)
-let emit_elab loc td =
+let emit_elab env loc td =
let loc = elab_loc loc in
- top_declarations := { gdesc = td; gloc = loc } :: !top_declarations
+ let dec ={ gdesc = td; gloc = loc } in
+ Debug.insert_global_declaration env dec;
+ top_declarations := dec :: !top_declarations
let reset() = top_declarations := []
@@ -730,7 +732,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env =
(* finishing the definition of an incomplete struct or union *)
let (ci', env') = elab_struct_or_union_info kind loc env members attrs in
(* Emit a global definition for it *)
- emit_elab loc (Gcompositedef(kind, tag', attrs, ci'.ci_members));
+ emit_elab env' loc (Gcompositedef(kind, tag', attrs, ci'.ci_members));
(* Replace infos but keep same ident *)
(tag', Env.add_composite env' tag' ci')
| Some(tag', {ci_sizeof = Some _}), Some _
@@ -745,7 +747,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env =
(* enter it with a new name *)
let (tag', env') = Env.enter_composite env tag ci in
(* emit it *)
- emit_elab loc (Gcompositedecl(kind, tag', attrs));
+ emit_elab env' loc (Gcompositedecl(kind, tag', attrs));
(tag', env')
| _, Some members ->
(* definition of a complete struct or union *)
@@ -753,12 +755,12 @@ and elab_struct_or_union only kind loc tag optmembers attrs env =
(* enter it, incomplete, with a new name *)
let (tag', env') = Env.enter_composite env tag ci1 in
(* emit a declaration so that inner structs and unions can refer to it *)
- emit_elab loc (Gcompositedecl(kind, tag', attrs));
+ emit_elab env' loc (Gcompositedecl(kind, tag', attrs));
(* elaborate the members *)
let (ci2, env'') =
elab_struct_or_union_info kind loc env' members attrs in
(* emit a definition *)
- emit_elab loc (Gcompositedef(kind, tag', attrs, ci2.ci_members));
+ emit_elab env'' loc (Gcompositedef(kind, tag', attrs, ci2.ci_members));
(* Replace infos but keep same ident *)
(tag', Env.add_composite env'' tag' ci2)
@@ -809,7 +811,7 @@ and elab_enum only loc tag optmembers attrs env =
let (dcls, env') = elab_members env 0L members in
let info = { ei_members = dcls; ei_attr = attrs } in
let (tag', env'') = Env.enter_enum env' tag info in
- emit_elab loc (Genumdef(tag', attrs, dcls));
+ emit_elab env' loc (Genumdef(tag', attrs, dcls));
(tag', env'')
(* Elaboration of a naked type, e.g. in a cast *)
@@ -1312,7 +1314,7 @@ let elab_expr loc env a =
let ty = TFun(TInt(IInt, []), None, false, []) in
(* Emit an extern declaration for it *)
let id = Env.fresh_ident n in
- emit_elab loc (Gdecl(Storage_extern, id, ty, None));
+ emit_elab env loc (Gdecl(Storage_extern, id, ty, None));
{ edesc = EVar id; etyp = ty }
| _ -> elab a1 in
let bl = List.map elab al in
@@ -1789,7 +1791,7 @@ let enter_typedefs loc env sto dl =
if redef Env.lookup_ident env s then
error loc "redefinition of identifier '%s' as different kind of symbol" s;
let (id, env') = Env.enter_typedef env s ty in
- emit_elab loc (Gtypedef(id, ty));
+ emit_elab env loc (Gtypedef(id, ty));
env') env dl
let enter_or_refine_ident local loc env s sto ty =
@@ -1865,7 +1867,7 @@ let enter_decdefs local loc env sto dl =
((sto', id, ty', init') :: decls, env2)
else begin
(* Global definition *)
- emit_elab loc (Gdecl(sto', id, ty', init'));
+ emit_elab env2 loc (Gdecl(sto', id, ty', init'));
(decls, env2)
end in
let (decls, env') = List.fold_left enter_decdef ([], env) dl in
@@ -1899,7 +1901,7 @@ let elab_fundef env spec name body loc =
let (func_ty, func_init) = __func__type_and_init s in
let (func_id, _, env3,func_ty) =
enter_or_refine_ident true loc env2 "__func__" Storage_static func_ty in
- emit_elab loc (Gdecl(Storage_static, func_id, func_ty, Some func_init));
+ emit_elab env3 loc (Gdecl(Storage_static, func_id, func_ty, Some func_init));
(* Elaborate function body *)
let body' = !elab_funbody_f ty_ret env3 body in
(* Special treatment of the "main" function *)
@@ -1925,7 +1927,7 @@ let elab_fundef env spec name body loc =
fd_vararg = vararg;
fd_locals = [];
fd_body = body'' } in
- emit_elab loc (Gfundef fn);
+ emit_elab env1 loc (Gfundef fn);
env1
let elab_kr_fundef env spec name params defs body loc =
@@ -1997,7 +1999,7 @@ let rec elab_definition (local: bool) (env: Env.t) (def: Cabs.definition)
(* pragma *)
| PRAGMA(s, loc) ->
- emit_elab loc (Gpragma s);
+ emit_elab env loc (Gpragma s);
([], env)
and elab_definitions local env = function
diff --git a/cparser/Parse.ml b/cparser/Parse.ml
index c9564c08..2be3a612 100644
--- a/cparser/Parse.ml
+++ b/cparser/Parse.ml
@@ -24,12 +24,7 @@ let transform_program t p name =
(run_pass Unblock.program 'b'
(run_pass Bitfields.program 'f'
p)))) in
- let debug =
- if !Clflags.option_g && Configuration.advanced_debug then
- Some (CtoDwarf.program_to_dwarf p p1 name)
- else
- None in
- (Rename.program p1 (Filename.chop_suffix name ".c")),debug
+ (Rename.program p1 (Filename.chop_suffix name ".c"))
let parse_transformations s =
let t = ref CharSet.empty in
@@ -46,7 +41,7 @@ let parse_transformations s =
let preprocessed_file transfs name sourcefile =
Cerrors.reset();
let ic = open_in sourcefile in
- let p,d =
+ let p =
try
let t = parse_transformations transfs in
let lb = Lexer.init name ic in
@@ -65,6 +60,6 @@ let preprocessed_file transfs name sourcefile =
Timing.time2 "Emulations" transform_program t p1 name
with
| Cerrors.Abort ->
- [],None in
+ [] in
close_in ic;
- if Cerrors.check_errors() then None,None else Some p,d
+ if Cerrors.check_errors() then None else Some p
diff --git a/cparser/Parse.mli b/cparser/Parse.mli
index ac8feb70..58c3cfb9 100644
--- a/cparser/Parse.mli
+++ b/cparser/Parse.mli
@@ -15,7 +15,7 @@
(* Entry point for the library: parse, elaborate, and transform *)
-val preprocessed_file: string -> string -> string -> C.program option * DwarfTypes.dw_entry option
+val preprocessed_file: string -> string -> string -> C.program option
(* first arg: desired transformations
second arg: source file name before preprocessing
diff --git a/debug/Debug.ml b/debug/Debug.ml
index eb195b33..ab20f630 100644
--- a/debug/Debug.ml
+++ b/debug/Debug.ml
@@ -21,9 +21,11 @@ type implem =
mutable init: string -> unit;
mutable atom_function: ident -> atom -> unit;
mutable atom_global_variable: ident -> atom -> unit;
- mutable set_composite_size: ident -> struct_or_union -> int -> unit;
- mutable set_member_offset: ident -> string -> int -> int -> unit;
- mutable insert_declaration: globdecl -> Env.t -> unit;
+ mutable set_composite_size: ident -> struct_or_union -> int option -> unit;
+ mutable set_member_offset: ident -> string -> int -> unit;
+ mutable set_bitfield_offset: ident -> string -> int -> string -> int -> unit;
+ mutable insert_global_declaration: Env.t -> globdecl -> unit;
+ mutable add_fun_addr: atom -> (int * int) -> unit
}
let implem =
@@ -32,8 +34,10 @@ let implem =
atom_function = (fun _ _ -> ());
atom_global_variable = (fun _ _ -> ());
set_composite_size = (fun _ _ _ -> ());
- set_member_offset = (fun _ _ _ _ -> ());
- insert_declaration = (fun _ _ -> ());
+ set_member_offset = (fun _ _ _ -> ());
+ set_bitfield_offset = (fun _ _ _ _ _ -> ());
+ insert_global_declaration = (fun _ _ -> ());
+ add_fun_addr = (fun _ _ -> ());
}
let init () =
@@ -43,19 +47,25 @@ let init () =
implem.atom_global_variable <- DebugInformation.atom_global_variable;
implem.set_composite_size <- DebugInformation.set_composite_size;
implem.set_member_offset <- DebugInformation.set_member_offset;
- implem.insert_declaration <- DebugInformation.insert_declaration;
+ implem.set_bitfield_offset <- DebugInformation.set_bitfield_offset;
+ implem.insert_global_declaration <- DebugInformation.insert_global_declaration;
+ implem.add_fun_addr <- DebugInformation.add_fun_addr;
end else begin
- implem.init <- (fun _ -> ());
- implem.atom_function <- (fun _ _ -> ());
- implem.atom_global_variable <- (fun _ _ -> ());
- implem.set_composite_size <- (fun _ _ _ -> ());
- implem.set_member_offset <- (fun _ _ _ _ -> ());
- implem.insert_declaration <- (fun _ _ -> ())
+ implem.init <- (fun _ -> ());
+ implem.atom_function <- (fun _ _ -> ());
+ implem.atom_global_variable <- (fun _ _ -> ());
+ implem.set_composite_size <- (fun _ _ _ -> ());
+ implem.set_member_offset <- (fun _ _ _ -> ());
+ implem.set_bitfield_offset <- (fun _ _ _ _ _ -> ());
+ implem.insert_global_declaration <- (fun _ _ -> ());
+ implem.add_fun_addr <- (fun _ _ -> ())
end
let init_compile_unit name = implem.init name
let atom_function id atom = implem.atom_function id atom
let atom_global_variable id atom = implem.atom_global_variable id atom
let set_composite_size id sou size = implem.set_composite_size id sou size
-let set_member_offset id field off size = implem.set_member_offset id field off size
-let insert_declaration dec env = implem.insert_declaration dec env
+let set_member_offset id field off = implem.set_member_offset id field off
+let set_bitfield_offset id field off underlying size = implem.set_bitfield_offset id field off underlying size
+let insert_global_declaration env dec = implem.insert_global_declaration env dec
+let add_fun_addr atom addr = implem.add_fun_addr atom addr
diff --git a/debug/Debug.mli b/debug/Debug.mli
index ea72aeb4..ae32af5b 100644
--- a/debug/Debug.mli
+++ b/debug/Debug.mli
@@ -18,6 +18,8 @@ val init: unit -> unit
val init_compile_unit: string -> unit
val atom_function: ident -> atom -> unit
val atom_global_variable: ident -> atom -> unit
-val set_composite_size: ident -> struct_or_union -> int -> unit
-val set_member_offset: ident -> string -> int -> int -> unit
-val insert_declaration: globdecl -> Env.t -> unit
+val set_composite_size: ident -> struct_or_union -> int option -> unit
+val set_member_offset: ident -> string -> int -> unit
+val set_bitfield_offset: ident -> string -> int -> string -> int -> unit
+val insert_global_declaration: Env.t -> globdecl -> unit
+val add_fun_addr: atom -> (int * int) -> unit
diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml
index 30d026c7..53f73115 100644
--- a/debug/DebugInformation.ml
+++ b/debug/DebugInformation.ml
@@ -343,7 +343,9 @@ type function_information = {
fun_return_type: int option; (* Again the special case of void functions *)
fun_vararg: bool;
fun_parameter: parameter_information list;
- fun_locals: int list;
+ fun_locals: int list;
+ fun_low_pc: int option;
+ fun_high_pc: int option;
}
type definition_type =
@@ -373,6 +375,13 @@ let find_fun_stamp id =
| Function f -> id,f
| _ -> assert false
+let find_fun_atom id =
+ let id = (Hashtbl.find atom_to_definition id) in
+ let f = Hashtbl.find definitions id in
+ match f with
+ | Function f -> id,f
+ | _ -> assert false
+
let replace_var id var =
let var = GlobalVariable var in
@@ -388,7 +397,7 @@ let gen_comp_typ sou id at =
else
TUnion (id,at)
-let insert_declaration dec env =
+let insert_global_declaration env dec=
let insert d_dec stamp =
let id = next_id () in
Hashtbl.add definitions id d_dec;
@@ -441,6 +450,8 @@ let insert_declaration dec env =
fun_vararg = f.fd_vararg;
fun_parameter = params;
fun_locals = [];
+ fun_low_pc = None;
+ fun_high_pc = None;
} in
insert (Function fd) f.fd_name.stamp
| Gcompositedecl (sou,id,at) ->
@@ -481,18 +492,28 @@ let insert_declaration dec env =
{en with enum_file_loc = Some dec.gloc; enum_enumerators = enumerator;})
| Gpragma _ -> ()
-let set_member_offset str field offset byte_size =
+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 members = List.map (fun a -> if name a then
- {a with cfd_byte_offset = Some offset; cfd_byte_size = Some byte_size;}
+ {a with cfd_byte_offset = Some offset;}
else a) 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 = Some 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.map (fun a -> if name a then
+ {a with cfd_bit_offset = Some offset; cfd_bitfield = Some underlying; cfd_byte_size = Some size}
+ else
+ a) comp.ct_members in
+ {comp with ct_members = members;})
let atom_global_variable id atom =
let id,var = find_var_stamp id.stamp in
@@ -504,6 +525,10 @@ let atom_function id atom =
replace_fun id ({f with fun_atom = Some atom;});
Hashtbl.add atom_to_definition atom id
+let add_fun_addr atom (high,low) =
+ let id,f = find_fun_atom atom in
+ replace_fun id ({f with fun_high_pc = Some high; fun_low_pc = Some low;})
+
let init name =
id := 0;
file_name := name;
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index c85a9efc..09cf72eb 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -130,7 +130,6 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
add_attr_some e.formal_parameter_artificial (add_abbr_entry (0x34,artificial_type_abbr));
add_location (get_location e.formal_parameter_id) buf;
add_attr_some e.formal_parameter_name add_name;
- add_location (get_segment_location e.formal_parameter_id) buf;
add_type buf;
add_attr_some e.formal_parameter_variable_parameter (add_abbr_entry (0x4b,variable_parameter_type_abbr))
| DW_TAG_label _ ->
@@ -205,7 +204,6 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
add_attr_some e.variable_external (add_abbr_entry (0x3f,external_type_abbr));
add_location (get_location e.variable_id) buf;
add_name buf;
- add_location (get_segment_location e.variable_id) buf;
add_type buf
| DW_TAG_volatile_type _ ->
prologue 0x35;
@@ -367,7 +365,6 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
print_opt_value oc fp.formal_parameter_artificial print_flag;
print_opt_value oc (get_location fp.formal_parameter_id) print_loc;
print_opt_value oc fp.formal_parameter_name print_string;
- print_opt_value oc (get_segment_location fp.formal_parameter_id) print_loc;
print_ref oc fp.formal_parameter_type;
print_opt_value oc fp.formal_parameter_variable_parameter print_flag
@@ -441,7 +438,6 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
print_opt_value oc var.variable_external print_flag;
print_opt_value oc (get_location var.variable_id) print_loc;
print_string oc var.variable_name;
- print_opt_value oc (get_segment_location var.variable_id) print_loc;
print_ref oc var.variable_type
let print_volatile_type oc vt =
diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli
index 174f2403..b852d1f4 100644
--- a/debug/DwarfTypes.mli
+++ b/debug/DwarfTypes.mli
@@ -270,7 +270,6 @@ module type DWARF_TARGET=
val name_of_section: section_name -> string
val get_fun_addr: string -> (int * int) option
val get_location: int -> location_value option
- val get_segment_location: int -> location_value option
val get_frame_base: int -> location_value option
val symbol: out_channel -> atom -> unit
end
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 04acf902..47d6e81c 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -108,6 +108,7 @@ let preprocess ifile ofile =
(* From preprocessed C to Csyntax *)
let parse_c_file sourcename ifile =
+ Debug.init_compile_unit sourcename;
Sections.initialize();
(* Simplification options *)
let simplifs =
@@ -117,10 +118,10 @@ let parse_c_file sourcename ifile =
^ (if !option_fpacked_structs then "p" else "")
in
(* Parsing and production of a simplified C AST *)
- let ast,debug =
+ let ast =
match Parse.preprocessed_file simplifs sourcename ifile with
- | None,_ -> exit 2
- | Some p,d -> p,d in
+ | None -> exit 2
+ | Some p -> p in
(* Save C AST if requested *)
if !option_dparse then begin
let ofile = output_filename sourcename ".c" ".parsed.c" in
@@ -141,7 +142,7 @@ let parse_c_file sourcename ifile =
PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax;
close_out oc
end;
- csyntax,debug
+ csyntax,None
(* Dump Asm code in binary format for the validator *)
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index 5eb52e88..c50b3230 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -284,7 +284,6 @@ let coqint_of_camlint64 : int64 -> Integers.Int64.int = Z.of_uint64
type atom = positive
let atom_of_string = (Hashtbl.create 17 : (string, atom) Hashtbl.t)
-let atom_of_stamp = (Hashtbl.create 17: (int, atom) Hashtbl.t)
let string_of_atom = (Hashtbl.create 17 : (atom, string) Hashtbl.t)
let next_atom = ref Coq_xH
@@ -296,14 +295,7 @@ let intern_string s =
next_atom := Pos.succ !next_atom;
Hashtbl.add atom_of_string s a;
Hashtbl.add string_of_atom a s;
- a
-
-let add_stamp s a =
- Hashtbl.add atom_of_stamp s a
-
-let stamp_atom s =
- Hashtbl.find atom_of_stamp s
-
+ a
let extern_atom a =
try
Hashtbl.find string_of_atom a
generated by cgit (git 2.34.1) at 2024-06-02 18:10:34 +0000