From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 8 Aug 2008 13:18:42 +0200
Subject: Imported Upstream version 8.2~beta4+dfsg

---
 parsing/g_prim.ml4 | 20 +++++++++++++++-----
 1 file changed, 15 insertions(+), 5 deletions(-)

(limited to 'parsing/g_prim.ml4')

diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index c3792d65..1e738384 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(*i $Id: g_prim.ml4 10155 2007-09-28 22:36:35Z glondu $ i*)
+(*i $Id: g_prim.ml4 11309 2008-08-06 10:30:35Z herbelin $ i*)
 
 open Pcoq
 open Names
@@ -23,6 +23,16 @@ open Nametab
 
 let local_make_qualid l id = make_qualid (make_dirpath l) id
 
+let my_int_of_string loc s =
+  try
+    let n = int_of_string s in
+    (* To avoid Array.make errors (that e.g. Undo uses), we set a *)
+    (* more restricted limit than int_of_string does *)
+    if n > 1024 * 2048 then raise Exit;
+    n
+  with Failure _ | Exit ->
+    Util.user_err_loc (loc,"",Pp.str "Cannot support a so large number.")
+
 GEXTEND Gram
   GLOBAL: 
     bigint natural integer identref name ident var preident
@@ -79,7 +89,7 @@ GEXTEND Gram
   ;
   ne_string:
     [ [ s = STRING -> 
-        if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string"); s
+        if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string."); s
     ] ]
   ;
   dirpath:
@@ -90,11 +100,11 @@ GEXTEND Gram
     [ [ s = STRING -> s ] ]
   ;
   integer:
-    [ [ i = INT      -> int_of_string i
-      | "-"; i = INT -> - int_of_string i ] ]
+    [ [ i = INT      -> my_int_of_string loc i
+      | "-"; i = INT -> - my_int_of_string loc i ] ]
   ;
   natural:
-    [ [ i = INT -> int_of_string i ] ]
+    [ [ i = INT -> my_int_of_string loc i ] ]
   ;
   bigint: (* Negative numbers are dealt with specially *)
     [ [ i = INT -> (Bigint.of_string i) ] ]
-- 
cgit v1.2.3