diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-10-13 13:38:35 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-10-13 13:38:35 +0200 |
| commit | 7af1dae4e776b3977fcb16b5a770644e2932d7ca (patch) | |
| tree | fec7b2270e7d40eb0e593fa5adc4657fa7352e84 /configure | |
| parent | e13e255b375774a632fd825d32a3146ed593d11c (diff) | |
| download | compcert-kvx-7af1dae4e776b3977fcb16b5a770644e2932d7ca.tar.gz compcert-kvx-7af1dae4e776b3977fcb16b5a770644e2932d7ca.zip | |
refactoring of RTLpathSE_impl.v (split with _simu_specs)
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_junk.v RTLpathScheduler.v RTLpathSchedulerproof.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\\ |