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 /backend/CSEproof.v | |
| parent | d08b080747225160b80c3f04bdfd9cd67550b425 (diff) | |
| download | compcert-kvx-e16b34d9fc1aa7854759787fd52ad59c964c2d4b.tar.gz compcert-kvx-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 'backend/CSEproof.v')
0 files changed, 0 insertions, 0 deletions