diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-06-19 19:57:07 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-06-19 19:57:07 +0200 |
commit | 6c0851fafad28d4d63476d47d75a06f67af704a5 (patch) | |
tree | 23b55b8d60b6f67c71b30d6c6c943600cc1b2f45 /configure | |
parent | 6c411683654608bfeabc307e8ed219a1de0426c7 (diff) | |
download | compcert-kvx-6c0851fafad28d4d63476d47d75a06f67af704a5.tar.gz compcert-kvx-6c0851fafad28d4d63476d47d75a06f67af704a5.zip |
start aarch64/Asmblock (work-in-progress)
Diffstat (limited to 'configure')
-rwxr-xr-x | configure | 5 |
1 files changed, 3 insertions, 2 deletions
@@ -697,7 +697,7 @@ echo "-R lib compcert.lib \ -R MenhirLib compcert.MenhirLib" > _CoqProject case $arch in aarch64) - echo "-R kvx compcert.kvx" >> _CoqProject + echo "-R kvx/lib compcert.kvx.lib -R kvx/abstractbb compcert.kvx.abstractbb" >> _CoqProject # import KVX libraries for aarch64 ;; x86) echo "-R x86_${bitsize} compcert.x86_${bitsize}" >> _CoqProject @@ -841,12 +841,13 @@ RESPONSEFILE="none" EOF fi -if [ "$arch" = "aarch64" ]; then +if [ "$arch" = "aarch64" ]; then # for aarch64 scheduling cat >> Makefile.config <<EOF ARCHDIRS=$arch kvx/lib kvx/abstractbb kvx/abstractbb/Impure BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v OptionMonad.v IterList.v PseudoAsmblock.v PseudoAsmblockproof.v ForwardSimulationBlock.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\\ + Asmblock.v\\ Asmgenproof0.v Asmgenproof1.v Asmgenproof.v # TODO: CHANGE THIS EOF fi |