diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-04-15 10:58:33 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-04-15 10:58:33 +0200 |
| commit | 5cde15375b66e41f380a2a130c3060d9be3cb177 (patch) | |
| tree | 23becf17d4b410eebc03692d29b979e860d8c551 /configure | |
| parent | d9c189200ee004d1823f4c37cbfd7efc6c152eda (diff) | |
| download | compcert-kvx-5cde15375b66e41f380a2a130c3060d9be3cb177.tar.gz compcert-kvx-5cde15375b66e41f380a2a130c3060d9be3cb177.zip | |
simplifying the translation, external calls + cfi_step on builtins
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -844,7 +844,7 @@ ARCHDIRS=$arch $arch/lib $arch/abstractbb $arch/abstractbb/Impure EXECUTE=k1-cluster --syscall=libstd_scalls.so -- CFLAGS= -D __K1C_COS__ SIMU=k1-cluster -- -BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v OptionMonad.v PseudoAsmblock.v PseudoAsmblockproof.v\\ +BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v OptionMonad.v IterList.v PseudoAsmblock.v PseudoAsmblockproof.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\\ |