diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-11 11:03:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-11 11:03:30 +0200 |
| commit | 79b2f30b22e1a0baeea614813e6984871ec16089 (patch) | |
| tree | 70342e5a24cfd422ad144b239bdc104691013052 | |
| parent | d5ff40b57c880a096d8997d20f6211880336659a (diff) | |
| parent | 2a6876b762f21e624a9138927dff5baf29086397 (diff) | |
Merge PR #8021: Get rid of horrendous hack limiting the size of parsed integers
| -rw-r--r-- | parsing/g_prim.mlg | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index 774db97f2..dfb788907 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -24,13 +24,9 @@ let local_make_qualid loc l id = make_qualid ~loc (DirPath.make 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 -> - CErrors.user_err ~loc (Pp.str "Cannot support a so large number.") + int_of_string s + with Failure _ -> + CErrors.user_err ~loc (Pp.str "This number is too large.") } |