diff options
| author |  Checkmate50 <dgeisler50@gmail.com> | 2016-07-19 16:39:54 -0600 |
|---|---|---|
| committer | Checkmate50 <dgeisler50@gmail.com> | 2016-07-19 16:39:54 -0600 |
| commit | 86c78db45fad37209663bf87547a50a880760051 (patch) | |
| tree | afb65ae7053e5fe34b5ab7b306c26011ffa393a6 /Source/Core/BoogiePL.atg | |
| parent | 59052004251c655e06951eb4615938259fdf4844 (diff) | |
fixed an issue with parsing floating points
Diffstat (limited to 'Source/Core/BoogiePL.atg')
| -rw-r--r-- | Source/Core/BoogiePL.atg | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 31823110..f74f8bff 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -145,7 +145,11 @@ TOKENS decimal = digit {digit} 'e' [ '-' ] digit {digit} . dec_float = digit {digit} '.' digit {digit} [ 'e' [ '-' ] digit {digit} ] . - float = digit {digit} 'e' digit {digit} 'f' digit {digit} 'e' digit {digit} . + float = [ '-' ] digit {digit} 'e' [ '-' ] digit {digit} 'f' digit {digit} 'e' digit {digit} + | '0' 'N' 'a' 'N' digit {digit} 'e' digit {digit} + | '0' 'n' 'a' 'n' digit {digit} 'e' digit {digit} + | '0' '+' 'o' 'o' digit {digit} 'e' digit {digit} + | '0' '-' 'o' 'o' digit {digit} 'e' digit {digit} . COMMENTS FROM "/*" TO "*/" NESTED COMMENTS FROM "//" TO lf @@ -1292,7 +1296,7 @@ AtomExpression<out Expr/*!*/ e> Expression<out e> ")" (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List<Expr>{ e }); .) - | "(" ( Expression<out e> (. if (e is BvBounds) + | "(" ( Expression<out e> (. if (e is BvBounds) this.SemErr("parentheses around bitvector bounds " + "are not allowed"); .) | Forall (. x = t; .) @@ -1518,8 +1522,8 @@ Float<out BigFloat n> ) (. try { n = BigFloat.FromString(s); - } catch (FormatException) { - this.SemErr("incorrectly formatted number"); + } catch (FormatException e) { + this.SemErr("incorrectly formatted floating point, " + e.Message); n = BigFloat.ZERO; } .) |