diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-20 12:00:16 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-20 12:00:16 +0100 |
| commit | 6462da4e8f25ce5df951635828901ad0180e9958 (patch) | |
| tree | ef5d83e00bd04f448ef46480bb5cd218175c6430 /configure | |
| parent | 92188c18a3761fa14dfdb97010cebe919548a010 (diff) | |
| download | compcert-kvx-6462da4e8f25ce5df951635828901ad0180e9958.tar.gz compcert-kvx-6462da4e8f25ce5df951635828901ad0180e9958.zip | |
Integrating Asmvliw.v in the proof chain
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -804,7 +804,7 @@ if [ "$arch" = "mppa_k1c" ]; then cat >> Makefile.config <<EOF ARCHDIRS=$arch $arch/lib $arch/abstractbb $arch/abstractbb/Impure BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\ - Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v\\ + Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v\\ ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\ Asmblockdeps.v\\ AbstractBasicBlocksDef.v DepTreeTheory.v ImpDep.v Parallelizability.v\\ |