diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-07-03 11:06:07 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-07-17 09:17:28 +0200 |
commit | e16b34d9fc1aa7854759787fd52ad59c964c2d4b (patch) | |
tree | ba63485dfd5706cb9191d8ce4a2cfb71d3604287 /common/Builtins0.v | |
parent | d08b080747225160b80c3f04bdfd9cd67550b425 (diff) | |
download | compcert-e16b34d9fc1aa7854759787fd52ad59c964c2d4b.tar.gz compcert-e16b34d9fc1aa7854759787fd52ad59c964c2d4b.zip |
Perform constant propagation for known built-in functions
When an external function is a known built-in function and it is
applied to compile-time integer or FP constants, we can use
the known semantics of the builtin to compute the result
at compile-time.
Diffstat (limited to 'common/Builtins0.v')
0 files changed, 0 insertions, 0 deletions