From b4c6087cd0faf3d165ca5450f7462b9fbe98796f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 20 Jul 2020 11:55:35 +0200 Subject: Added error for redefined builtin. We check in the initial environment if a function is already defined to avoid redefinition of functions that are part of the builtin environment. --- cparser/Elab.ml | 2 ++ cparser/Env.ml | 3 +++ cparser/Env.mli | 1 + 3 files changed, 6 insertions(+) (limited to 'cparser') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 4f2ddce7..b74e34d0 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2624,6 +2624,8 @@ let elab_fundef genv spec name defs body loc = and structs and unions defined in the parameter list. *) let (fun_id, sto, inline, noret, ty, kr_params, genv, lenv) = elab_fundef_name genv spec name in + if Env.is_builtin fun_id.C.name then + error loc "definition of builtin function '%s'" fun_id.C.name; let s = fun_id.C.name in if sto = Storage_auto || sto = Storage_register then fatal_error loc "invalid storage class %s on function" diff --git a/cparser/Env.ml b/cparser/Env.ml index 4723a725..00806be1 100644 --- a/cparser/Env.ml +++ b/cparser/Env.ml @@ -316,6 +316,9 @@ let set_builtins blt = List.iter Init.add_typedef blt.builtin_typedefs; List.iter Init.add_function blt.builtin_functions +let is_builtin name = + ident_is_bound !Init.env name + (* Error reporting *) open Printf diff --git a/cparser/Env.mli b/cparser/Env.mli index 1baab68f..589a76c7 100644 --- a/cparser/Env.mli +++ b/cparser/Env.mli @@ -84,3 +84,4 @@ val initial: unit -> t val initial_identifiers: unit -> C.ident list val initial_declarations: unit -> C.globdecl list val set_builtins: C.builtins -> unit +val is_builtin : string -> bool -- cgit