From 5e2574cbef1ba132aacc73b4a079cc0b5584f589 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 23 Feb 2017 14:57:59 +0100 Subject: [safe-string] Enable -safe-string ! We now build Coq with `-safe-string`, which enforces functional use of the `string` datatype. Coq was pretty safe in these regard so only a few tweaks were needed. - coq_makefile: build plugins with -safe-string too. - `names.ml`: we remove `String.copy` uses, as they are not needed. --- configure.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'configure.ml') diff --git a/configure.ml b/configure.ml index 82ce931d6..dfc6724a2 100644 --- a/configure.ml +++ b/configure.ml @@ -264,6 +264,10 @@ module Prefs = struct let debug = ref true let profile = ref false let annotate = ref false + (* Note, disabling this should be OK, but be careful with the + sharing invariants. + *) + let safe_string = ref true let nativecompiler = ref (not (os_type_win32 || os_type_cygwin)) let coqwebsite = ref "http://coq.inria.fr/" let force_caml_version = ref false @@ -386,6 +390,9 @@ let coq_annotate_flag = then if program_in_path "ocamlmerlin" then "-bin-annot" else "-annot" else "" +let coq_safe_string = + if !Prefs.safe_string then "-safe-string" else "" + let cflags = "-Wall -Wno-unused -g -O2" (** * Architecture *) @@ -1118,7 +1125,7 @@ let write_makefile f = pr "CAMLHLIB=%S\n\n" camllib; pr "# Caml link command and Caml make top command\n"; pr "# Caml flags\n"; - pr "CAMLFLAGS=-rectypes %s\n" coq_annotate_flag; + pr "CAMLFLAGS=-rectypes %s %s\n" coq_annotate_flag coq_safe_string; pr "# User compilation flag\n"; pr "USERFLAGS=\n\n"; pr "# Flags for GCC\n"; -- cgit v1.2.3