diff options
-rw-r--r-- | backend/PrintAsm.ml | 12 | ||||
-rw-r--r-- | cfrontend/C2C.ml | 11 | ||||
-rw-r--r-- | cparser/Bitfields.ml | 1 | ||||
-rw-r--r-- | cparser/Cutil.ml | 21 | ||||
-rw-r--r-- | cparser/Cutil.mli | 2 | ||||
-rw-r--r-- | cparser/Elab.ml | 28 | ||||
-rw-r--r-- | cparser/Parse.ml | 13 | ||||
-rw-r--r-- | cparser/Parse.mli | 2 | ||||
-rw-r--r-- | debug/Debug.ml | 38 | ||||
-rw-r--r-- | debug/Debug.mli | 8 | ||||
-rw-r--r-- | debug/DebugInformation.ml | 35 | ||||
-rw-r--r-- | debug/DwarfPrinter.ml | 4 | ||||
-rw-r--r-- | debug/DwarfTypes.mli | 1 | ||||
-rw-r--r-- | driver/Driver.ml | 9 | ||||
-rw-r--r-- | lib/Camlcoq.ml | 10 |
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 |