aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2019-05-31 19:09:25 +0200
committerXavier Leroy <xavierleroy@users.noreply.github.com>2019-06-06 10:58:13 +0200
commit0025c4db576dbc174946b7adb83d4e0b81ce4b5f (patch)
tree9e4218cfebe3bc74dbd723cdd50332a062c7e13e /Makefile
parentb028cfb4a2c342a49e165fa2267176feec7977ed (diff)
downloadcompcert-0025c4db576dbc174946b7adb83d4e0b81ce4b5f.tar.gz
compcert-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 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 8ab6b5b0..369fd4cd 100644
--- a/Makefile
+++ b/Makefile
@@ -67,7 +67,7 @@ COMMON=Errors.v AST.v Linking.v \
# Back-end modules (in backend/, $(ARCH)/)
BACKEND=\
- Cminor.v Op.v CminorSel.v \
+ Cminor.v Cminortyping.v Op.v CminorSel.v \
SelectOp.v SelectDiv.v SplitLong.v SelectLong.v Selection.v \
SelectOpproof.v SelectDivproof.v SplitLongproof.v \
SelectLongproof.v Selectionproof.v \