From 10941819e09e2f9090e7fe39301a0b9026a0eba0 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Wed, 5 Nov 2014 14:36:14 +0100
Subject: Verification of the Unusedglob pass (removal of unreferenced static
 global definitions).  Assorted changes to ia32/Op.v.  PowerPC and ARM need
 updating.

---
 Makefile | 1 +
 1 file changed, 1 insertion(+)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 2b668724..3f87287e 100644
--- a/Makefile
+++ b/Makefile
@@ -91,6 +91,7 @@ BACKEND=\
   ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \
   CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \
   NeedDomain.v NeedOp.v Deadcode.v Deadcodeproof.v \
+  Unusedglob.v Unusedglobproof.v \
   Machregs.v Locations.v Conventions1.v Conventions.v LTL.v \
   Allocation.v Allocproof.v \
   Tunneling.v Tunnelingproof.v \
-- 
cgit 


From 866e612bf63568cbe9871bb1d6724323493651e7 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Thu, 11 Dec 2014 09:29:48 +0100
Subject: Preserve single quotes (e.g. in CPREPRO) when generating compcert.ini

---
 Makefile | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 3f87287e..896a456e 100644
--- a/Makefile
+++ b/Makefile
@@ -222,16 +222,16 @@ latexdoc:
 	@chmod -w $*.v
 
 compcert.ini: Makefile.config VERSION
-	(echo stdlib_path=$(LIBDIR); \
-         echo prepro=$(CPREPRO); \
-         echo asm=$(CASM); \
-         echo linker=$(CLINKER); \
-         echo arch=$(ARCH); \
-         echo model=$(MODEL); \
-         echo abi=$(ABI); \
-         echo system=$(SYSTEM); \
-         echo has_runtime_lib=$(HAS_RUNTIME_LIB); \
-         echo asm_supports_cfi=$(ASM_SUPPORTS_CFI); \
+	(echo "stdlib_path=$(LIBDIR)"; \
+         echo "prepro=$(CPREPRO)"; \
+         echo "asm=$(CASM)"; \
+         echo "linker=$(CLINKER)"; \
+         echo "arch=$(ARCH)"; \
+         echo "model=$(MODEL)"; \
+         echo "abi=$(ABI)"; \
+         echo "system=$(SYSTEM)"; \
+         echo "has_runtime_lib=$(HAS_RUNTIME_LIB)"; \
+         echo "asm_supports_cfi=$(ASM_SUPPORTS_CFI)"; \
          version=`cat VERSION`; \
          echo version=$$version) \
         > compcert.ini
-- 
cgit 


From 97257c59566d9506a2ff397ec35fff7b59506a8f Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Wed, 17 Dec 2014 11:32:16 +0100
Subject: Use cp instead of symbolic links for executables. Now that we search
 for compcert.ini from Sys.executable, symbolic links cause compcert.ini not
 to be found.

---
 Makefile | 23 ++++++++---------------
 1 file changed, 8 insertions(+), 15 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 896a456e..352a1b2f 100644
--- a/Makefile
+++ b/Makefile
@@ -31,6 +31,7 @@ COQDEP="$(COQBIN)coqdep" $(COQINCLUDES)
 COQDOC="$(COQBIN)coqdoc"
 COQEXEC="$(COQBIN)coqtop" $(COQINCLUDES) -batch -load-vernac-source
 COQCHK="$(COQBIN)coqchk" $(COQINCLUDES)
+CP=cp
 
 OCAMLBUILD=ocamlbuild
 OCB_OPTIONS=\
@@ -130,14 +131,6 @@ DRIVER=Compopts.v Compiler.v Complements.v
 FILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \
   $(PARSERVALIDATOR) $(PARSER)
 
-# Symbolic links vs. copy
-
-ifneq (,$(findstring CYGWIN,$(shell uname -s)))
-SLN=cp
-else
-SLN=ln -s
-endif
-
 all:
 	$(MAKE) proof
 	$(MAKE) extraction
@@ -160,34 +153,34 @@ extraction/STAMP: $(FILES:.v=.vo) extraction/extraction.v $(ARCH)/extractionMach
 
 ccomp: extraction/STAMP compcert.ini
 	$(OCAMLBUILD) $(OCB_OPTIONS) Driver.native \
-        && rm -f ccomp && $(SLN) _build/driver/Driver.native ccomp
+        && $(CP) _build/driver/Driver.native ccomp
 
 ccomp.prof: extraction/STAMP compcert.ini
 	$(OCAMLBUILD) $(OCB_OPTIONS) Driver.p.native \
-        && rm -f ccomp.prof && $(SLN) _build/driver/Driver.p.native ccomp.prof
+        && $(CP) _build/driver/Driver.p.native ccomp.prof
 
 ccomp.byte: extraction/STAMP compcert.ini
 	$(OCAMLBUILD) $(OCB_OPTIONS) Driver.d.byte \
-        && rm -f ccomp.byte && $(SLN) _build/driver/Driver.d.byte ccomp.byte
+        && $(CP) _build/driver/Driver.d.byte ccomp.byte
 
 runtime:
 	$(MAKE) -C runtime
 
 cchecklink: compcert.ini
 	$(OCAMLBUILD) $(OCB_OPTIONS_CHECKLINK) Validator.native \
-        && rm -f cchecklink && $(SLN) _build/checklink/Validator.native cchecklink
+        && $(CP) _build/checklink/Validator.native cchecklink
 
 cchecklink.byte: compcert.ini
 	$(OCAMLBUILD) $(OCB_OPTIONS_CHECKLINK) Validator.d.byte \
-        && rm -f cchecklink.byte && $(SLN) _build/checklink/Validator.d.byte cchecklink.byte
+        && $(CP) _build/checklink/Validator.d.byte cchecklink.byte
 
 clightgen: extraction/STAMP compcert.ini exportclight/Clightdefs.vo
 	$(OCAMLBUILD) $(OCB_OPTIONS_CLIGHTGEN) Clightgen.native \
-        && rm -f clightgen && $(SLN) _build/exportclight/Clightgen.native clightgen
+        && $(CP) _build/exportclight/Clightgen.native clightgen
 
 clightgen.byte: extraction/STAMP compcert.ini exportclight/Clightdefs.vo
 	$(OCAMLBUILD) $(OCB_OPTIONS_CLIGHTGEN) Clightgen.d.byte \
-        && rm -f clightgen.byte && $(SLN) _build/exportclight/Clightgen.d.byte clightgen.byte
+        && $(CP) _build/exportclight/Clightgen.d.byte clightgen.byte
 
 .PHONY: proof extraction ccomp ccomp.prof ccomp.byte runtime cchecklink cchecklink.byte clightgen clightgen.byte
 
-- 
cgit