From 7a6bb90048db7a254e959b1e3c308bac5fe6c418 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 11 Oct 2015 17:43:59 +0200 Subject: Use Coq strings instead of idents to name external and builtin functions. The AST.ident type represents source-level identifiers as unique positive numbers. However, the mapping identifiers <-> AST.ident differs between runs of CompCert on different source files. This is problematic when we need to produce or recognize external functions and builtin functions with fixed names, for example: * in $ARCH/Machregs.v to define the register conventions for builtin functions; * in the VST program logic from Princeton to treat thread primitives specially. So far, we used AST.ident_of_string to recover the ident associated with a string. However, this function is defined in OCaml and doesn't execute within Coq. This is a problem both for VST and for future executability of CompCert within Coq. This commit replaces "ident" by "string" in the arguments of EF_external, EF_builtin, EF_inline_asm, EF_annot, and EF_annot_val. This provides stable names for externals and builtins, as needed. For inline asm and annotations, it's a matter of taste, but using strings feels more natural. EF_debug keeps using idents, since some kinds of EF_debug annotations talk about program variables. --- cfrontend/C2C.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'cfrontend/C2C.ml') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index bd281374..9b31dfdb 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -769,7 +769,7 @@ let rec convertExpr env e = | {edesc = C.EConst(CStr txt)} :: args1 -> let targs1 = convertTypArgs env [] args1 in Ebuiltin( - EF_annot(intern_string txt, typlist_of_typelist targs1), + EF_annot(coqstring_of_camlstring txt, typlist_of_typelist targs1), targs1, convertExprList env args1, convertTyp env e.etyp) | _ -> error "ill-formed __builtin_annot (first argument must be string literal)"; @@ -781,7 +781,7 @@ let rec convertExpr env e = | [ {edesc = C.EConst(CStr txt)}; arg ] -> let targ = convertTyp env (Cutil.default_argument_conversion env arg.etyp) in - Ebuiltin(EF_annot_val(intern_string txt, typ_of_type targ), + Ebuiltin(EF_annot_val(coqstring_of_camlstring txt, typ_of_type targ), Tcons(targ, Tnil), convertExprList env [arg], convertTyp env e.etyp) | _ -> @@ -822,7 +822,7 @@ let rec convertExpr env e = let sg = signature_of_type targs tres {cc_vararg = true; cc_unproto = false; cc_structret = false} in - Ebuiltin(EF_external(intern_string "printf", sg), + Ebuiltin(EF_external(coqstring_of_camlstring "printf", sg), targs, convertExprList env args, tres) | C.ECall(fn, args) -> @@ -877,7 +877,7 @@ let convertAsm loc env txt outputs inputs clobber = let e = let tinputs = convertTypArgs env [] inputs' in let toutput = convertTyp env ty_res in - Ebuiltin(EF_inline_asm(intern_string txt', + Ebuiltin(EF_inline_asm(coqstring_of_camlstring txt', signature_of_type tinputs toutput cc_default, clobber'), tinputs, @@ -1085,14 +1085,15 @@ let convertFundecl env (sto, id, ty, optinit) = | Tfunction(args, res, cconv) -> (args, res, cconv) | _ -> assert false in let id' = intern_string id.name in + let id'' = coqstring_of_camlstring id.name in let sg = signature_of_type args res cconv in let ef = if id.name = "malloc" then EF_malloc else if id.name = "free" then EF_free else if Str.string_match re_builtin id.name 0 && List.mem_assoc id.name builtins.functions - then EF_builtin(id', sg) - else EF_external(id', sg) in + then EF_builtin(id'', sg) + else EF_external(id'', sg) in (id', Gfun(External(ef, args, res, cconv))) (** Initializers *) -- cgit From 012827a7cba40f434b9fc6ce1b46dc725473eae7 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 12 Oct 2015 14:33:15 +0200 Subject: Unified function for adding the atom identifier. Instead of defining two functions for adding the mapping from atom to debug id we use one function which then sets the corresponding values. Bug 17392. --- cfrontend/C2C.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'cfrontend/C2C.ml') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index bd281374..6826804f 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1060,7 +1060,7 @@ let convertFundef loc env fd = fd.fd_locals in let body' = convertStmt env fd.fd_body in let id' = intern_string fd.fd_name.name in - Debug.atom_function fd.fd_name id'; + Debug.atom_global fd.fd_name id'; Hashtbl.add decl_atom id' { a_storage = fd.fd_storage; a_alignment = None; @@ -1126,7 +1126,7 @@ let convertInitializer env ty i = let convertGlobvar loc env (sto, id, ty, optinit) = let id' = intern_string id.name in - Debug.atom_global_variable id id'; + Debug.atom_global id id'; let ty' = convertTyp env ty in let sz = Ctypes.sizeof !comp_env ty' in let al = Ctypes.alignof !comp_env ty' in -- cgit From 60ab550a952c3d9719b2a91ec90c9b58769f6717 Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 14 Oct 2015 15:07:48 +0200 Subject: bug 17392: remove trailing whitespace in source files --- cfrontend/C2C.ml | 76 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 38 insertions(+), 38 deletions(-) (limited to 'cfrontend/C2C.ml') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 6826804f..61528185 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -141,8 +141,8 @@ let builtins_generic = { (* Block copy *) "__builtin_memcpy_aligned", (TVoid [], - [TPtr(TVoid [], []); - TPtr(TVoid [AConst], []); + [TPtr(TVoid [], []); + TPtr(TVoid [AConst], []); TInt(IUInt, []); TInt(IUInt, [])], false); @@ -357,12 +357,12 @@ let make_builtin_memcpy args = let sz1 = match Initializers.constval !comp_env sz with | Errors.OK(Vint n) -> n - | _ -> error "ill-formed __builtin_memcpy_aligned (3rd argument must be + | _ -> error "ill-formed __builtin_memcpy_aligned (3rd argument must be a constant)"; Integers.Int.zero in let al1 = match Initializers.constval !comp_env al with | Errors.OK(Vint n) -> n - | _ -> error "ill-formed __builtin_memcpy_aligned (4th argument must be + | _ -> error "ill-formed __builtin_memcpy_aligned (4th argument must be a constant)"; Integers.Int.one in (* to check: sz1 > 0, al1 divides sz1, al1 = 1|2|4|8 *) (* Issue #28: must decay array types to pointer types *) @@ -384,7 +384,7 @@ let va_list_ptr e = let make_builtin_va_arg_by_val helper ty ty_ret arg = let ty_fun = Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), ty_ret, cc_default) in - Ecast + Ecast (Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun), Econs(va_list_ptr arg, Enil), ty_ret), @@ -392,13 +392,13 @@ let make_builtin_va_arg_by_val helper ty ty_ret arg = let make_builtin_va_arg_by_ref helper ty arg = let ty_fun = - Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), + Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), Tpointer(Tvoid, noattr), cc_default) in let ty_ptr = Tpointer(ty, noattr) in let call = Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun), - Econs(va_list_ptr arg, + Econs(va_list_ptr arg, Econs(Esizeof(ty, Tint(I32, Unsigned, noattr)), Enil)), Tpointer(Tvoid, noattr)) in Evalof(Ederef(Ecast(call, ty_ptr), ty), ty) @@ -406,13 +406,13 @@ let make_builtin_va_arg_by_ref helper ty arg = let make_builtin_va_arg env ty e = match ty with | Tint _ | Tpointer _ -> - make_builtin_va_arg_by_val + make_builtin_va_arg_by_val "__compcert_va_int32" ty (Tint(I32, Unsigned, noattr)) e | Tlong _ -> - make_builtin_va_arg_by_val + make_builtin_va_arg_by_val "__compcert_va_int64" ty (Tlong(Unsigned, noattr)) e | Tfloat _ -> - make_builtin_va_arg_by_val + make_builtin_va_arg_by_val "__compcert_va_float64" ty (Tfloat(F64, noattr)) e | Tstruct _ | Tunion _ -> make_builtin_va_arg_by_ref @@ -433,7 +433,7 @@ let rec log2 n = if n = 1 then 0 else 1 + log2 (n lsr 1) let convertAttr a = { attr_volatile = List.mem AVolatile a; - attr_alignas = + attr_alignas = let n = Cutil.alignas_attribute a in if n > 0 then Some (N.of_int (log2 n)) else None } @@ -463,7 +463,7 @@ let convertFkind = function | C.FFloat -> F32 | C.FDouble -> F64 | C.FLongDouble -> - if not !Clflags.option_flongdouble then unsupported "'long double' type"; + if not !Clflags.option_flongdouble then unsupported "'long double' type"; F64 let rec convertTyp env t = @@ -524,11 +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 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) + TStruct (id,attr) | C.Union -> TUnion (id,attr) in Debug.set_composite_size id su (Cutil.sizeof env t); Composite(intern_string id.name, @@ -763,7 +763,7 @@ let rec convertExpr env e = EF_debug(P.of_int64 kind, intern_string text, typlist_of_typelist targs2), targs2, convertExprList env args2, convertTyp env e.etyp) - + | C.ECall({edesc = C.EVar {name = "__builtin_annot"}}, args) -> begin match args with | {edesc = C.EConst(CStr txt)} :: args1 -> @@ -774,20 +774,20 @@ let rec convertExpr env e = | _ -> error "ill-formed __builtin_annot (first argument must be string literal)"; ezero - end - + end + | C.ECall({edesc = C.EVar {name = "__builtin_annot_intval"}}, args) -> begin match args with | [ {edesc = C.EConst(CStr txt)}; arg ] -> let targ = convertTyp env (Cutil.default_argument_conversion env arg.etyp) in Ebuiltin(EF_annot_val(intern_string txt, typ_of_type targ), - Tcons(targ, Tnil), convertExprList env [arg], + Tcons(targ, Tnil), convertExprList env [arg], convertTyp env e.etyp) | _ -> error "ill-formed __builtin_annot_intval (first argument must be string literal)"; ezero - end + end | C.ECall({edesc = C.EVar {name = "__builtin_memcpy_aligned"}}, args) -> make_builtin_memcpy (convertExprList env args) @@ -822,9 +822,9 @@ let rec convertExpr env e = let sg = signature_of_type targs tres {cc_vararg = true; cc_unproto = false; cc_structret = false} in - Ebuiltin(EF_external(intern_string "printf", sg), + Ebuiltin(EF_external(intern_string "printf", sg), targs, convertExprList env args, tres) - + | C.ECall(fn, args) -> if not (supported_return_type env e.etyp) then unsupported ("function returning a result of type " ^ string_of_type e.etyp ^ " (consider adding option -fstruct-return)"); @@ -867,17 +867,17 @@ and convertExprList env el = (* Extended assembly *) let convertAsm loc env txt outputs inputs clobber = - let (txt', output', inputs') = + let (txt', output', inputs') = ExtendedAsm.transf_asm loc env txt outputs inputs clobber in let clobber' = List.map (fun s -> coqstring_of_camlstring (String.uppercase s)) clobber in let ty_res = match output' with None -> TVoid [] | Some e -> e.etyp in (* Build the Ebuiltin expression *) - let e = + let e = let tinputs = convertTypArgs env [] inputs' in let toutput = convertTyp env ty_res in - Ebuiltin(EF_inline_asm(intern_string txt', + Ebuiltin(EF_inline_asm(intern_string txt', signature_of_type tinputs toutput cc_default, clobber'), tinputs, @@ -894,7 +894,7 @@ type switchlabel = | Case of C.exp | Default -type switchbody = +type switchbody = | Label of switchlabel | Stmt of C.stmt @@ -922,16 +922,16 @@ let rec groupSwitch = function (Cutil.sseq s.sloc s fst, cases) (* Test whether the statement contains case and give an *) -let rec contains_case s = +let rec contains_case s = match s.sdesc with - | C.Sskip - | C.Sdo _ + | C.Sskip + | C.Sdo _ | C.Sbreak - | C.Scontinue + | C.Scontinue | C.Sswitch _ (* Stop at a switch *) - | C.Sgoto _ - | C.Sreturn _ - | C.Sdecl _ + | C.Sgoto _ + | C.Sreturn _ + | C.Sdecl _ | C.Sasm _ -> () | C.Sseq (s1,s2) | C.Sif(_,s1,s2) -> contains_case s1; contains_case s2 @@ -1021,7 +1021,7 @@ and convertSwitch env is_64 = function match lbl with | Default -> None - | Case e -> + | Case e -> match Ceval.integer_expr env e with | None -> unsupported "'case' label is not a compile-time integer"; None @@ -1127,7 +1127,7 @@ let convertInitializer env ty i = let convertGlobvar loc env (sto, id, ty, optinit) = let id' = intern_string id.name in Debug.atom_global id id'; - let ty' = convertTyp env ty in + let ty' = convertTyp env ty in let sz = Ctypes.sizeof !comp_env ty' in let al = Ctypes.alignof !comp_env ty' in let attr = Cutil.attributes_of_type env ty in @@ -1189,7 +1189,7 @@ let rec convertGlobdecls env res gl = warning ("'#pragma " ^ s ^ "' directive ignored"); convertGlobdecls env res gl' -(** Convert struct and union declarations. +(** Convert struct and union declarations. Result is a list of CompCert C composite declarations. *) let rec convertCompositedefs env res gl = @@ -1228,7 +1228,7 @@ let rec translEnv env = function module IdentSet = Set.Make(struct type t = C.ident let compare = compare end) let cleanupGlobals p = - + (* First pass: determine what is defined *) let strong = ref IdentSet.empty (* def functions or variables with inits *) and weak = ref IdentSet.empty (* variables without inits *) @@ -1251,7 +1251,7 @@ let cleanupGlobals p = | _ -> () in List.iter classify_def p; - (* Second pass: keep "best" definition for each identifier *) + (* Second pass: keep "best" definition for each identifier *) let rec clean defs accu = function | [] -> accu | g :: gl -> -- cgit From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- cfrontend/C2C.ml | 76 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 38 insertions(+), 38 deletions(-) (limited to 'cfrontend/C2C.ml') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 9b31dfdb..4835f785 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -141,8 +141,8 @@ let builtins_generic = { (* Block copy *) "__builtin_memcpy_aligned", (TVoid [], - [TPtr(TVoid [], []); - TPtr(TVoid [AConst], []); + [TPtr(TVoid [], []); + TPtr(TVoid [AConst], []); TInt(IUInt, []); TInt(IUInt, [])], false); @@ -357,12 +357,12 @@ let make_builtin_memcpy args = let sz1 = match Initializers.constval !comp_env sz with | Errors.OK(Vint n) -> n - | _ -> error "ill-formed __builtin_memcpy_aligned (3rd argument must be + | _ -> error "ill-formed __builtin_memcpy_aligned (3rd argument must be a constant)"; Integers.Int.zero in let al1 = match Initializers.constval !comp_env al with | Errors.OK(Vint n) -> n - | _ -> error "ill-formed __builtin_memcpy_aligned (4th argument must be + | _ -> error "ill-formed __builtin_memcpy_aligned (4th argument must be a constant)"; Integers.Int.one in (* to check: sz1 > 0, al1 divides sz1, al1 = 1|2|4|8 *) (* Issue #28: must decay array types to pointer types *) @@ -384,7 +384,7 @@ let va_list_ptr e = let make_builtin_va_arg_by_val helper ty ty_ret arg = let ty_fun = Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), ty_ret, cc_default) in - Ecast + Ecast (Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun), Econs(va_list_ptr arg, Enil), ty_ret), @@ -392,13 +392,13 @@ let make_builtin_va_arg_by_val helper ty ty_ret arg = let make_builtin_va_arg_by_ref helper ty arg = let ty_fun = - Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), + Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), Tpointer(Tvoid, noattr), cc_default) in let ty_ptr = Tpointer(ty, noattr) in let call = Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun), - Econs(va_list_ptr arg, + Econs(va_list_ptr arg, Econs(Esizeof(ty, Tint(I32, Unsigned, noattr)), Enil)), Tpointer(Tvoid, noattr)) in Evalof(Ederef(Ecast(call, ty_ptr), ty), ty) @@ -406,13 +406,13 @@ let make_builtin_va_arg_by_ref helper ty arg = let make_builtin_va_arg env ty e = match ty with | Tint _ | Tpointer _ -> - make_builtin_va_arg_by_val + make_builtin_va_arg_by_val "__compcert_va_int32" ty (Tint(I32, Unsigned, noattr)) e | Tlong _ -> - make_builtin_va_arg_by_val + make_builtin_va_arg_by_val "__compcert_va_int64" ty (Tlong(Unsigned, noattr)) e | Tfloat _ -> - make_builtin_va_arg_by_val + make_builtin_va_arg_by_val "__compcert_va_float64" ty (Tfloat(F64, noattr)) e | Tstruct _ | Tunion _ -> make_builtin_va_arg_by_ref @@ -433,7 +433,7 @@ let rec log2 n = if n = 1 then 0 else 1 + log2 (n lsr 1) let convertAttr a = { attr_volatile = List.mem AVolatile a; - attr_alignas = + attr_alignas = let n = Cutil.alignas_attribute a in if n > 0 then Some (N.of_int (log2 n)) else None } @@ -463,7 +463,7 @@ let convertFkind = function | C.FFloat -> F32 | C.FDouble -> F64 | C.FLongDouble -> - if not !Clflags.option_flongdouble then unsupported "'long double' type"; + if not !Clflags.option_flongdouble then unsupported "'long double' type"; F64 let rec convertTyp env t = @@ -524,11 +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 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) + TStruct (id,attr) | C.Union -> TUnion (id,attr) in Debug.set_composite_size id su (Cutil.sizeof env t); Composite(intern_string id.name, @@ -763,7 +763,7 @@ let rec convertExpr env e = EF_debug(P.of_int64 kind, intern_string text, typlist_of_typelist targs2), targs2, convertExprList env args2, convertTyp env e.etyp) - + | C.ECall({edesc = C.EVar {name = "__builtin_annot"}}, args) -> begin match args with | {edesc = C.EConst(CStr txt)} :: args1 -> @@ -774,20 +774,20 @@ let rec convertExpr env e = | _ -> error "ill-formed __builtin_annot (first argument must be string literal)"; ezero - end - + end + | C.ECall({edesc = C.EVar {name = "__builtin_annot_intval"}}, args) -> begin match args with | [ {edesc = C.EConst(CStr txt)}; arg ] -> let targ = convertTyp env (Cutil.default_argument_conversion env arg.etyp) in Ebuiltin(EF_annot_val(coqstring_of_camlstring txt, typ_of_type targ), - Tcons(targ, Tnil), convertExprList env [arg], + Tcons(targ, Tnil), convertExprList env [arg], convertTyp env e.etyp) | _ -> error "ill-formed __builtin_annot_intval (first argument must be string literal)"; ezero - end + end | C.ECall({edesc = C.EVar {name = "__builtin_memcpy_aligned"}}, args) -> make_builtin_memcpy (convertExprList env args) @@ -822,9 +822,9 @@ let rec convertExpr env e = let sg = signature_of_type targs tres {cc_vararg = true; cc_unproto = false; cc_structret = false} in - Ebuiltin(EF_external(coqstring_of_camlstring "printf", sg), + Ebuiltin(EF_external(coqstring_of_camlstring "printf", sg), targs, convertExprList env args, tres) - + | C.ECall(fn, args) -> if not (supported_return_type env e.etyp) then unsupported ("function returning a result of type " ^ string_of_type e.etyp ^ " (consider adding option -fstruct-return)"); @@ -867,17 +867,17 @@ and convertExprList env el = (* Extended assembly *) let convertAsm loc env txt outputs inputs clobber = - let (txt', output', inputs') = + let (txt', output', inputs') = ExtendedAsm.transf_asm loc env txt outputs inputs clobber in let clobber' = List.map (fun s -> coqstring_of_camlstring (String.uppercase s)) clobber in let ty_res = match output' with None -> TVoid [] | Some e -> e.etyp in (* Build the Ebuiltin expression *) - let e = + let e = let tinputs = convertTypArgs env [] inputs' in let toutput = convertTyp env ty_res in - Ebuiltin(EF_inline_asm(coqstring_of_camlstring txt', + Ebuiltin(EF_inline_asm(coqstring_of_camlstring txt', signature_of_type tinputs toutput cc_default, clobber'), tinputs, @@ -894,7 +894,7 @@ type switchlabel = | Case of C.exp | Default -type switchbody = +type switchbody = | Label of switchlabel | Stmt of C.stmt @@ -922,16 +922,16 @@ let rec groupSwitch = function (Cutil.sseq s.sloc s fst, cases) (* Test whether the statement contains case and give an *) -let rec contains_case s = +let rec contains_case s = match s.sdesc with - | C.Sskip - | C.Sdo _ + | C.Sskip + | C.Sdo _ | C.Sbreak - | C.Scontinue + | C.Scontinue | C.Sswitch _ (* Stop at a switch *) - | C.Sgoto _ - | C.Sreturn _ - | C.Sdecl _ + | C.Sgoto _ + | C.Sreturn _ + | C.Sdecl _ | C.Sasm _ -> () | C.Sseq (s1,s2) | C.Sif(_,s1,s2) -> contains_case s1; contains_case s2 @@ -1021,7 +1021,7 @@ and convertSwitch env is_64 = function match lbl with | Default -> None - | Case e -> + | Case e -> match Ceval.integer_expr env e with | None -> unsupported "'case' label is not a compile-time integer"; None @@ -1128,7 +1128,7 @@ let convertInitializer env ty i = let convertGlobvar loc env (sto, id, ty, optinit) = let id' = intern_string id.name in Debug.atom_global_variable id id'; - let ty' = convertTyp env ty in + let ty' = convertTyp env ty in let sz = Ctypes.sizeof !comp_env ty' in let al = Ctypes.alignof !comp_env ty' in let attr = Cutil.attributes_of_type env ty in @@ -1190,7 +1190,7 @@ let rec convertGlobdecls env res gl = warning ("'#pragma " ^ s ^ "' directive ignored"); convertGlobdecls env res gl' -(** Convert struct and union declarations. +(** Convert struct and union declarations. Result is a list of CompCert C composite declarations. *) let rec convertCompositedefs env res gl = @@ -1229,7 +1229,7 @@ let rec translEnv env = function module IdentSet = Set.Make(struct type t = C.ident let compare = compare end) let cleanupGlobals p = - + (* First pass: determine what is defined *) let strong = ref IdentSet.empty (* def functions or variables with inits *) and weak = ref IdentSet.empty (* variables without inits *) @@ -1252,7 +1252,7 @@ let cleanupGlobals p = | _ -> () in List.iter classify_def p; - (* Second pass: keep "best" definition for each identifier *) + (* Second pass: keep "best" definition for each identifier *) let rec clean defs accu = function | [] -> accu | g :: gl -> -- cgit