diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-10-17 15:43:14 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-10-17 15:43:14 +0200 |
commit | db3183cacb132d7153f653e2c3ae20b92ddfc03c (patch) | |
tree | c8a756d36267abd3349cec82c1f4daadff083371 /configure | |
parent | ae3e1ed0515236e25924b12d475bc991a33b7632 (diff) | |
download | compcert-kvx-db3183cacb132d7153f653e2c3ae20b92ddfc03c.tar.gz compcert-kvx-db3183cacb132d7153f653e2c3ae20b92ddfc03c.zip |
fixing the move of the verified prepass scheduler into scheduling/ directory
Diffstat (limited to 'configure')
-rwxr-xr-x | configure | 4 |
1 files changed, 1 insertions, 3 deletions
@@ -847,12 +847,10 @@ EXECUTE=kvx-cluster --syscall=libstd_scalls.so -- CFLAGS= -D __KVX_COS__ SIMU=kvx-cluster -- BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\ - RTLpath.v RTLpathproof.v RTLpathLivegen.v RTLpathLivegenproof.v RTLpathSE_theory.v RTLpathSE_simu_specs.v RTLpathSE_impl.v RTLpathScheduler.v RTLpathSchedulerproof.v\\ Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v Asmblockprops.v\\ ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\ Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\ - AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v\\ - ImpConfig.v ImpCore.v ImpExtern.v ImpHCons.v ImpIO.v ImpLoops.v ImpMonads.v ImpPrelude.v + AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v EOF fi |