Commit adff86c0 authored by Sylvain Boulmé's avatar Sylvain Boulmé
Browse files

fix extraction of non-aarch64 targets

parent 471a8363
......@@ -76,6 +76,7 @@
/lib/Responsefile.ml
/driver/Version.ml
/driver/Compiler.v
/extraction/extraction.v
# Documentation
/doc/coq2html
/doc/coq2html.ml
......
......@@ -249,8 +249,8 @@ endif
tools/compiler_expand: tools/compiler_expand.ml
ifeq ($(OCAML_NATIVE_COMP),true)
ocamlopt -o $@ $+
ocamlc -o $@ $+
else
ocamlc -o $@ $+
endif
tools/modorder: tools/modorder.ml
......@@ -274,6 +274,11 @@ latexdoc:
@tools/ndfun $*.vp > $*.v || { rm -f $*.v; exit 2; }
@chmod a-w $*.v
extraction/extraction.v: Makefile extraction/extraction.vexpand
cat extraction/extraction.vexpand > extraction/extraction.v
echo "$(EXTRA_EXTRACTION)" >> extraction/extraction.v
echo "." >> extraction/extraction.v
driver/Compiler.v: driver/Compiler.vexpand tools/compiler_expand
tools/compiler_expand driver/Compiler.vexpand $@
......@@ -354,10 +359,10 @@ clean:
rm -f $(patsubst %, %/*.vo*, $(DIRS))
rm -f $(patsubst %, %/.*.aux, $(DIRS))
rm -rf doc/html doc/*.glob
rm -f driver/Version.ml
rm -f driver/Version.ml driver/Compiler.v
rm -f compcert.ini compcert.config
rm -f extraction/STAMP extraction/*.ml extraction/*.mli .depend.extr
rm -f tools/ndfun tools/modorder tools/*.cm? tools/*.o
rm -f extraction/STAMP extraction/*.ml extraction/*.mli .depend.extr extraction/extraction.v
rm -f tools/ndfun tools/modorder tools/compiler_expand tools/*.cm? tools/*.o
rm -f $(GENERATED) .depend
rm -f .lia.cache
$(MAKE) -f Makefile.extr clean
......
......@@ -824,6 +824,7 @@ BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v OptionMonad.v IterList
ImpConfig.v ImpCore.v ImpExtern.v ImpHCons.v ImpIO.v ImpLoops.v ImpMonads.v ImpPrelude.v
# TODO: UPDATE THIS
# DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v
EXTRA_EXTRACTION= Asmgen.Asmgen_expand.loadimm32 Asmgen.Asmgen_expand.addimm64 Asmgen.Asmgen_expand.storeptr
EOF
fi
......
......@@ -248,5 +248,3 @@ Separate Extraction
Parser.translation_unit_file
Compopts.optim_postpass
Archi.has_notrap_loads
Asmgen.Asmgen_expand.loadimm32 Asmgen.Asmgen_expand.addimm64
Asmgen.Asmgen_expand.storeptr.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment