summaryrefslogtreecommitdiff
path: root/parsing/g_prim.ml4
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
commit870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch)
tree0c647056de1832cf1dba5ba58758b9121418e4be /parsing/g_prim.ml4
parenta0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff)
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'parsing/g_prim.ml4')
-rw-r--r--parsing/g_prim.ml420
1 files changed, 15 insertions, 5 deletions
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) ] ]