diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2020-07-20 11:55:35 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2020-07-20 16:27:00 +0200 |
| commit | b4c6087cd0faf3d165ca5450f7462b9fbe98796f (patch) | |
| tree | 43a654c4382446241322379e12bd2d779f8572d8 /cparser/Elab.ml | |
| parent | 72f78307cec2ac8fb33d657b118a930b2acfe8ad (diff) | |
| download | compcert-b4c6087cd0faf3d165ca5450f7462b9fbe98796f.tar.gz compcert-b4c6087cd0faf3d165ca5450f7462b9fbe98796f.zip | |
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.
Diffstat (limited to 'cparser/Elab.ml')
| -rw-r--r-- | cparser/Elab.ml | 2 |
1 files changed, 2 insertions, 0 deletions
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" |