diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-05-31 19:09:25 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-06-06 10:58:13 +0200 |
| commit | 0025c4db576dbc174946b7adb83d4e0b81ce4b5f (patch) | |
| tree | 9e4218cfebe3bc74dbd723cdd50332a062c7e13e /backend/Selection.v | |
| parent | b028cfb4a2c342a49e165fa2267176feec7977ed (diff) | |
| download | compcert-kvx-0025c4db576dbc174946b7adb83d4e0b81ce4b5f.tar.gz compcert-kvx-0025c4db576dbc174946b7adb83d4e0b81ce4b5f.zip | |
Type inference and type checking for Cminor
This module is similar to RTLtyping: it performs type inference and
type checking, but on the Cminor intermediate representation rather
than the RTL IR. For each function, it returns a mapping from variables
to types. Its first use will be if-conversion optimization.
Diffstat (limited to 'backend/Selection.v')
0 files changed, 0 insertions, 0 deletions