From b52b60054e9d08ab7cdc20620c18bc2c45e71a2c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 Jun 2014 20:23:36 +0200 Subject: Checking that a library name is valid before compilation. Fixes bug #3333. --- library/library.ml | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) (limited to 'library') 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 (); -- cgit v1.2.3