diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-22 09:09:45 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-22 09:09:45 +0200 |
| commit | 70618966a9ba8b3d0b5c5ec970ec71f1629fbedf (patch) | |
| tree | 935824ed63933cdc333c60707a774fac5ad6949b /configure | |
| parent | df6ccab1280be1f5a47c3def1dd9cba0c91016dd (diff) | |
| download | compcert-kvx-70618966a9ba8b3d0b5c5ec970ec71f1629fbedf.tar.gz compcert-kvx-70618966a9ba8b3d0b5c5ec970ec71f1629fbedf.zip | |
start a junk implementation of the pre-pass verifier
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -845,7 +845,7 @@ 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_impl.v RTLpathScheduler.v RTLpathSchedulerproof.v\\ + RTLpath.v RTLpathproof.v RTLpathLivegen.v RTLpathLivegenproof.v RTLpathSE_theory.v RTLpathSE_impl_junk.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\\ |