aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Env.mli
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2020-07-20 11:55:35 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2020-07-20 16:27:00 +0200
commitb4c6087cd0faf3d165ca5450f7462b9fbe98796f (patch)
tree43a654c4382446241322379e12bd2d779f8572d8 /cparser/Env.mli
parent72f78307cec2ac8fb33d657b118a930b2acfe8ad (diff)
downloadcompcert-kvx-b4c6087cd0faf3d165ca5450f7462b9fbe98796f.tar.gz
compcert-kvx-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/Env.mli')
-rw-r--r--cparser/Env.mli1
1 files changed, 1 insertions, 0 deletions
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