diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2019-12-19 23:36:01 +0100 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-12-21 10:34:53 +0100 |
commit | 4b042d572b943c8cb3b86b61e3282bba58f488ab (patch) | |
tree | ae34d15572708ca62101f92b4e3acc1f480a092e /lib/Lattice.v | |
parent | 4dfcd7d4be18e8bc437ca170782212aa06635a95 (diff) | |
download | compcert-4b042d572b943c8cb3b86b61e3282bba58f488ab.tar.gz compcert-4b042d572b943c8cb3b86b61e3282bba58f488ab.zip |
Added error for unknown builtin functions. (#208)
Previously, using an unknown builtin function was treated like any
other call to an undeclared function: a warning was emitted, and
an error occurred at link-time.
With this commit, using an unknown builtin function is an error,
like in Clang.
Diffstat (limited to 'lib/Lattice.v')
0 files changed, 0 insertions, 0 deletions