diff options
Diffstat (limited to 'Source/Core/BoogiePL.atg')
-rw-r--r-- | Source/Core/BoogiePL.atg | 25 |
1 files changed, 21 insertions, 4 deletions
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 091ceeb0..31823110 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -144,7 +144,8 @@ TOKENS string = quote { regularStringChar | "\\\"" } quote. decimal = digit {digit} 'e' [ '-' ] digit {digit} . - float = digit {digit} '.' 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} . COMMENTS FROM "/*" TO "*/" NESTED COMMENTS FROM "//" TO lf @@ -330,7 +331,7 @@ TypeAtom<out Bpl.Type/*!*/ ty> ( "int" (. ty = new BasicType(t, SimpleType.Int); .) | "real" (. ty = new BasicType(t, SimpleType.Real); .) | "bool" (. ty = new BasicType(t, SimpleType.Bool); .) - /* note: bitvectors are handled in UnresolvedTypeIdentifier */ + /* note: bitvectors and floats are handled in UnresolvedTypeIdentifier */ | "(" Type<out ty> @@ -1252,7 +1253,7 @@ ArrayExpression<out Expr/*!*/ e> /*------------------------------------------------------------------------*/ AtomExpression<out Expr/*!*/ e> -= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; += (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; BigFloat bf; List<Expr>/*!*/ es; List<Variable>/*!*/ ds; Trigger trig; List<TypeVariable>/*!*/ typeParams; IdentifierExpr/*!*/ id; @@ -1265,6 +1266,7 @@ AtomExpression<out Expr/*!*/ e> | "true" (. e = new LiteralExpr(t, true); .) | Nat<out bn> (. e = new LiteralExpr(t, bn); .) | Dec<out bd> (. e = new LiteralExpr(t, bd); .) + | Float<out bf> (. e = new LiteralExpr(t, bf); .) | BvLit<out bn, out n> (. e = new LiteralExpr(t, bn, n); .) | Ident<out x> (. id = new IdentifierExpr(x, x.val); e = id; .) @@ -1479,7 +1481,7 @@ Dec<out BigDec n> ( decimal (. s = t.val; .) | - float (. s = t.val; .) + dec_float (. s = t.val; .) ) (. try { n = BigDec.FromString(s); @@ -1508,4 +1510,19 @@ BvLit<out BigNum n, out int m> } .) . + +Float<out BigFloat n> += (. string s = ""; .) + ( + float (. s = t.val; .) + ) + (. try { + n = BigFloat.FromString(s); + } catch (FormatException) { + this.SemErr("incorrectly formatted number"); + n = BigFloat.ZERO; + } + .) + . + END BoogiePL. |