aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorSylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>2021-05-28 15:24:16 +0200
committerSylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>2021-05-28 15:24:16 +0200
commitb79d0a04787d9234cf580841bf58e592fe4ab3ee (patch)
treed1bef8184071e30612178cfc53c820e59b1e0675 /Makefile
parent25595a7b34b70011dcb77aae277ee1cdb8920c60 (diff)
downloadcompcert-kvx-b79d0a04787d9234cf580841bf58e592fe4ab3ee.tar.gz
compcert-kvx-b79d0a04787d9234cf580841bf58e592fe4ab3ee.zip
starting to extend RTLtoBTL with Liveness checking (on BTL side)
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 3d9e8bdd..60cf380b 100644
--- a/Makefile
+++ b/Makefile
@@ -144,7 +144,7 @@ SCHEDULING= \
RTLpathSchedulerproof.v RTLpath.v \
RTLpathScheduler.v RTLpathWFcheck.v \
BTL.v BTLmatchRTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v \
- BTL_SEtheory.v
+ BTL_Livecheck.v BTL_Scheduler.v BTL_Schedulerproof.v BTL_SEtheory.v
# C front-end modules (in cfrontend/)