Checking that a library name is valid before compilation.

Fixes bug #3333.

1 files changed, 22 insertions, 1 deletions

diff --git a/library/library.ml b/library/library.ml
index fc74d25b4..4f023ce6d 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -663,6 +663,25 @@ let check_coq_overwriting p id =
       (strbrk ("Cannot build module "^DirPath.to_string p^"."^Id.to_string id^
       ": it starts with prefix \"Coq\" which is reserved for the Coq library."))
 
+(* Verifies that a string starts by a letter and do not contain
+   others caracters than letters, digits, or `_` *)
+
+let check_module_name s =
+  let msg c =
+    strbrk "Invalid module name: " ++ str s ++ strbrk " character " ++
+    (if c = '\'' then str "\"'\"" else (str "'" ++ str (String.make 1 c) ++ str "'")) ++
+    strbrk " is not allowed in module names\n"
+  in
+  let err c = errorlabstrm "" (msg c) in
+  match String.get s 0 with
+    | 'a' .. 'z' | 'A' .. 'Z' ->
+        for i = 1 to (String.length s)-1 do
+          match String.get s i with
+            | 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '_'  -> ()
+            | c -> err c
+        done
+    | c -> err c
+
 let start_library f =
   let paths = Loadpath.get_paths () in
   let _, longf =
@@ -673,7 +692,9 @@ let start_library f =
       Loadpath.logical lp
     with Not_found -> Nameops.default_root_prefix
   in
-  let id = Id.of_string (Filename.basename f) in
+  let file = Filename.basename f in
+  let id = Id.of_string file in
+  check_module_name file;
   check_coq_overwriting ldir0 id;
   let ldir = add_dirpath_suffix ldir0 id in
   OpaqueTables.reset ();