aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-30 10:12:09 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-30 10:12:09 +0200
commitfd00d28f8065acf9b09a6510e1612a91e30ca29c (patch)
tree323df3891fdf06ee6bec7a9c38fb562b71b5dc3a /Makefile
parent4aad20a92dc926d8c537e65946ca03bf2b6b02b9 (diff)
downloadcompcert-kvx-fd00d28f8065acf9b09a6510e1612a91e30ca29c.tar.gz
compcert-kvx-fd00d28f8065acf9b09a6510e1612a91e30ca29c.zip
more on injection
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile1
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index ec5e2cd0..4cf9ccf1 100644
--- a/Makefile
+++ b/Makefile
@@ -86,6 +86,7 @@ BACKEND=\
Kildall.v Liveness.v \
ValueDomain.v ValueAOp.v ValueAnalysis.v \
ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \
+ Inject.v \
CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \
CSE2deps.v CSE2depsproof.v \
CSE2.v CSE2proof.v \