summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/AbsInt/IntervalDomain.cs6
-rw-r--r--Source/Basetypes/BigFloat.cs982
-rw-r--r--Source/Core/AbsyExpr.cs12
-rw-r--r--Source/Core/AbsyType.cs8
-rw-r--r--Source/Core/BoogiePL.atg25
-rw-r--r--Source/Core/Parser.cs889
-rw-r--r--Source/Core/Scanner.cs385
-rw-r--r--Test/floats/float0.bpl8
-rw-r--r--Test/floats/float1.bpl24
9 files changed, 1213 insertions, 1126 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index 9d37476f..1d35b735 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -695,10 +695,10 @@ namespace Microsoft.Boogie.AbstractInterpretation
Lo = floor;
Hi = ceiling;
} else if (node.Val is BigFloat) {
- BigNum floor, ceiling;
+ BigInteger floor, ceiling;
((BigFloat)node.Val).FloorCeiling(out floor, out ceiling);
- Lo = floor.ToBigInteger;
- Hi = ceiling.ToBigInteger;
+ Lo = floor;
+ Hi = ceiling;
} else if (node.Val is bool) {
if ((bool)node.Val) {
// true
diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs
index 3c4cc40a..5f711e70 100644
--- a/Source/Basetypes/BigFloat.cs
+++ b/Source/Basetypes/BigFloat.cs
@@ -1,475 +1,507 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using System.Diagnostics.Contracts;
-using System.Diagnostics;
-
-namespace Microsoft.Basetypes
-{
- using BIM = System.Numerics.BigInteger;
-
- /// <summary>
- /// A representation of a 32-bit floating point value
- /// Note that this value has a 1-bit sign, 8-bit exponent, and 24-bit significand
- /// </summary>
- public struct BigFloat
- {
- //Please note that this code outline is copy-pasted from BigDec.cs
-
- // the internal representation
- [Rep]
- internal readonly BigNum significand; //Note that the significand arrangement matches standard fp arrangement (most significant bit is farthest left)
- [Rep]
- internal readonly int significandSize;
- [Rep]
- internal readonly BigNum exponent; //The value of the exponent is always positive as per fp representation requirements
- [Rep]
- internal readonly int exponentSize; //The bit size of the exponent
- [Rep]
- internal readonly String value; //Only used with second syntax
- [Rep]
- internal readonly bool isNeg;
-
- public BigNum Significand {
- get {
- return significand;
- }
- }
-
- public BigNum Exponent {
- get {
- return exponent;
- }
- }
-
- public int SignificandSize {
- get {
- return significandSize;
- }
- }
-
- public int ExponentSize {
- get {
- return exponentSize;
- }
- }
-
- public bool IsNegative {
- get {
- return this.isNeg;
- }
- }
-
- public String Value {
- get {
- return value;
- }
- }
-
- public static BigFloat ZERO(int exponentSize, int significandSize) { return new BigFloat(false, BigNum.ZERO, BigNum.ZERO, exponentSize, significandSize); } //Does not include negative zero
-
- private static readonly BigNum two = new BigNum(2);
- private static readonly BigNum one = new BigNum(1);
- private static BigNum two_n(int n) {
- BigNum toReturn = one;
- for (int i = 0; i < n; i++)
- toReturn = toReturn * two;
- return toReturn;
- }
-
-
- ////////////////////////////////////////////////////////////////////////////
- // Constructors
-
- //Please note that these constructors will be called throughout boogie
- //For a complete summary of where this class has been added, simply view constructor references
-
- [Pure]
- public static BigFloat FromInt(int v) {
- return new BigFloat(v.ToString(), 8, 24);
- }
-
- public static BigFloat FromInt(int v, int exponentSize, int significandSize)
- {
- return new BigFloat(v.ToString(), exponentSize, significandSize);
- }
-
- public static BigFloat FromBigInt(BIM v) {
- return new BigFloat(v.ToString(), 8, 24);
- }
-
- public static BigFloat FromBigInt(BIM v, int exponentSize, int significandSize)
- {
- return new BigFloat(v.ToString(), exponentSize, significandSize);
- }
-
- public static BigFloat FromBigDec(BigDec v)
- {
- return new BigFloat(v.ToDecimalString(), 8, 24);
- }
-
- public static BigFloat FromBigDec(BigDec v, int exponentSize, int significandSize)
- {
- return new BigFloat(v.ToDecimalString(), exponentSize, significandSize);
- }
-
- [Pure]
- public static BigFloat FromString(String v, int exp, int sig) { //String must be
- return new BigFloat(v, exp, sig);
- }
-
- public BigFloat(bool sign, BigNum exponent, BigNum significand, int exponentSize, int significandSize) {
- this.exponentSize = exponentSize;
- this.exponent = exponent;
- this.significand = significand;
- this.significandSize = significandSize+1;
- this.isNeg = sign;
- this.value = "";
- }
-
- public BigFloat(String value, int exponentSize, int significandSize) {
- this.exponentSize = exponentSize;
- this.significandSize = significandSize;
- this.exponent = BigNum.ZERO;
- this.significand = BigNum.ZERO;
- this.value = value;
- this.isNeg = value[0] == '-';
- }
-
- private BigNum maxsignificand()
- {
- BigNum result = one;
- for (int i = 0; i < significandSize; i++)
- result = result * two;
- return result - one;
- }
- private int maxExponent() { return (int)Math.Pow(2, exponentSize) - 1; }
-
-
-
- ////////////////////////////////////////////////////////////////////////////
- // Basic object operations
-
- [Pure]
- [Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj) {
- if (obj == null)
- return false;
- if (!(obj is BigFloat))
- return false;
-
- return (this == (BigFloat)obj);
- }
-
- [Pure]
- public override int GetHashCode() {
- return significand.GetHashCode() * 13 + Exponent.GetHashCode();
- }
-
- [Pure]
- public override string/*!*/ ToString() {
- Contract.Ensures(Contract.Result<string>() != null);
- return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value;
- }
-
-
- ////////////////////////////////////////////////////////////////////////////
- // Conversion operations
-
- /// <summary>
- /// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!!
- /// Converts the given decimal value (provided as a string) to the nearest floating point approximation
- /// the returned fp assumes the given significand and exponent size
- /// </summary>
- /// <param name="value"></param>
- /// <param name="significandSize"></param>
- /// <param name="exponentSize"></param>
- /// <returns></returns>
- public static BigFloat Round(String value, int exponentSize, int significandSize)
- {
- int i = value.IndexOf('.');
- if (i == -1)
- return Round(BigNum.FromString(value), BigNum.ZERO, exponentSize, significandSize);
- return Round(i == 0 ? BigNum.ZERO : BigNum.FromString(value.Substring(0, i)), BigNum.FromString(value.Substring(i + 1, value.Length - i - 1)), exponentSize, significandSize);
- }
-
- /// <summary>
- /// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!!!
- /// Converts value.dec_value to a the closest float approximation with the given significandSize, exponentSize
- /// Returns the result of this calculation
- /// </summary>
- /// <param name="value"></param>
- /// <param name="power"></param>
- /// <param name="significandSize"></param>
- /// <param name="exponentSize"></param>
- /// <returns></returns>
- public static BigFloat Round(BigNum value, BigNum dec_value, int exponentSize, int significandSize)
- {
- int exp = 0;
- BigNum one = new BigNum(1);
- BigNum ten = new BigNum(10);
- BigNum dec_max = new BigNum(0); //represents the order of magnitude of dec_value for carrying during calculations
-
- //First, determine the exponent
- while (value > one) { //Divide by two, increment exponent by 1
- if (!(value % two).IsZero) { //Add "1.0" to the decimal
- dec_max = new BigNum(10);
- while (dec_max < dec_value)
- dec_max = dec_max * ten;
- dec_value = dec_value + dec_max;
- }
- value = value / two;
- if (!(dec_value % ten).IsZero)
- dec_value = dec_value * ten; //Creates excess zeroes to avoid losing data during division
- dec_value = dec_value / two;
- exp++;
- }
- if (value.IsZero && !dec_value.IsZero) {
- dec_max = new BigNum(10);
- while (dec_max < dec_value)
- dec_max = dec_max * ten;
- while (value.IsZero) {//Multiply by two, decrement exponent by 1
- dec_value = dec_value * two;
- if (dec_value >= dec_max) {
- dec_value = dec_value - dec_max;
- value = value + one;
- }
- exp--;
- }
- }
-
- //Second, calculate the significand
- value = new BigNum(0); //remove implicit bit
- dec_max = new BigNum(10);
- while (dec_max < dec_value)
- dec_max = dec_max * ten;
- for (int i = significandSize; i > 0 && !dec_value.IsZero; i--) { //Multiply by two until the significand is fully calculated
- dec_value = dec_value * two;
- if (dec_value >= dec_max) {
- dec_value = dec_value - dec_max;
- value = value + two_n(i); //Note that i is decrementing so that the most significant bit is left-most in the representation
- }
- }
-
- return new BigFloat(false, BigNum.ZERO, BigNum.FromString(value.ToString()), exponentSize, significandSize); //Sign not actually checked...
- }
-
- // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int).
- /// <summary>
- /// NOTE: THIS PROBABLY WON'T GIVE USEFUL OUTPUT!!!
- /// Computes the floor and ceiling of this BigFloat. Note the choice of rounding towards negative
- /// infinity rather than zero for floor is because SMT-LIBv2's to_int function floors this way.
- /// </summary>
- /// <param name="floor">The Floor (rounded towards negative infinity)</param>
- /// <param name="ceiling">Ceiling (rounded towards positive infinity)</param>
- public void FloorCeiling(out BigNum floor, out BigNum ceiling) {
- //TODO: fix for fp functionality
- BigNum n = Significand;
- BigNum e = Exponent;
- if (n.IsZero) {
- floor = ceiling = n;
- } else if (BigNum.ZERO <= e) {
- // it's an integer
- for (; BigNum.ZERO < e; e = e - one)
- {
- n = n * two;
- }
- floor = ceiling = n;
- } else {
- // it's a non-zero integer, so the ceiling is one more than the floor
- for (; BigNum.ZERO < e && !n.IsZero; e = e + one)
- {
- n = n / two; // Division rounds towards negative infinity
- }
-
- if (!IsNegative) {
- floor = n;
- ceiling = n + one;
- } else {
- ceiling = n;
- floor = n - one;
- }
- }
- Debug.Assert(floor <= ceiling, "Invariant was not maintained");
- }
-
- [Pure]
- public String ToDecimalString(int maxDigits) {
- //TODO: fix for fp functionality
- {
- throw new NotImplementedException();
- }
- }
-
- public String ToBVString(){
- if (this.IsSpecialType) {
- return "_ " + this.value + " " + this.exponentSize + " " + this.significandSize;
- }
- else if (this.Value == "") {
- return "fp (_ bv" + (this.isNeg ? "1" : "0") + " 1) (_ bv" + this.exponent + " " + this.exponentSize + ") (_ bv" + this.significand + " " + (this.significandSize-1) + ")";
- }
- else {
- return "(_ to_fp " + this.exponentSize + " " + this.significandSize + ") (_ bv" + this.value + " " + (this.exponentSize + this.significandSize).ToString() + ")";
- }
- }
-
- [Pure]
- public string ToDecimalString() {
- Contract.Ensures(Contract.Result<string>() != null);
- return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value;
- }
-
- [Pure]
- public static string Zeros(int n) {
- //TODO: fix for fp functionality
- Contract.Requires(0 <= n);
- if (n <= 10) {
- var tenZeros = "0000000000";
- return tenZeros.Substring(0, n);
- } else {
- var d = n / 2;
- var s = Zeros(d);
- if (n % 2 == 0) {
- return s + s;
- } else {
- return s + s + "0";
- }
- }
- }
-
-
- ////////////////////////////////////////////////////////////////////////////
- // Basic arithmetic operations
-
- [Pure]
- public BigFloat Abs {
- get {
- return new BigFloat(true, Exponent, Significand, ExponentSize, SignificandSize);
- }
- }
-
- [Pure]
- public BigFloat Negate {
- get {
- if (value != "")
- return value[0] == '-' ? new BigFloat(value.Remove(0, 1), ExponentSize, significandSize) : new BigFloat("-" + value, ExponentSize, significandSize);
- return new BigFloat(!isNeg, Exponent, Significand, ExponentSize, SignificandSize);
- }
- }
-
- [Pure]
- public static BigFloat operator -(BigFloat x) {
- return x.Negate;
- }
-
- [Pure]
- public static BigFloat operator +(BigFloat x, BigFloat y) {
- //TODO: Modify for correct fp functionality
- Contract.Requires(x.ExponentSize == y.ExponentSize);
- Contract.Requires(x.significandSize == y.significandSize);
- BigNum m1 = x.significand;
- BigNum e1 = x.Exponent;
- BigNum m2 = y.significand;
- BigNum e2 = y.Exponent;
- m1 = m1 + two_n(x.significandSize + 1); //Add implicit bit
- m2 = m2 + two_n(y.significandSize + 1);
- if (e2 > e1) {
- m1 = y.significand;
- e1 = y.Exponent;
- m2 = x.significand;
- e2 = x.Exponent;
- }
-
- while (e2 < e1) {
- m2 = m2 / two;
- e2 = e2 + one;
- }
-
- return new BigFloat(false, e1, m1 + m2, x.significandSize, x.ExponentSize);
- }
-
- [Pure]
- public static BigFloat operator -(BigFloat x, BigFloat y) {
- return x + y.Negate;
- }
-
- [Pure]
- public static BigFloat operator *(BigFloat x, BigFloat y) {
- Contract.Requires(x.ExponentSize == y.ExponentSize);
- Contract.Requires(x.significandSize == y.significandSize);
- return new BigFloat(x.isNeg ^ y.isNeg, x.Exponent + y.Exponent, x.significand * y.significand, x.significandSize, x.ExponentSize);
- }
-
-
- ////////////////////////////////////////////////////////////////////////////
- // Some basic comparison operations
-
- public bool IsSpecialType {
- get {
- if (value == "")
- return false;
- return (value.Equals("NaN") || value.Equals("+oo") || value.Equals("-oo") || value.Equals("zero") || value.Equals("-zero"));
- }
- }
-
- public bool IsPositive {
- get {
- return !IsNegative;
- }
- }
-
- public bool IsZero {
- get {
- return significand.Equals(BigNum.ZERO) && Exponent == BigNum.ZERO;
- }
- }
-
- [Pure]
- public int CompareTo(BigFloat that) {
- if (this.exponent > that.exponent)
- return 1;
- if (this.exponent < that.exponent)
- return -1;
- if (this.significand == that.significand)
- return 0;
- return this.significand > that.significand ? 1 : -1;
- }
-
- [Pure]
- public static bool operator ==(BigFloat x, BigFloat y) {
- return x.CompareTo(y) == 0;
- }
-
- [Pure]
- public static bool operator !=(BigFloat x, BigFloat y) {
- return x.CompareTo(y) != 0;
- }
-
- [Pure]
- public static bool operator <(BigFloat x, BigFloat y) {
- return x.CompareTo(y) < 0;
- }
-
- [Pure]
- public static bool operator >(BigFloat x, BigFloat y) {
- return x.CompareTo(y) > 0;
- }
-
- [Pure]
- public static bool operator <=(BigFloat x, BigFloat y) {
- return x.CompareTo(y) <= 0;
- }
-
- [Pure]
- public static bool operator >=(BigFloat x, BigFloat y) {
- return x.CompareTo(y) >= 0;
- }
- }
-}
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics.Contracts;
+using System.Diagnostics;
+
+namespace Microsoft.Basetypes
+{
+ using BIM = System.Numerics.BigInteger;
+
+ /// <summary>
+ /// A representation of a 32-bit floating point value
+ /// Note that this value has a 1-bit sign, 8-bit exponent, and 24-bit significand
+ /// </summary>
+ public struct BigFloat
+ {
+ //Please note that this code outline is copy-pasted from BigDec.cs
+
+ // the internal representation
+ [Rep]
+ internal readonly BIM significand; //Note that the significand arrangement matches standard fp arrangement (most significant bit is farthest left)
+ [Rep]
+ internal readonly int significandSize;
+ [Rep]
+ internal readonly BIM exponent; //The value of the exponent is always positive as per fp representation requirements
+ [Rep]
+ internal readonly int exponentSize; //The bit size of the exponent
+ [Rep]
+ internal readonly String value; //Only used with second syntax
+ [Rep]
+ internal readonly bool isNeg;
+
+ public BIM Significand {
+ get {
+ return significand;
+ }
+ }
+
+ public BIM Exponent {
+ get {
+ return exponent;
+ }
+ }
+
+ public int SignificandSize {
+ get {
+ return significandSize;
+ }
+ }
+
+ public int ExponentSize {
+ get {
+ return exponentSize;
+ }
+ }
+
+ public bool IsNegative {
+ get {
+ return this.isNeg;
+ }
+ }
+
+ public String Value {
+ get {
+ return value;
+ }
+ }
+
+ public static BigFloat ZERO = new BigFloat(false, BIM.Zero, BIM.Zero, 24, 8); //Does not include negative zero
+
+ private static readonly BIM two = new BIM(2);
+ private static readonly BIM one = new BIM(1);
+ private static BIM two_n(int n) {
+ BIM toReturn = one;
+ for (int i = 0; i < n; i++)
+ toReturn = toReturn * two;
+ return toReturn;
+ }
+
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Constructors
+
+ //Please note that these constructors will be called throughout boogie
+ //For a complete summary of where this class has been added, simply view constructor references
+
+ [Pure]
+ public static BigFloat FromInt(int v) {
+ return new BigFloat(v.ToString(), 24, 8);
+ }
+
+ public static BigFloat FromInt(int v, int significandSize, int exponentSize)
+ {
+ return new BigFloat(v.ToString(), significandSize, exponentSize);
+ }
+
+ public static BigFloat FromBigInt(BIM v) {
+ return new BigFloat(v.ToString(), 24, 8);
+ }
+
+ public static BigFloat FromBigInt(BIM v, int significandSize, int exponentSize)
+ {
+ return new BigFloat(v.ToString(), significandSize, exponentSize);
+ }
+
+ public static BigFloat FromBigDec(BigDec v)
+ {
+ return new BigFloat(v.ToDecimalString(), 24, 8);
+ }
+
+ public static BigFloat FromBigDec(BigDec v, int significandSize, int exponentSize)
+ {
+ return new BigFloat(v.ToDecimalString(), significandSize, exponentSize);
+ }
+
+ [Pure]
+ public static BigFloat FromString(String s) {
+ /*
+ * String must be either of the format *e*f*e*
+ * or of the special value formats: 0NaN*e* 0nan*e* 0+oo*e* 0-oo*e*
+ * Where * indicates an integer value (digit)
+ */
+ BIM sig, exp;
+ int sigSize, expSize;
+ bool isNeg;
+
+ if (s.IndexOf('f') == -1) {
+ String val = s;
+ sigSize = int.Parse(s.Substring(4, s.IndexOf('e')-4));
+ expSize = int.Parse(s.Substring(s.IndexOf('e') + 1));
+ if (sigSize <= 0 || expSize <= 0)
+ throw new FormatException("Significand and Exponent sizes must be greater than 0");
+ return new BigFloat(val, sigSize, expSize);
+ }
+
+ sig = BIM.Parse(s.Substring(0, s.IndexOf('e')));
+ exp = BIM.Parse(s.Substring(s.IndexOf('e') + 1, s.IndexOf('f') - s.IndexOf('e') - 1));
+ sigSize = int.Parse(s.Substring(s.IndexOf('f') + 1, s.IndexOf('e', s.IndexOf('e') + 1) - s.IndexOf('f') - 1));
+ expSize = int.Parse(s.Substring(s.IndexOf('e', s.IndexOf('e') + 1) + 1));
+
+ if (sigSize <= 0 || expSize <= 0)
+ throw new FormatException("Significand and Exponent sizes must be greater than 0");
+
+ sigSize = sigSize - 1; //Get rid of sign bit
+ isNeg = sig < 0;
+ sig = BIM.Abs(sig);
+ exp = exp + BIM.Pow(new BIM(2), expSize-1) - BIM.One;
+
+ if (exp < 0 || exp >= BIM.Pow(new BIM(2), expSize))
+ throw new FormatException("The given exponent " + exp + " cannot fit in the bit size " + expSize);
+
+ if (sig >= BIM.Pow(new BIM(2), sigSize))
+ throw new FormatException("The given significand " + sig + " cannot fit in the bit size " + (sigSize+1));
+
+ return new BigFloat(isNeg, sig, exp, sigSize, expSize);
+ }
+
+ public BigFloat(bool isNeg, BIM significand, BIM exponent, int significandSize, int exponentSize) {
+ this.exponentSize = exponentSize;
+ this.exponent = exponent;
+ this.significand = significand;
+ this.significandSize = significandSize+1;
+ this.isNeg = isNeg;
+ this.value = "";
+ }
+
+ public BigFloat(String value, int significandSize, int exponentSize) {
+ this.exponentSize = exponentSize;
+ this.significandSize = significandSize;
+ this.exponent = BIM.Zero;
+ this.significand = BIM.Zero;
+ this.value = value;
+ if (value.Equals("nan"))
+ this.value = "NaN";
+ this.isNeg = value[0] == '-';
+ }
+
+ private BIM maxsignificand()
+ {
+ BIM result = one;
+ for (int i = 0; i < significandSize; i++)
+ result = result * two;
+ return result - one;
+ }
+ private int maxExponent() { return (int)Math.Pow(2, exponentSize) - 1; }
+
+
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Basic object operations
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj) {
+ if (obj == null)
+ return false;
+ if (!(obj is BigFloat))
+ return false;
+
+ return (this == (BigFloat)obj);
+ }
+
+ [Pure]
+ public override int GetHashCode() {
+ return significand.GetHashCode() * 13 + Exponent.GetHashCode();
+ }
+
+ [Pure]
+ public override string/*!*/ ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value;
+ }
+
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Conversion operations
+
+ /// <summary>
+ /// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!!
+ /// Converts the given decimal value (provided as a string) to the nearest floating point approximation
+ /// the returned fp assumes the given significand and exponent size
+ /// </summary>
+ /// <param name="value"></param>
+ /// <param name="significandSize"></param>
+ /// <param name="exponentSize"></param>
+ /// <returns></returns>
+ public static BigFloat Round(String value, int exponentSize, int significandSize)
+ {
+ int i = value.IndexOf('.');
+ if (i == -1)
+ return Round(BIM.Parse(value), BIM.Zero, exponentSize, significandSize);
+ return Round(i == 0 ? BIM.Zero : BIM.Parse(value.Substring(0, i)), BIM.Parse(value.Substring(i + 1, value.Length - i - 1)), exponentSize, significandSize);
+ }
+
+ /// <summary>
+ /// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!!!
+ /// Converts value.dec_value to a the closest float approximation with the given significandSize, exponentSize
+ /// Returns the result of this calculation
+ /// </summary>
+ /// <param name="value"></param>
+ /// <param name="power"></param>
+ /// <param name="significandSize"></param>
+ /// <param name="exponentSize"></param>
+ /// <returns></returns>
+ public static BigFloat Round(BIM value, BIM dec_value, int exponentSize, int significandSize)
+ {
+ int exp = 0;
+ BIM one = new BIM(1);
+ BIM ten = new BIM(10);
+ BIM dec_max = new BIM(0); //represents the order of magnitude of dec_value for carrying during calculations
+
+ //First, determine the exponent
+ while (value > one) { //Divide by two, increment exponent by 1
+ if (!(value % two).IsZero) { //Add "1.0" to the decimal
+ dec_max = new BIM(10);
+ while (dec_max < dec_value)
+ dec_max = dec_max * ten;
+ dec_value = dec_value + dec_max;
+ }
+ value = value / two;
+ if (!(dec_value % ten).IsZero)
+ dec_value = dec_value * ten; //Creates excess zeroes to avoid losing data during division
+ dec_value = dec_value / two;
+ exp++;
+ }
+ if (value.IsZero && !dec_value.IsZero) {
+ dec_max = new BIM(10);
+ while (dec_max < dec_value)
+ dec_max = dec_max * ten;
+ while (value.IsZero) {//Multiply by two, decrement exponent by 1
+ dec_value = dec_value * two;
+ if (dec_value >= dec_max) {
+ dec_value = dec_value - dec_max;
+ value = value + one;
+ }
+ exp--;
+ }
+ }
+
+ //Second, calculate the significand
+ value = new BIM(0); //remove implicit bit
+ dec_max = new BIM(10);
+ while (dec_max < dec_value)
+ dec_max = dec_max * ten;
+ for (int i = significandSize; i > 0 && !dec_value.IsZero; i--) { //Multiply by two until the significand is fully calculated
+ dec_value = dec_value * two;
+ if (dec_value >= dec_max) {
+ dec_value = dec_value - dec_max;
+ value = value + two_n(i); //Note that i is decrementing so that the most significant bit is left-most in the representation
+ }
+ }
+
+ return new BigFloat(false, BIM.Zero, BIM.Parse(value.ToString()), exponentSize, significandSize); //Sign not actually checked...
+ }
+
+ // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int).
+ /// <summary>
+ /// NOTE: This may give wrong results, it hasn't been tested extensively
+ /// If you're getting weird bugs, you may want to check this function out...
+ /// Computes the floor and ceiling of this BigFloat. Note the choice of rounding towards negative
+ /// infinity rather than zero for floor is because SMT-LIBv2's to_int function floors this way.
+ /// </summary>
+ /// <param name="floor">The Floor (rounded towards negative infinity)</param>
+ /// <param name="ceiling">Ceiling (rounded towards positive infinity)</param>
+ public void FloorCeiling(out BIM floor, out BIM ceiling)
+ {
+ BIM two = new BIM(2);
+
+ BIM sig = Significand + BIM.Pow(two, SignificandSize); //Add hidden bit
+ BIM exp = Exponent - BIM.Pow(two, ExponentSize);
+ sig = sig >> ExponentSize;
+
+ while (exp > BIM.Zero) {
+ exp--;
+ sig = sig >> 1;
+ }
+
+ if (isNeg) {
+ ceiling = -sig + 1;
+ floor = -sig;
+ }
+ else {
+ ceiling = sig + 1;
+ floor = sig;
+ }
+ }
+
+ [Pure]
+ public String ToDecimalString(int maxDigits) {
+ //TODO: fix for fp functionality
+ {
+ throw new NotImplementedException();
+ }
+ }
+
+ public String ToBVString(){
+ if (this.IsSpecialType) {
+ return "_ " + this.value + " " + this.exponentSize + " " + this.significandSize;
+ }
+ else if (this.Value == "") {
+ return "fp (_ bv" + (this.isNeg ? "1" : "0") + " 1) (_ bv" + this.exponent + " " + this.exponentSize + ") (_ bv" + this.significand + " " + (this.significandSize-1) + ")";
+ }
+ else {
+ return "(_ to_fp " + this.exponentSize + " " + this.significandSize + ") (_ bv" + this.value + " " + (this.exponentSize + this.significandSize).ToString() + ")";
+ }
+ }
+
+ [Pure]
+ public string ToDecimalString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value;
+ }
+
+ [Pure]
+ public static string Zeros(int n) {
+ //TODO: fix for fp functionality
+ Contract.Requires(0 <= n);
+ if (n <= 10) {
+ var tenZeros = "0000000000";
+ return tenZeros.Substring(0, n);
+ } else {
+ var d = n / 2;
+ var s = Zeros(d);
+ if (n % 2 == 0) {
+ return s + s;
+ } else {
+ return s + s + "0";
+ }
+ }
+ }
+
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Basic arithmetic operations
+
+ [Pure]
+ public BigFloat Abs {
+ get {
+ return new BigFloat(true, Exponent, Significand, ExponentSize, SignificandSize);
+ }
+ }
+
+ [Pure]
+ public BigFloat Negate {
+ get {
+ if (value != "")
+ return value[0] == '-' ? new BigFloat(value.Remove(0, 1), ExponentSize, significandSize) : new BigFloat("-" + value, ExponentSize, significandSize);
+ return new BigFloat(!isNeg, Exponent, Significand, ExponentSize, SignificandSize);
+ }
+ }
+
+ [Pure]
+ public static BigFloat operator -(BigFloat x) {
+ return x.Negate;
+ }
+
+ [Pure]
+ public static BigFloat operator +(BigFloat x, BigFloat y) {
+ //TODO: Modify for correct fp functionality
+ Contract.Requires(x.ExponentSize == y.ExponentSize);
+ Contract.Requires(x.significandSize == y.significandSize);
+ BIM m1 = x.significand;
+ BIM e1 = x.Exponent;
+ BIM m2 = y.significand;
+ BIM e2 = y.Exponent;
+ m1 = m1 + two_n(x.significandSize + 1); //Add implicit bit
+ m2 = m2 + two_n(y.significandSize + 1);
+ if (e2 > e1) {
+ m1 = y.significand;
+ e1 = y.Exponent;
+ m2 = x.significand;
+ e2 = x.Exponent;
+ }
+
+ while (e2 < e1) {
+ m2 = m2 / two;
+ e2 = e2 + one;
+ }
+
+ return new BigFloat(false, e1, m1 + m2, x.significandSize, x.ExponentSize);
+ }
+
+ [Pure]
+ public static BigFloat operator -(BigFloat x, BigFloat y) {
+ return x + y.Negate;
+ }
+
+ [Pure]
+ public static BigFloat operator *(BigFloat x, BigFloat y) {
+ Contract.Requires(x.ExponentSize == y.ExponentSize);
+ Contract.Requires(x.significandSize == y.significandSize);
+ return new BigFloat(x.isNeg ^ y.isNeg, x.Exponent + y.Exponent, x.significand * y.significand, x.significandSize, x.ExponentSize);
+ }
+
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Some basic comparison operations
+
+ public bool IsSpecialType {
+ get {
+ if (value == "")
+ return false;
+ return (value.Equals("NaN") || value.Equals("+oo") || value.Equals("-oo") || value.Equals("zero") || value.Equals("-zero"));
+ }
+ }
+
+ public bool IsPositive {
+ get {
+ return !IsNegative;
+ }
+ }
+
+ public bool IsZero {
+ get {
+ return significand.Equals(BigNum.ZERO) && Exponent == BIM.Zero;
+ }
+ }
+
+ [Pure]
+ public int CompareTo(BigFloat that) {
+ if (this.exponent > that.exponent)
+ return 1;
+ if (this.exponent < that.exponent)
+ return -1;
+ if (this.significand == that.significand)
+ return 0;
+ return this.significand > that.significand ? 1 : -1;
+ }
+
+ [Pure]
+ public static bool operator ==(BigFloat x, BigFloat y) {
+ return x.CompareTo(y) == 0;
+ }
+
+ [Pure]
+ public static bool operator !=(BigFloat x, BigFloat y) {
+ return x.CompareTo(y) != 0;
+ }
+
+ [Pure]
+ public static bool operator <(BigFloat x, BigFloat y) {
+ return x.CompareTo(y) < 0;
+ }
+
+ [Pure]
+ public static bool operator >(BigFloat x, BigFloat y) {
+ return x.CompareTo(y) > 0;
+ }
+
+ [Pure]
+ public static bool operator <=(BigFloat x, BigFloat y) {
+ return x.CompareTo(y) <= 0;
+ }
+
+ [Pure]
+ public static bool operator >=(BigFloat x, BigFloat y) {
+ return x.CompareTo(y) >= 0;
+ }
+ }
+}
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index bc2b4391..409254d0 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -584,7 +584,7 @@ namespace Microsoft.Boogie {
{
Contract.Requires(tok != null);
Val = v;
- Type = Type.GetFloatType(v.ExponentSize, v.SignificandSize);
+ Type = Type.GetFloatType(v.SignificandSize, v.ExponentSize);
if (immutable)
CachedHashCode = ComputeHashCode();
}
@@ -662,7 +662,7 @@ namespace Microsoft.Boogie {
return Type.Real;
} else if (Val is BigFloat) {
BigFloat temp = (BigFloat)Val;
- return Type.GetFloatType(temp.ExponentSize, temp.SignificandSize);
+ return Type.GetFloatType(temp.SignificandSize, temp.ExponentSize);
} else if (Val is BvConst) {
return Type.GetBvType(((BvConst)Val).Bits);
} else {
@@ -1724,10 +1724,10 @@ namespace Microsoft.Boogie {
return Type.Real;
}
if (arg0type.IsFloat && arg0type.Unify(arg1type)) {
- return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatSignificand);
+ return Type.GetFloatType(arg0.Type.FloatSignificand, arg0.Type.FloatExponent);
}
if (arg1type.IsFloat && arg1type.Unify(arg0type)) {
- return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatSignificand);
+ return Type.GetFloatType(arg1.Type.FloatSignificand, arg1.Type.FloatExponent);
}
goto BAD_TYPE;
case Opcode.Div:
@@ -1742,10 +1742,10 @@ namespace Microsoft.Boogie {
return Type.Real;
}
if (arg0type.IsFloat && arg0type.Unify(arg1type)) {
- return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatSignificand);
+ return Type.GetFloatType(arg0.Type.FloatSignificand, arg0.Type.FloatExponent);
}
if (arg1type.IsFloat && arg1type.Unify(arg0type)) {
- return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatSignificand);
+ return Type.GetFloatType(arg1.Type.FloatSignificand, arg1.Type.FloatExponent);
}
goto BAD_TYPE;
case Opcode.Pow:
diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index 08cf37cc..ab6ef5e9 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -386,12 +386,12 @@ namespace Microsoft.Boogie {
}
}
- static public FloatType GetFloatType(int exp, int man) {
+ static public FloatType GetFloatType(int sig, int exp) {
Contract.Requires(0 <= exp);
- Contract.Requires(0 <= man);
+ Contract.Requires(0 <= sig);
Contract.Ensures(Contract.Result<FloatType>() != null);
- return new FloatType(exp, man);
+ return new FloatType(sig, exp);
}
//------------ Match formal argument types on actual argument types
@@ -1094,7 +1094,7 @@ namespace Microsoft.Boogie {
public override string ToString()
{
Contract.Ensures(Contract.Result<string>() != null);
- return "float (" + Exponent + " " + Significand + ")";
+ return "float" + Significand + "e" + Exponent;
}
//----------- Equality ----------------------------------
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.
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 78823b61..a5e2921e 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -23,8 +23,9 @@ public class Parser {
public const int _digits = 3;
public const int _string = 4;
public const int _decimal = 5;
- public const int _float = 6;
- public const int maxT = 96;
+ public const int _dec_float = 6;
+ public const int _float = 7;
+ public const int maxT = 97;
const bool T = true;
const bool x = false;
@@ -117,7 +118,7 @@ private class BvBounds : Expr {
public BigNum Lower;
public BigNum Upper;
public BvBounds(IToken/*!*/ tok, BigNum lower, BigNum upper)
- : base(tok, /*immutable*/ false) {
+ : base(tok, /*immutable=*/ false) {
Contract.Requires(tok != null);
this.Lower = lower;
this.Upper = upper;
@@ -132,8 +133,7 @@ private class BvBounds : Expr {
Contract.Assert(false);throw new cce.UnreachableException();
}
public override void ComputeFreeVariables(GSet<object>/*!*/ freeVars) { Contract.Assert(false);throw new cce.UnreachableException(); }
- public override int ComputeHashCode()
- {
+ public override int ComputeHashCode() {
return base.GetHashCode();
}
}
@@ -220,7 +220,7 @@ private class BvBounds : Expr {
while (StartOf(1)) {
switch (la.kind) {
- case 21: {
+ case 22: {
Consts(out vs);
foreach(Bpl.Variable/*!*/ v in vs){
Contract.Assert(v != null);
@@ -229,7 +229,7 @@ private class BvBounds : Expr {
break;
}
- case 25: {
+ case 26: {
Function(out ds);
foreach(Bpl.Declaration/*!*/ d in ds){
Contract.Assert(d != null);
@@ -238,12 +238,12 @@ private class BvBounds : Expr {
break;
}
- case 29: {
+ case 30: {
Axiom(out ax);
Pgm.AddTopLevelDeclaration(ax);
break;
}
- case 30: {
+ case 31: {
UserDefinedTypes(out ts);
foreach(Declaration/*!*/ td in ts){
Contract.Assert(td != null);
@@ -252,7 +252,7 @@ private class BvBounds : Expr {
break;
}
- case 7: {
+ case 8: {
GlobalVars(out vs);
foreach(Bpl.Variable/*!*/ v in vs){
Contract.Assert(v != null);
@@ -261,7 +261,7 @@ private class BvBounds : Expr {
break;
}
- case 32: {
+ case 33: {
Procedure(out pr, out im);
Pgm.AddTopLevelDeclaration(pr);
if (im != null) {
@@ -270,7 +270,7 @@ private class BvBounds : Expr {
break;
}
- case 33: {
+ case 34: {
Implementation(out nnim);
Pgm.AddTopLevelDeclaration(nnim);
break;
@@ -286,17 +286,17 @@ private class BvBounds : Expr {
bool u = false; QKeyValue kv = null;
bool ChildrenComplete = false;
List<ConstantParent/*!*/> Parents = null;
- Expect(21);
+ Expect(22);
y = t;
- while (la.kind == 27) {
+ while (la.kind == 28) {
Attribute(ref kv);
}
- if (la.kind == 22) {
+ if (la.kind == 23) {
Get();
u = true;
}
IdsType(out xs);
- if (la.kind == 23) {
+ if (la.kind == 24) {
OrderSpec(out ChildrenComplete, out Parents);
}
bool makeClone = false;
@@ -320,7 +320,7 @@ private class BvBounds : Expr {
ds.Add(new Constant(y, x, u, ParentsClone, ChildrenComplete, kv));
}
- Expect(8);
+ Expect(9);
}
void Function(out List<Declaration>/*!*/ ds) {
@@ -337,44 +337,44 @@ private class BvBounds : Expr {
Expr definition = null;
Expr/*!*/ tmp;
- Expect(25);
- while (la.kind == 27) {
+ Expect(26);
+ while (la.kind == 28) {
Attribute(ref kv);
}
Ident(out z);
- if (la.kind == 19) {
+ if (la.kind == 20) {
TypeParams(out typeParamTok, out typeParams);
}
- Expect(9);
+ Expect(10);
if (StartOf(2)) {
VarOrType(out tyd, out argKv);
arguments.Add(new Formal(tyd.tok, tyd, true, argKv));
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
VarOrType(out tyd, out argKv);
arguments.Add(new Formal(tyd.tok, tyd, true, argKv));
}
}
- Expect(10);
+ Expect(11);
argKv = null;
- if (la.kind == 26) {
+ if (la.kind == 27) {
Get();
- Expect(9);
- VarOrType(out retTyd, out argKv);
Expect(10);
- } else if (la.kind == 11) {
+ VarOrType(out retTyd, out argKv);
+ Expect(11);
+ } else if (la.kind == 12) {
Get();
Type(out retTy);
retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy);
- } else SynErr(97);
- if (la.kind == 27) {
+ } else SynErr(98);
+ if (la.kind == 28) {
Get();
Expression(out tmp);
definition = tmp;
- Expect(28);
- } else if (la.kind == 8) {
+ Expect(29);
+ } else if (la.kind == 9) {
Get();
- } else SynErr(98);
+ } else SynErr(99);
if (retTyd == null) {
// construct a dummy type for the case of syntax error
retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int));
@@ -429,30 +429,30 @@ private class BvBounds : Expr {
void Axiom(out Axiom/*!*/ m) {
Contract.Ensures(Contract.ValueAtReturn(out m) != null); Expr/*!*/ e; QKeyValue kv = null;
- Expect(29);
- while (la.kind == 27) {
+ Expect(30);
+ while (la.kind == 28) {
Attribute(ref kv);
}
IToken/*!*/ x = t;
Proposition(out e);
- Expect(8);
+ Expect(9);
m = new Axiom(x,e, null, kv);
}
void UserDefinedTypes(out List<Declaration/*!*/>/*!*/ ts) {
Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out ts))); Declaration/*!*/ decl; QKeyValue kv = null; ts = new List<Declaration/*!*/> ();
- Expect(30);
- while (la.kind == 27) {
+ Expect(31);
+ while (la.kind == 28) {
Attribute(ref kv);
}
UserDefinedType(out decl, kv);
ts.Add(decl);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
UserDefinedType(out decl, kv);
ts.Add(decl);
}
- Expect(8);
+ Expect(9);
}
void GlobalVars(out List<Variable>/*!*/ ds) {
@@ -461,12 +461,12 @@ private class BvBounds : Expr {
ds = new List<Variable>();
var dsx = ds;
- Expect(7);
- while (la.kind == 27) {
+ Expect(8);
+ while (la.kind == 28) {
Attribute(ref kv);
}
IdsTypeWheres(true, "global variables", delegate(TypedIdent tyd) { dsx.Add(new GlobalVariable(tyd.tok, tyd, kv)); } );
- Expect(8);
+ Expect(9);
}
void Procedure(out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl) {
@@ -482,9 +482,9 @@ private class BvBounds : Expr {
QKeyValue kv = null;
impl = null;
- Expect(32);
+ Expect(33);
ProcSignature(true, out x, out typeParams, out ins, out outs, out kv);
- if (la.kind == 8) {
+ if (la.kind == 9) {
Get();
while (StartOf(3)) {
Spec(pre, mods, post);
@@ -497,7 +497,7 @@ private class BvBounds : Expr {
impl = new Implementation(x, x.val, typeParams,
Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
- } else SynErr(99);
+ } else SynErr(100);
proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv);
}
@@ -509,7 +509,7 @@ private class BvBounds : Expr {
StmtList/*!*/ stmtList;
QKeyValue kv;
- Expect(33);
+ Expect(34);
ProcSignature(false, out x, out typeParams, out ins, out outs, out kv);
ImplBody(out locals, out stmtList);
impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors);
@@ -523,7 +523,7 @@ private class BvBounds : Expr {
void IdsTypeWheres(bool allowWhereClauses, string context, System.Action<TypedIdent> action ) {
IdsTypeWhere(allowWhereClauses, context, action);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
IdsTypeWhere(allowWhereClauses, context, action);
}
@@ -533,12 +533,12 @@ private class BvBounds : Expr {
Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
QKeyValue kv = null;
- Expect(7);
- while (la.kind == 27) {
+ Expect(8);
+ while (la.kind == 28) {
Attribute(ref kv);
}
IdsTypeWheres(true, "local variables", delegate(TypedIdent tyd) { ds.Add(new LocalVariable(tyd.tok, tyd, kv)); } );
- Expect(8);
+ Expect(9);
}
void ProcFormals(bool incoming, bool allowWhereClauses, out List<Variable>/*!*/ ds) {
@@ -547,16 +547,16 @@ private class BvBounds : Expr {
var dsx = ds;
var context = allowWhereClauses ? "procedure formals" : "the 'implementation' copies of formals";
- Expect(9);
- if (la.kind == 1 || la.kind == 27) {
+ Expect(10);
+ if (la.kind == 1 || la.kind == 28) {
AttrsIdsTypeWheres(allowWhereClauses, allowWhereClauses, context, delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new Formal(tyd.tok, tyd, incoming, kv)); });
}
- Expect(10);
+ Expect(11);
}
void AttrsIdsTypeWheres(bool allowAttributes, bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action ) {
AttributesIdsTypeWhere(allowAttributes, allowWhereClauses, context, action);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
AttributesIdsTypeWhere(allowAttributes, allowWhereClauses, context, action);
}
@@ -575,7 +575,7 @@ private class BvBounds : Expr {
void IdsType(out List<TypedIdent>/*!*/ tyds) {
Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); List<IToken>/*!*/ ids; Bpl.Type/*!*/ ty;
Idents(out ids);
- Expect(11);
+ Expect(12);
Type(out ty);
tyds = new List<TypedIdent>();
foreach(Token/*!*/ id in ids){
@@ -589,7 +589,7 @@ private class BvBounds : Expr {
Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List<IToken>();
Ident(out id);
xs.Add(id);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
Ident(out id);
xs.Add(id);
@@ -607,14 +607,14 @@ private class BvBounds : Expr {
TypeArgs(args);
}
ty = new UnresolvedTypeIdentifier (tok, tok.val, args);
- } else if (la.kind == 17 || la.kind == 19) {
+ } else if (la.kind == 18 || la.kind == 20) {
MapType(out ty);
- } else SynErr(100);
+ } else SynErr(101);
}
void AttributesIdsTypeWhere(bool allowAttributes, bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action ) {
QKeyValue kv = null;
- while (la.kind == 27) {
+ while (la.kind == 28) {
Attribute(ref kv);
if (!allowAttributes) {
kv = null;
@@ -628,9 +628,9 @@ private class BvBounds : Expr {
void IdsTypeWhere(bool allowWhereClauses, string context, System.Action<TypedIdent> action ) {
List<IToken>/*!*/ ids; Bpl.Type/*!*/ ty; Expr wh = null; Expr/*!*/ nne;
Idents(out ids);
- Expect(11);
+ Expect(12);
Type(out ty);
- if (la.kind == 13) {
+ if (la.kind == 14) {
Get();
Expression(out nne);
if (!allowWhereClauses) {
@@ -650,7 +650,7 @@ private class BvBounds : Expr {
void Expression(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
ImpliesExpression(false, out e0);
- while (la.kind == 55 || la.kind == 56) {
+ while (la.kind == 56 || la.kind == 57) {
EquivOp();
x = t;
ImpliesExpression(false, out e1);
@@ -660,20 +660,20 @@ private class BvBounds : Expr {
void TypeAtom(out Bpl.Type/*!*/ ty) {
Contract.Ensures(Contract.ValueAtReturn(out ty) != null); ty = dummyType;
- if (la.kind == 14) {
+ if (la.kind == 15) {
Get();
ty = new BasicType(t, SimpleType.Int);
- } else if (la.kind == 15) {
+ } else if (la.kind == 16) {
Get();
ty = new BasicType(t, SimpleType.Real);
- } else if (la.kind == 16) {
+ } else if (la.kind == 17) {
Get();
ty = new BasicType(t, SimpleType.Bool);
- } else if (la.kind == 9) {
+ } else if (la.kind == 10) {
Get();
Type(out ty);
- Expect(10);
- } else SynErr(101);
+ Expect(11);
+ } else SynErr(102);
}
void Ident(out IToken/*!*/ x) {
@@ -700,10 +700,10 @@ private class BvBounds : Expr {
if (StartOf(6)) {
TypeArgs(ts);
}
- } else if (la.kind == 17 || la.kind == 19) {
+ } else if (la.kind == 18 || la.kind == 20) {
MapType(out ty);
ts.Add(ty);
- } else SynErr(102);
+ } else SynErr(103);
}
void MapType(out Bpl.Type/*!*/ ty) {
@@ -713,16 +713,16 @@ private class BvBounds : Expr {
Bpl.Type/*!*/ result;
List<TypeVariable>/*!*/ typeParameters = new List<TypeVariable>();
- if (la.kind == 19) {
+ if (la.kind == 20) {
TypeParams(out nnTok, out typeParameters);
tok = nnTok;
}
- Expect(17);
+ Expect(18);
if (tok == null) tok = t;
if (StartOf(6)) {
Types(arguments);
}
- Expect(18);
+ Expect(19);
Type(out result);
ty = new MapType(tok, typeParameters, arguments, result);
@@ -730,10 +730,10 @@ private class BvBounds : Expr {
void TypeParams(out IToken/*!*/ tok, out List<TypeVariable>/*!*/ typeParams) {
Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); List<IToken>/*!*/ typeParamToks;
- Expect(19);
+ Expect(20);
tok = t;
Idents(out typeParamToks);
- Expect(20);
+ Expect(21);
typeParams = new List<TypeVariable> ();
foreach(Token/*!*/ id in typeParamToks){
Contract.Assert(id != null);
@@ -745,7 +745,7 @@ private class BvBounds : Expr {
Contract.Requires(ts != null); Bpl.Type/*!*/ ty;
Type(out ty);
ts.Add(ty);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
Type(out ty);
ts.Add(ty);
@@ -757,21 +757,21 @@ private class BvBounds : Expr {
Parents = null;
bool u;
IToken/*!*/ parent;
- Expect(23);
+ Expect(24);
Parents = new List<ConstantParent/*!*/> ();
u = false;
- if (la.kind == 1 || la.kind == 22) {
- if (la.kind == 22) {
+ if (la.kind == 1 || la.kind == 23) {
+ if (la.kind == 23) {
Get();
u = true;
}
Ident(out parent);
Parents.Add(new ConstantParent (
new IdentifierExpr(parent, parent.val), u));
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
u = false;
- if (la.kind == 22) {
+ if (la.kind == 23) {
Get();
u = true;
}
@@ -780,7 +780,7 @@ private class BvBounds : Expr {
new IdentifierExpr(parent, parent.val), u));
}
}
- if (la.kind == 24) {
+ if (la.kind == 25) {
Get();
ChildrenComplete = true;
}
@@ -793,12 +793,12 @@ private class BvBounds : Expr {
IToken/*!*/ tok;
kv = null;
- while (la.kind == 27) {
+ while (la.kind == 28) {
Attribute(ref kv);
}
Type(out ty);
tok = ty.tok;
- if (la.kind == 11) {
+ if (la.kind == 12) {
Get();
var uti = ty as UnresolvedTypeIdentifier;
if (uti != null && uti.Arguments.Count == 0) {
@@ -824,7 +824,7 @@ private class BvBounds : Expr {
if (la.kind == 1) {
WhiteSpaceIdents(out paramTokens);
}
- if (la.kind == 31) {
+ if (la.kind == 32) {
Get();
Type(out body);
synonym = true;
@@ -856,15 +856,15 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
Contract.Ensures(Contract.ValueAtReturn(out name) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); Contract.Ensures(Contract.ValueAtReturn(out ins) != null); Contract.Ensures(Contract.ValueAtReturn(out outs) != null);
IToken/*!*/ typeParamTok; typeParams = new List<TypeVariable>();
outs = new List<Variable>(); kv = null;
- while (la.kind == 27) {
+ while (la.kind == 28) {
Attribute(ref kv);
}
Ident(out name);
- if (la.kind == 19) {
+ if (la.kind == 20) {
TypeParams(out typeParamTok, out typeParams);
}
ProcFormals(true, allowWhereClausesOnFormals, out ins);
- if (la.kind == 26) {
+ if (la.kind == 27) {
Get();
ProcFormals(false, allowWhereClausesOnFormals, out outs);
}
@@ -872,7 +872,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
void Spec(List<Requires>/*!*/ pre, List<IdentifierExpr>/*!*/ mods, List<Ensures>/*!*/ post) {
Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); List<IToken>/*!*/ ms;
- if (la.kind == 34) {
+ if (la.kind == 35) {
Get();
if (la.kind == 1) {
Idents(out ms);
@@ -882,19 +882,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
}
}
- Expect(8);
- } else if (la.kind == 35) {
+ Expect(9);
+ } else if (la.kind == 36) {
Get();
SpecPrePost(true, pre, post);
- } else if (la.kind == 36 || la.kind == 37) {
+ } else if (la.kind == 37 || la.kind == 38) {
SpecPrePost(false, pre, post);
- } else SynErr(103);
+ } else SynErr(104);
}
void ImplBody(out List<Variable>/*!*/ locals, out StmtList/*!*/ stmtList) {
Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); locals = new List<Variable>();
- Expect(27);
- while (la.kind == 7) {
+ Expect(28);
+ while (la.kind == 8) {
LocalVars(locals);
}
StmtList(out stmtList);
@@ -902,25 +902,25 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
void SpecPrePost(bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post) {
Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null;
- if (la.kind == 36) {
+ if (la.kind == 37) {
Get();
tok = t;
- while (la.kind == 27) {
+ while (la.kind == 28) {
Attribute(ref kv);
}
Proposition(out e);
- Expect(8);
+ Expect(9);
pre.Add(new Requires(tok, free, e, null, kv));
- } else if (la.kind == 37) {
+ } else if (la.kind == 38) {
Get();
tok = t;
- while (la.kind == 27) {
+ while (la.kind == 28) {
Attribute(ref kv);
}
Proposition(out e);
- Expect(8);
+ Expect(9);
post.Add(new Ensures(tok, free, e, null, kv));
- } else SynErr(104);
+ } else SynErr(105);
}
void StmtList(out StmtList/*!*/ stmtList) {
@@ -957,7 +957,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
cs = new List<Cmd>();
}
- } else if (la.kind == 40 || la.kind == 42 || la.kind == 45) {
+ } else if (la.kind == 41 || la.kind == 43 || la.kind == 46) {
StructuredCmd(out ecn);
ec = ecn;
if (startToken == null) { startToken = ec.tok; cs = new List<Cmd>(); }
@@ -977,7 +977,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
}
}
- Expect(28);
+ Expect(29);
IToken/*!*/ endCurly = t;
if (startToken == null && bigblocks.Count == 0) {
startToken = t; cs = new List<Cmd>();
@@ -1005,33 +1005,33 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
LabelOrAssign(out c, out label);
break;
}
- case 46: {
+ case 47: {
Get();
x = t;
- while (la.kind == 27) {
+ while (la.kind == 28) {
Attribute(ref kv);
}
Proposition(out e);
c = new AssertCmd(x, e, kv);
- Expect(8);
+ Expect(9);
break;
}
- case 47: {
+ case 48: {
Get();
x = t;
- while (la.kind == 27) {
+ while (la.kind == 28) {
Attribute(ref kv);
}
Proposition(out e);
c = new AssumeCmd(x, e, kv);
- Expect(8);
+ Expect(9);
break;
}
- case 48: {
+ case 49: {
Get();
x = t;
Idents(out xs);
- Expect(8);
+ Expect(9);
ids = new List<IdentifierExpr>();
foreach(IToken/*!*/ y in xs){
Contract.Assert(y != null);
@@ -1041,25 +1041,25 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
break;
}
- case 35: case 51: case 52: {
+ case 36: case 52: case 53: {
CallCmd(out cn);
- Expect(8);
+ Expect(9);
c = cn;
break;
}
- case 53: {
+ case 54: {
ParCallCmd(out cn);
c = cn;
break;
}
- case 49: {
+ case 50: {
Get();
x = t;
- Expect(8);
+ Expect(9);
c = new YieldCmd(x);
break;
}
- default: SynErr(105); break;
+ default: SynErr(106); break;
}
}
@@ -1067,16 +1067,16 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
Contract.Ensures(Contract.ValueAtReturn(out ec) != null); ec = dummyStructuredCmd; Contract.Assume(cce.IsPeerConsistent(ec));
IfCmd/*!*/ ifcmd; WhileCmd/*!*/ wcmd; BreakCmd/*!*/ bcmd;
- if (la.kind == 40) {
+ if (la.kind == 41) {
IfCmd(out ifcmd);
ec = ifcmd;
- } else if (la.kind == 42) {
+ } else if (la.kind == 43) {
WhileCmd(out wcmd);
ec = wcmd;
- } else if (la.kind == 45) {
+ } else if (la.kind == 46) {
BreakCmd(out bcmd);
ec = bcmd;
- } else SynErr(106);
+ } else SynErr(107);
}
void TransferCmd(out TransferCmd/*!*/ tc) {
@@ -1084,7 +1084,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
Token y; List<IToken>/*!*/ xs;
List<String> ss = new List<String>();
- if (la.kind == 38) {
+ if (la.kind == 39) {
Get();
y = t;
Idents(out xs);
@@ -1093,11 +1093,11 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
ss.Add(s.val); }
tc = new GotoCmd(y, ss);
- } else if (la.kind == 39) {
+ } else if (la.kind == 40) {
Get();
tc = new ReturnCmd(t);
- } else SynErr(107);
- Expect(8);
+ } else SynErr(108);
+ Expect(9);
}
void IfCmd(out IfCmd/*!*/ ifcmd) {
@@ -1107,21 +1107,21 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
IfCmd/*!*/ elseIf; IfCmd elseIfOption = null;
StmtList/*!*/ els; StmtList elseOption = null;
- Expect(40);
+ Expect(41);
x = t;
Guard(out guard);
- Expect(27);
+ Expect(28);
StmtList(out thn);
- if (la.kind == 41) {
+ if (la.kind == 42) {
Get();
- if (la.kind == 40) {
+ if (la.kind == 41) {
IfCmd(out elseIf);
elseIfOption = elseIf;
- } else if (la.kind == 27) {
+ } else if (la.kind == 28) {
Get();
StmtList(out els);
elseOption = els;
- } else SynErr(108);
+ } else SynErr(109);
}
ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption);
}
@@ -1133,18 +1133,18 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
StmtList/*!*/ body;
QKeyValue kv = null;
- Expect(42);
+ Expect(43);
x = t;
Guard(out guard);
Contract.Assume(guard == null || cce.Owner.None(guard));
- while (la.kind == 35 || la.kind == 43) {
+ while (la.kind == 36 || la.kind == 44) {
isFree = false; z = la/*lookahead token*/;
- if (la.kind == 35) {
+ if (la.kind == 36) {
Get();
isFree = true;
}
- Expect(43);
- while (la.kind == 27) {
+ Expect(44);
+ while (la.kind == 28) {
Attribute(ref kv);
}
Expression(out e);
@@ -1155,9 +1155,9 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
}
kv = null;
- Expect(8);
+ Expect(9);
}
- Expect(27);
+ Expect(28);
StmtList(out body);
wcmd = new WhileCmd(x, guard, invariants, body);
}
@@ -1166,27 +1166,27 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
Contract.Ensures(Contract.ValueAtReturn(out bcmd) != null); IToken/*!*/ x; IToken/*!*/ y;
string breakLabel = null;
- Expect(45);
+ Expect(46);
x = t;
if (la.kind == 1) {
Ident(out y);
breakLabel = y.val;
}
- Expect(8);
+ Expect(9);
bcmd = new BreakCmd(x, breakLabel);
}
void Guard(out Expr e) {
Expr/*!*/ ee; e = null;
- Expect(9);
- if (la.kind == 44) {
+ Expect(10);
+ if (la.kind == 45) {
Get();
e = null;
} else if (StartOf(9)) {
Expression(out ee);
e = ee;
- } else SynErr(109);
- Expect(10);
+ } else SynErr(110);
+ Expect(11);
}
void LabelOrAssign(out Cmd c, out IToken label) {
@@ -1199,40 +1199,40 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
Ident(out id);
x = t;
- if (la.kind == 11) {
+ if (la.kind == 12) {
Get();
c = null; label = x;
- } else if (la.kind == 12 || la.kind == 17 || la.kind == 50) {
+ } else if (la.kind == 13 || la.kind == 18 || la.kind == 51) {
lhss = new List<AssignLhs/*!*/>();
lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val));
- while (la.kind == 17) {
+ while (la.kind == 18) {
MapAssignIndex(out y, out indexes);
lhs = new MapAssignLhs(y, lhs, indexes);
}
lhss.Add(lhs);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
Ident(out id);
lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val));
- while (la.kind == 17) {
+ while (la.kind == 18) {
MapAssignIndex(out y, out indexes);
lhs = new MapAssignLhs(y, lhs, indexes);
}
lhss.Add(lhs);
}
- Expect(50);
+ Expect(51);
x = t; /* use location of := */
Expression(out e0);
rhss = new List<Expr/*!*/> ();
rhss.Add(e0);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
Expression(out e0);
rhss.Add(e0);
}
- Expect(8);
+ Expect(9);
c = new AssignCmd(x, lhss, rhss);
- } else SynErr(110);
+ } else SynErr(111);
}
void CallCmd(out Cmd c) {
@@ -1243,17 +1243,17 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
QKeyValue kv = null;
c = null;
- if (la.kind == 51) {
+ if (la.kind == 52) {
Get();
isAsync = true;
}
- if (la.kind == 35) {
+ if (la.kind == 36) {
Get();
isFree = true;
}
- Expect(52);
+ Expect(53);
x = t;
- while (la.kind == 27) {
+ while (la.kind == 28) {
Attribute(ref kv);
}
CallParams(isAsync, isFree, kv, x, out c);
@@ -1267,19 +1267,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
Cmd c = null;
List<CallCmd> callCmds = new List<CallCmd>();
- Expect(53);
+ Expect(54);
x = t;
- while (la.kind == 27) {
+ while (la.kind == 28) {
Attribute(ref kv);
}
CallParams(false, false, kv, x, out c);
callCmds.Add((CallCmd)c);
- while (la.kind == 54) {
+ while (la.kind == 55) {
Get();
CallParams(false, false, kv, x, out c);
callCmds.Add((CallCmd)c);
}
- Expect(8);
+ Expect(9);
d = new ParCallCmd(x, callCmds, kv);
}
@@ -1287,18 +1287,18 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out indexes))); indexes = new List<Expr/*!*/> ();
Expr/*!*/ e;
- Expect(17);
+ Expect(18);
x = t;
if (StartOf(9)) {
Expression(out e);
indexes.Add(e);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
Expression(out e);
indexes.Add(e);
}
}
- Expect(18);
+ Expect(19);
}
void CallParams(bool isAsync, bool isFree, QKeyValue kv, IToken x, out Cmd c) {
@@ -1310,53 +1310,53 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
c = null;
Ident(out first);
- if (la.kind == 9) {
+ if (la.kind == 10) {
Get();
if (StartOf(9)) {
Expression(out en);
es.Add(en);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
Expression(out en);
es.Add(en);
}
}
- Expect(10);
+ Expect(11);
c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync;
- } else if (la.kind == 12 || la.kind == 50) {
+ } else if (la.kind == 13 || la.kind == 51) {
ids.Add(new IdentifierExpr(first, first.val));
- if (la.kind == 12) {
+ if (la.kind == 13) {
Get();
Ident(out p);
ids.Add(new IdentifierExpr(p, p.val));
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
Ident(out p);
ids.Add(new IdentifierExpr(p, p.val));
}
}
- Expect(50);
+ Expect(51);
Ident(out first);
- Expect(9);
+ Expect(10);
if (StartOf(9)) {
Expression(out en);
es.Add(en);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
Expression(out en);
es.Add(en);
}
}
- Expect(10);
+ Expect(11);
c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync;
- } else SynErr(111);
+ } else SynErr(112);
}
void Expressions(out List<Expr>/*!*/ es) {
Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new List<Expr>();
Expression(out e);
es.Add(e);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
Expression(out e);
es.Add(e);
@@ -1367,7 +1367,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
LogicalExpression(out e0);
if (StartOf(10)) {
- if (la.kind == 57 || la.kind == 58) {
+ if (la.kind == 58 || la.kind == 59) {
ImpliesOp();
x = t;
ImpliesExpression(true, out e1);
@@ -1379,7 +1379,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
x = t;
LogicalExpression(out e1);
e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0);
- while (la.kind == 59 || la.kind == 60) {
+ while (la.kind == 60 || la.kind == 61) {
ExpliesOp();
x = t;
LogicalExpression(out e1);
@@ -1390,23 +1390,23 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
}
void EquivOp() {
- if (la.kind == 55) {
+ if (la.kind == 56) {
Get();
- } else if (la.kind == 56) {
+ } else if (la.kind == 57) {
Get();
- } else SynErr(112);
+ } else SynErr(113);
}
void LogicalExpression(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
RelationalExpression(out e0);
if (StartOf(11)) {
- if (la.kind == 61 || la.kind == 62) {
+ if (la.kind == 62 || la.kind == 63) {
AndOp();
x = t;
RelationalExpression(out e1);
e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1);
- while (la.kind == 61 || la.kind == 62) {
+ while (la.kind == 62 || la.kind == 63) {
AndOp();
x = t;
RelationalExpression(out e1);
@@ -1417,7 +1417,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
x = t;
RelationalExpression(out e1);
e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1);
- while (la.kind == 63 || la.kind == 64) {
+ while (la.kind == 64 || la.kind == 65) {
OrOp();
x = t;
RelationalExpression(out e1);
@@ -1428,19 +1428,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
}
void ImpliesOp() {
- if (la.kind == 57) {
+ if (la.kind == 58) {
Get();
- } else if (la.kind == 58) {
+ } else if (la.kind == 59) {
Get();
- } else SynErr(113);
+ } else SynErr(114);
}
void ExpliesOp() {
- if (la.kind == 59) {
+ if (la.kind == 60) {
Get();
- } else if (la.kind == 60) {
+ } else if (la.kind == 61) {
Get();
- } else SynErr(114);
+ } else SynErr(115);
}
void RelationalExpression(out Expr/*!*/ e0) {
@@ -1454,25 +1454,25 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
}
void AndOp() {
- if (la.kind == 61) {
+ if (la.kind == 62) {
Get();
- } else if (la.kind == 62) {
+ } else if (la.kind == 63) {
Get();
- } else SynErr(115);
+ } else SynErr(116);
}
void OrOp() {
- if (la.kind == 63) {
+ if (la.kind == 64) {
Get();
- } else if (la.kind == 64) {
+ } else if (la.kind == 65) {
Get();
- } else SynErr(116);
+ } else SynErr(117);
}
void BvTerm(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
Term(out e0);
- while (la.kind == 73) {
+ while (la.kind == 74) {
Get();
x = t;
Term(out e1);
@@ -1483,64 +1483,64 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
void RelOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
switch (la.kind) {
- case 65: {
+ case 66: {
Get();
x = t; op=BinaryOperator.Opcode.Eq;
break;
}
- case 19: {
+ case 20: {
Get();
x = t; op=BinaryOperator.Opcode.Lt;
break;
}
- case 20: {
+ case 21: {
Get();
x = t; op=BinaryOperator.Opcode.Gt;
break;
}
- case 66: {
+ case 67: {
Get();
x = t; op=BinaryOperator.Opcode.Le;
break;
}
- case 67: {
+ case 68: {
Get();
x = t; op=BinaryOperator.Opcode.Ge;
break;
}
- case 68: {
+ case 69: {
Get();
x = t; op=BinaryOperator.Opcode.Neq;
break;
}
- case 69: {
+ case 70: {
Get();
x = t; op=BinaryOperator.Opcode.Subtype;
break;
}
- case 70: {
+ case 71: {
Get();
x = t; op=BinaryOperator.Opcode.Neq;
break;
}
- case 71: {
+ case 72: {
Get();
x = t; op=BinaryOperator.Opcode.Le;
break;
}
- case 72: {
+ case 73: {
Get();
x = t; op=BinaryOperator.Opcode.Ge;
break;
}
- default: SynErr(117); break;
+ default: SynErr(118); break;
}
}
void Term(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op;
Factor(out e0);
- while (la.kind == 74 || la.kind == 75) {
+ while (la.kind == 75 || la.kind == 76) {
AddOp(out x, out op);
Factor(out e1);
e0 = Expr.Binary(x, op, e0, e1);
@@ -1559,19 +1559,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
void AddOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
- if (la.kind == 74) {
+ if (la.kind == 75) {
Get();
x = t; op=BinaryOperator.Opcode.Add;
- } else if (la.kind == 75) {
+ } else if (la.kind == 76) {
Get();
x = t; op=BinaryOperator.Opcode.Sub;
- } else SynErr(118);
+ } else SynErr(119);
}
void Power(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
UnaryExpression(out e0);
- if (la.kind == 79) {
+ if (la.kind == 80) {
Get();
x = t;
Power(out e1);
@@ -1581,46 +1581,46 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
void MulOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
- if (la.kind == 44) {
+ if (la.kind == 45) {
Get();
x = t; op=BinaryOperator.Opcode.Mul;
- } else if (la.kind == 76) {
+ } else if (la.kind == 77) {
Get();
x = t; op=BinaryOperator.Opcode.Div;
- } else if (la.kind == 77) {
+ } else if (la.kind == 78) {
Get();
x = t; op=BinaryOperator.Opcode.Mod;
- } else if (la.kind == 78) {
+ } else if (la.kind == 79) {
Get();
x = t; op=BinaryOperator.Opcode.RealDiv;
- } else SynErr(119);
+ } else SynErr(120);
}
void UnaryExpression(out Expr/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
e = dummyExpr;
- if (la.kind == 75) {
+ if (la.kind == 76) {
Get();
x = t;
UnaryExpression(out e);
e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e);
- } else if (la.kind == 80 || la.kind == 81) {
+ } else if (la.kind == 81 || la.kind == 82) {
NegOp();
x = t;
UnaryExpression(out e);
e = Expr.Unary(x, UnaryOperator.Opcode.Not, e);
} else if (StartOf(14)) {
CoercionExpression(out e);
- } else SynErr(120);
+ } else SynErr(121);
}
void NegOp() {
- if (la.kind == 80) {
+ if (la.kind == 81) {
Get();
- } else if (la.kind == 81) {
+ } else if (la.kind == 82) {
Get();
- } else SynErr(121);
+ } else SynErr(122);
}
void CoercionExpression(out Expr/*!*/ e) {
@@ -1629,7 +1629,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
BigNum bn;
ArrayExpression(out e);
- while (la.kind == 11) {
+ while (la.kind == 12) {
Get();
x = t;
if (StartOf(6)) {
@@ -1644,7 +1644,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);
}
- } else SynErr(122);
+ } else SynErr(123);
}
}
@@ -1655,7 +1655,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
List<Expr>/*!*/ allArgs = dummyExprSeq;
AtomExpression(out e);
- while (la.kind == 17) {
+ while (la.kind == 18) {
Get();
x = t; allArgs = new List<Expr> ();
allArgs.Add(e);
@@ -1668,7 +1668,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
else
allArgs.Add(index0);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
Expression(out e1);
if (bvExtract || e1 is BvBounds)
@@ -1676,7 +1676,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
allArgs.Add(e1);
}
- if (la.kind == 50) {
+ if (la.kind == 51) {
Get();
Expression(out e1);
if (bvExtract || e1 is BvBounds)
@@ -1690,7 +1690,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
allArgs.Add(e1); store = true;
}
}
- Expect(18);
+ Expect(19);
if (store)
e = new NAryExpr(x, new MapStore(x, allArgs.Count - 2), allArgs);
else if (bvExtract)
@@ -1715,7 +1715,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
}
void 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;
@@ -1725,12 +1725,12 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
List<Block/*!*/>/*!*/ blocks;
switch (la.kind) {
- case 82: {
+ case 83: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 83: {
+ case 84: {
Get();
e = new LiteralExpr(t, true);
break;
@@ -1745,6 +1745,11 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
e = new LiteralExpr(t, bd);
break;
}
+ case 7: {
+ Float(out bf);
+ e = new LiteralExpr(t, bf);
+ break;
+ }
case 2: {
BvLit(out bn, out n);
e = new LiteralExpr(t, bn, n);
@@ -1753,65 +1758,65 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
case 1: {
Ident(out x);
id = new IdentifierExpr(x, x.val); e = id;
- if (la.kind == 9) {
+ if (la.kind == 10) {
Get();
if (StartOf(9)) {
Expressions(out es);
e = new NAryExpr(x, new FunctionCall(id), es);
- } else if (la.kind == 10) {
+ } else if (la.kind == 11) {
e = new NAryExpr(x, new FunctionCall(id), new List<Expr>());
- } else SynErr(123);
- Expect(10);
+ } else SynErr(124);
+ Expect(11);
}
break;
}
- case 84: {
+ case 85: {
Get();
x = t;
- Expect(9);
- Expression(out e);
Expect(10);
+ Expression(out e);
+ Expect(11);
e = new OldExpr(x, e);
break;
}
- case 14: {
+ case 15: {
Get();
x = t;
- Expect(9);
- Expression(out e);
Expect(10);
+ Expression(out e);
+ Expect(11);
e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new List<Expr>{ e });
break;
}
- case 15: {
+ case 16: {
Get();
x = t;
- Expect(9);
- Expression(out e);
Expect(10);
+ Expression(out e);
+ Expect(11);
e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List<Expr>{ e });
break;
}
- case 9: {
+ case 10: {
Get();
if (StartOf(9)) {
Expression(out e);
if (e is BvBounds)
this.SemErr("parentheses around bitvector bounds " +
"are not allowed");
- } else if (la.kind == 88 || la.kind == 89) {
+ } else if (la.kind == 89 || la.kind == 90) {
Forall();
x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
if (typeParams.Count + ds.Count > 0)
e = new ForallExpr(x, typeParams, ds, kv, trig, e);
- } else if (la.kind == 90 || la.kind == 91) {
+ } else if (la.kind == 91 || la.kind == 92) {
Exists();
x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
if (typeParams.Count + ds.Count > 0)
e = new ExistsExpr(x, typeParams, ds, kv, trig, e);
- } else if (la.kind == 92 || la.kind == 93) {
+ } else if (la.kind == 93 || la.kind == 94) {
Lambda();
x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
@@ -1819,20 +1824,20 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
SemErr("triggers not allowed in lambda expressions");
if (typeParams.Count + ds.Count > 0)
e = new LambdaExpr(x, typeParams, ds, kv, e);
- } else SynErr(124);
- Expect(10);
+ } else SynErr(125);
+ Expect(11);
break;
}
- case 40: {
+ case 41: {
IfThenElseExpression(out e);
break;
}
- case 85: {
+ case 86: {
CodeExpression(out locals, out blocks);
e = new CodeExpr(locals, blocks);
break;
}
- default: SynErr(125); break;
+ default: SynErr(126); break;
}
}
@@ -1844,7 +1849,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
} else if (la.kind == 6) {
Get();
s = t.val;
- } else SynErr(126);
+ } else SynErr(127);
try {
n = BigDec.FromString(s);
} catch (FormatException) {
@@ -1854,6 +1859,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
}
+ void Float(out BigFloat n) {
+ string s = "";
+ Expect(7);
+ s = t.val;
+ try {
+ n = BigFloat.FromString(s);
+ } catch (FormatException e) {
+ this.SemErr("incorrectly formatted floating point: " + e.Message);
+ n = BigFloat.ZERO;
+ }
+
+ }
+
void BvLit(out BigNum n, out int m) {
Expect(2);
int pos = t.val.IndexOf("bv");
@@ -1871,11 +1889,11 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
}
void Forall() {
- if (la.kind == 88) {
+ if (la.kind == 89) {
Get();
- } else if (la.kind == 89) {
+ } else if (la.kind == 90) {
Get();
- } else SynErr(127);
+ } else SynErr(128);
}
void QuantifierBody(IToken/*!*/ q, out List<TypeVariable>/*!*/ typeParams, out List<Variable>/*!*/ ds,
@@ -1886,35 +1904,35 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
kv = null;
ds = new List<Variable> ();
- if (la.kind == 19) {
+ if (la.kind == 20) {
TypeParams(out tok, out typeParams);
- if (la.kind == 1 || la.kind == 27) {
+ if (la.kind == 1 || la.kind == 28) {
BoundVars(q, out ds);
}
- } else if (la.kind == 1 || la.kind == 27) {
+ } else if (la.kind == 1 || la.kind == 28) {
BoundVars(q, out ds);
- } else SynErr(128);
+ } else SynErr(129);
QSep();
- while (la.kind == 27) {
+ while (la.kind == 28) {
AttributeOrTrigger(ref kv, ref trig);
}
Expression(out body);
}
void Exists() {
- if (la.kind == 90) {
+ if (la.kind == 91) {
Get();
- } else if (la.kind == 91) {
+ } else if (la.kind == 92) {
Get();
- } else SynErr(129);
+ } else SynErr(130);
}
void Lambda() {
- if (la.kind == 92) {
+ if (la.kind == 93) {
Get();
- } else if (la.kind == 93) {
+ } else if (la.kind == 94) {
Get();
- } else SynErr(130);
+ } else SynErr(131);
}
void IfThenElseExpression(out Expr/*!*/ e) {
@@ -1922,12 +1940,12 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
IToken/*!*/ tok;
Expr/*!*/ e0, e1, e2;
e = dummyExpr;
- Expect(40);
+ Expect(41);
tok = t;
Expression(out e0);
- Expect(87);
+ Expect(88);
Expression(out e1);
- Expect(41);
+ Expect(42);
Expression(out e2);
e = new NAryExpr(tok, new IfThenElse(tok), new List<Expr>{ e0, e1, e2 });
}
@@ -1936,8 +1954,8 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new List<Variable>(); Block/*!*/ b;
blocks = new List<Block/*!*/>();
- Expect(85);
- while (la.kind == 7) {
+ Expect(86);
+ while (la.kind == 8) {
LocalVars(locals);
}
SpecBlock(out b);
@@ -1946,7 +1964,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
SpecBlock(out b);
blocks.Add(b);
}
- Expect(86);
+ Expect(87);
}
void SpecBlock(out Block/*!*/ b) {
@@ -1959,7 +1977,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
Expr/*!*/ e;
Ident(out x);
- Expect(11);
+ Expect(12);
while (StartOf(8)) {
LabelOrCmd(out c, out label);
if (c != null) {
@@ -1971,7 +1989,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
}
}
- if (la.kind == 38) {
+ if (la.kind == 39) {
Get();
y = t;
Idents(out xs);
@@ -1980,12 +1998,12 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
ss.Add(s.val); }
b = new Block(x,x.val,cs,new GotoCmd(y,ss));
- } else if (la.kind == 39) {
+ } else if (la.kind == 40) {
Get();
Expression(out e);
b = new Block(x,x.val,cs,new ReturnExprCmd(t,e));
- } else SynErr(131);
- Expect(8);
+ } else SynErr(132);
+ Expect(9);
}
void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {
@@ -1993,16 +2011,16 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
string key;
List<object/*!*/> parameters; object/*!*/ param;
- Expect(27);
+ Expect(28);
tok = t;
- if (la.kind == 11) {
+ if (la.kind == 12) {
Get();
Expect(1);
key = t.val; parameters = new List<object/*!*/>();
if (StartOf(16)) {
AttributeParameter(out param);
parameters.Add(param);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
AttributeParameter(out param);
parameters.Add(param);
@@ -2030,7 +2048,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
} else if (StartOf(9)) {
Expression(out e);
es = new List<Expr> { e };
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
Expression(out e);
es.Add(e);
@@ -2041,8 +2059,8 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
trig.AddLast(new Trigger(tok, true, es, null));
}
- } else SynErr(132);
- Expect(28);
+ } else SynErr(133);
+ Expect(29);
}
void AttributeParameter(out object/*!*/ o) {
@@ -2056,15 +2074,15 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
} else if (StartOf(9)) {
Expression(out e);
o = e;
- } else SynErr(133);
+ } else SynErr(134);
}
void QSep() {
- if (la.kind == 94) {
+ if (la.kind == 95) {
Get();
- } else if (la.kind == 95) {
+ } else if (la.kind == 96) {
Get();
- } else SynErr(134);
+ } else SynErr(135);
}
@@ -2080,23 +2098,23 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
}
static readonly bool[,]/*!*/ set = {
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,x,T,x, x,T,T,T, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,T, T,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x}
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,T,T, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,T,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,T,T,x, T,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,T,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,T,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,T, x,x,T,T, T,T,T,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,T,T,T, x,T,T,T, x,x,T,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,T,T,T, x,T,T,T, x,x,T,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,T,T,T, x,T,T,T, x,x,T,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,T,T,T, T,T,T,T, x,x,T,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x}
};
} // end Parser
@@ -2127,135 +2145,136 @@ public class Errors {
case 3: s = "digits expected"; break;
case 4: s = "string expected"; break;
case 5: s = "decimal expected"; break;
- case 6: s = "float expected"; break;
- case 7: s = "\"var\" expected"; break;
- case 8: s = "\";\" expected"; break;
- case 9: s = "\"(\" expected"; break;
- case 10: s = "\")\" expected"; break;
- case 11: s = "\":\" expected"; break;
- case 12: s = "\",\" expected"; break;
- case 13: s = "\"where\" expected"; break;
- case 14: s = "\"int\" expected"; break;
- case 15: s = "\"real\" expected"; break;
- case 16: s = "\"bool\" expected"; break;
- case 17: s = "\"[\" expected"; break;
- case 18: s = "\"]\" expected"; break;
- case 19: s = "\"<\" expected"; break;
- case 20: s = "\">\" expected"; break;
- case 21: s = "\"const\" expected"; break;
- case 22: s = "\"unique\" expected"; break;
- case 23: s = "\"extends\" expected"; break;
- case 24: s = "\"complete\" expected"; break;
- case 25: s = "\"function\" expected"; break;
- case 26: s = "\"returns\" expected"; break;
- case 27: s = "\"{\" expected"; break;
- case 28: s = "\"}\" expected"; break;
- case 29: s = "\"axiom\" expected"; break;
- case 30: s = "\"type\" expected"; break;
- case 31: s = "\"=\" expected"; break;
- case 32: s = "\"procedure\" expected"; break;
- case 33: s = "\"implementation\" expected"; break;
- case 34: s = "\"modifies\" expected"; break;
- case 35: s = "\"free\" expected"; break;
- case 36: s = "\"requires\" expected"; break;
- case 37: s = "\"ensures\" expected"; break;
- case 38: s = "\"goto\" expected"; break;
- case 39: s = "\"return\" expected"; break;
- case 40: s = "\"if\" expected"; break;
- case 41: s = "\"else\" expected"; break;
- case 42: s = "\"while\" expected"; break;
- case 43: s = "\"invariant\" expected"; break;
- case 44: s = "\"*\" expected"; break;
- case 45: s = "\"break\" expected"; break;
- case 46: s = "\"assert\" expected"; break;
- case 47: s = "\"assume\" expected"; break;
- case 48: s = "\"havoc\" expected"; break;
- case 49: s = "\"yield\" expected"; break;
- case 50: s = "\":=\" expected"; break;
- case 51: s = "\"async\" expected"; break;
- case 52: s = "\"call\" expected"; break;
- case 53: s = "\"par\" expected"; break;
- case 54: s = "\"|\" expected"; break;
- case 55: s = "\"<==>\" expected"; break;
- case 56: s = "\"\\u21d4\" expected"; break;
- case 57: s = "\"==>\" expected"; break;
- case 58: s = "\"\\u21d2\" expected"; break;
- case 59: s = "\"<==\" expected"; break;
- case 60: s = "\"\\u21d0\" expected"; break;
- case 61: s = "\"&&\" expected"; break;
- case 62: s = "\"\\u2227\" expected"; break;
- case 63: s = "\"||\" expected"; break;
- case 64: s = "\"\\u2228\" expected"; break;
- case 65: s = "\"==\" expected"; break;
- case 66: s = "\"<=\" expected"; break;
- case 67: s = "\">=\" expected"; break;
- case 68: s = "\"!=\" expected"; break;
- case 69: s = "\"<:\" expected"; break;
- case 70: s = "\"\\u2260\" expected"; break;
- case 71: s = "\"\\u2264\" expected"; break;
- case 72: s = "\"\\u2265\" expected"; break;
- case 73: s = "\"++\" expected"; break;
- case 74: s = "\"+\" expected"; break;
- case 75: s = "\"-\" expected"; break;
- case 76: s = "\"div\" expected"; break;
- case 77: s = "\"mod\" expected"; break;
- case 78: s = "\"/\" expected"; break;
- case 79: s = "\"**\" expected"; break;
- case 80: s = "\"!\" expected"; break;
- case 81: s = "\"\\u00ac\" expected"; break;
- case 82: s = "\"false\" expected"; break;
- case 83: s = "\"true\" expected"; break;
- case 84: s = "\"old\" expected"; break;
- case 85: s = "\"|{\" expected"; break;
- case 86: s = "\"}|\" expected"; break;
- case 87: s = "\"then\" expected"; break;
- case 88: s = "\"forall\" expected"; break;
- case 89: s = "\"\\u2200\" expected"; break;
- case 90: s = "\"exists\" expected"; break;
- case 91: s = "\"\\u2203\" expected"; break;
- case 92: s = "\"lambda\" expected"; break;
- case 93: s = "\"\\u03bb\" expected"; break;
- case 94: s = "\"::\" expected"; break;
- case 95: s = "\"\\u2022\" expected"; break;
- case 96: s = "??? expected"; break;
- case 97: s = "invalid Function"; break;
+ case 6: s = "dec_float expected"; break;
+ case 7: s = "float expected"; break;
+ case 8: s = "\"var\" expected"; break;
+ case 9: s = "\";\" expected"; break;
+ case 10: s = "\"(\" expected"; break;
+ case 11: s = "\")\" expected"; break;
+ case 12: s = "\":\" expected"; break;
+ case 13: s = "\",\" expected"; break;
+ case 14: s = "\"where\" expected"; break;
+ case 15: s = "\"int\" expected"; break;
+ case 16: s = "\"real\" expected"; break;
+ case 17: s = "\"bool\" expected"; break;
+ case 18: s = "\"[\" expected"; break;
+ case 19: s = "\"]\" expected"; break;
+ case 20: s = "\"<\" expected"; break;
+ case 21: s = "\">\" expected"; break;
+ case 22: s = "\"const\" expected"; break;
+ case 23: s = "\"unique\" expected"; break;
+ case 24: s = "\"extends\" expected"; break;
+ case 25: s = "\"complete\" expected"; break;
+ case 26: s = "\"function\" expected"; break;
+ case 27: s = "\"returns\" expected"; break;
+ case 28: s = "\"{\" expected"; break;
+ case 29: s = "\"}\" expected"; break;
+ case 30: s = "\"axiom\" expected"; break;
+ case 31: s = "\"type\" expected"; break;
+ case 32: s = "\"=\" expected"; break;
+ case 33: s = "\"procedure\" expected"; break;
+ case 34: s = "\"implementation\" expected"; break;
+ case 35: s = "\"modifies\" expected"; break;
+ case 36: s = "\"free\" expected"; break;
+ case 37: s = "\"requires\" expected"; break;
+ case 38: s = "\"ensures\" expected"; break;
+ case 39: s = "\"goto\" expected"; break;
+ case 40: s = "\"return\" expected"; break;
+ case 41: s = "\"if\" expected"; break;
+ case 42: s = "\"else\" expected"; break;
+ case 43: s = "\"while\" expected"; break;
+ case 44: s = "\"invariant\" expected"; break;
+ case 45: s = "\"*\" expected"; break;
+ case 46: s = "\"break\" expected"; break;
+ case 47: s = "\"assert\" expected"; break;
+ case 48: s = "\"assume\" expected"; break;
+ case 49: s = "\"havoc\" expected"; break;
+ case 50: s = "\"yield\" expected"; break;
+ case 51: s = "\":=\" expected"; break;
+ case 52: s = "\"async\" expected"; break;
+ case 53: s = "\"call\" expected"; break;
+ case 54: s = "\"par\" expected"; break;
+ case 55: s = "\"|\" expected"; break;
+ case 56: s = "\"<==>\" expected"; break;
+ case 57: s = "\"\\u21d4\" expected"; break;
+ case 58: s = "\"==>\" expected"; break;
+ case 59: s = "\"\\u21d2\" expected"; break;
+ case 60: s = "\"<==\" expected"; break;
+ case 61: s = "\"\\u21d0\" expected"; break;
+ case 62: s = "\"&&\" expected"; break;
+ case 63: s = "\"\\u2227\" expected"; break;
+ case 64: s = "\"||\" expected"; break;
+ case 65: s = "\"\\u2228\" expected"; break;
+ case 66: s = "\"==\" expected"; break;
+ case 67: s = "\"<=\" expected"; break;
+ case 68: s = "\">=\" expected"; break;
+ case 69: s = "\"!=\" expected"; break;
+ case 70: s = "\"<:\" expected"; break;
+ case 71: s = "\"\\u2260\" expected"; break;
+ case 72: s = "\"\\u2264\" expected"; break;
+ case 73: s = "\"\\u2265\" expected"; break;
+ case 74: s = "\"++\" expected"; break;
+ case 75: s = "\"+\" expected"; break;
+ case 76: s = "\"-\" expected"; break;
+ case 77: s = "\"div\" expected"; break;
+ case 78: s = "\"mod\" expected"; break;
+ case 79: s = "\"/\" expected"; break;
+ case 80: s = "\"**\" expected"; break;
+ case 81: s = "\"!\" expected"; break;
+ case 82: s = "\"\\u00ac\" expected"; break;
+ case 83: s = "\"false\" expected"; break;
+ case 84: s = "\"true\" expected"; break;
+ case 85: s = "\"old\" expected"; break;
+ case 86: s = "\"|{\" expected"; break;
+ case 87: s = "\"}|\" expected"; break;
+ case 88: s = "\"then\" expected"; break;
+ case 89: s = "\"forall\" expected"; break;
+ case 90: s = "\"\\u2200\" expected"; break;
+ case 91: s = "\"exists\" expected"; break;
+ case 92: s = "\"\\u2203\" expected"; break;
+ case 93: s = "\"lambda\" expected"; break;
+ case 94: s = "\"\\u03bb\" expected"; break;
+ case 95: s = "\"::\" expected"; break;
+ case 96: s = "\"\\u2022\" expected"; break;
+ case 97: s = "??? expected"; break;
case 98: s = "invalid Function"; break;
- case 99: s = "invalid Procedure"; break;
- case 100: s = "invalid Type"; break;
- case 101: s = "invalid TypeAtom"; break;
- case 102: s = "invalid TypeArgs"; break;
- case 103: s = "invalid Spec"; break;
- case 104: s = "invalid SpecPrePost"; break;
- case 105: s = "invalid LabelOrCmd"; break;
- case 106: s = "invalid StructuredCmd"; break;
- case 107: s = "invalid TransferCmd"; break;
- case 108: s = "invalid IfCmd"; break;
- case 109: s = "invalid Guard"; break;
- case 110: s = "invalid LabelOrAssign"; break;
- case 111: s = "invalid CallParams"; break;
- case 112: s = "invalid EquivOp"; break;
- case 113: s = "invalid ImpliesOp"; break;
- case 114: s = "invalid ExpliesOp"; break;
- case 115: s = "invalid AndOp"; break;
- case 116: s = "invalid OrOp"; break;
- case 117: s = "invalid RelOp"; break;
- case 118: s = "invalid AddOp"; break;
- case 119: s = "invalid MulOp"; break;
- case 120: s = "invalid UnaryExpression"; break;
- case 121: s = "invalid NegOp"; break;
- case 122: s = "invalid CoercionExpression"; break;
- case 123: s = "invalid AtomExpression"; break;
+ case 99: s = "invalid Function"; break;
+ case 100: s = "invalid Procedure"; break;
+ case 101: s = "invalid Type"; break;
+ case 102: s = "invalid TypeAtom"; break;
+ case 103: s = "invalid TypeArgs"; break;
+ case 104: s = "invalid Spec"; break;
+ case 105: s = "invalid SpecPrePost"; break;
+ case 106: s = "invalid LabelOrCmd"; break;
+ case 107: s = "invalid StructuredCmd"; break;
+ case 108: s = "invalid TransferCmd"; break;
+ case 109: s = "invalid IfCmd"; break;
+ case 110: s = "invalid Guard"; break;
+ case 111: s = "invalid LabelOrAssign"; break;
+ case 112: s = "invalid CallParams"; break;
+ case 113: s = "invalid EquivOp"; break;
+ case 114: s = "invalid ImpliesOp"; break;
+ case 115: s = "invalid ExpliesOp"; break;
+ case 116: s = "invalid AndOp"; break;
+ case 117: s = "invalid OrOp"; break;
+ case 118: s = "invalid RelOp"; break;
+ case 119: s = "invalid AddOp"; break;
+ case 120: s = "invalid MulOp"; break;
+ case 121: s = "invalid UnaryExpression"; break;
+ case 122: s = "invalid NegOp"; break;
+ case 123: s = "invalid CoercionExpression"; break;
case 124: s = "invalid AtomExpression"; break;
case 125: s = "invalid AtomExpression"; break;
- case 126: s = "invalid Dec"; break;
- case 127: s = "invalid Forall"; break;
- case 128: s = "invalid QuantifierBody"; break;
- case 129: s = "invalid Exists"; break;
- case 130: s = "invalid Lambda"; break;
- case 131: s = "invalid SpecBlock"; break;
- case 132: s = "invalid AttributeOrTrigger"; break;
- case 133: s = "invalid AttributeParameter"; break;
- case 134: s = "invalid QSep"; break;
+ case 126: s = "invalid AtomExpression"; break;
+ case 127: s = "invalid Dec"; break;
+ case 128: s = "invalid Forall"; break;
+ case 129: s = "invalid QuantifierBody"; break;
+ case 130: s = "invalid Exists"; break;
+ case 131: s = "invalid Lambda"; break;
+ case 132: s = "invalid SpecBlock"; break;
+ case 133: s = "invalid AttributeOrTrigger"; break;
+ case 134: s = "invalid AttributeParameter"; break;
+ case 135: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index e068fc4b..1185963f 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/Scanner.cs
@@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer {
public class Scanner {
const char EOL = '\n';
const int eofSym = 0; /* pdt */
- const int maxT = 96;
- const int noSym = 96;
+ const int maxT = 97;
+ const int noSym = 97;
[ContractInvariantMethod]
@@ -267,41 +267,41 @@ public class Scanner {
for (int i = 65; i <= 90; ++i) start[i] = 2;
for (int i = 94; i <= 122; ++i) start[i] = 2;
for (int i = 126; i <= 126; ++i) start[i] = 2;
- for (int i = 48; i <= 57; ++i) start[i] = 16;
+ for (int i = 48; i <= 57; ++i) start[i] = 19;
for (int i = 34; i <= 34; ++i) start[i] = 6;
start[92] = 1;
- start[59] = 19;
- start[40] = 20;
- start[41] = 21;
- start[58] = 55;
- start[44] = 22;
- start[91] = 23;
- start[93] = 24;
- start[60] = 56;
- start[62] = 57;
- start[123] = 25;
- start[125] = 58;
- start[61] = 59;
- start[42] = 60;
- start[124] = 61;
- start[8660] = 28;
- start[8658] = 30;
- start[8656] = 31;
- start[38] = 32;
- start[8743] = 34;
- start[8744] = 36;
- start[33] = 62;
- start[8800] = 40;
- start[8804] = 41;
- start[8805] = 42;
- start[43] = 63;
- start[45] = 44;
- start[47] = 45;
- start[172] = 47;
- start[8704] = 50;
- start[8707] = 51;
- start[955] = 52;
- start[8226] = 54;
+ start[59] = 24;
+ start[40] = 25;
+ start[41] = 26;
+ start[58] = 60;
+ start[44] = 27;
+ start[91] = 28;
+ start[93] = 29;
+ start[60] = 61;
+ start[62] = 62;
+ start[123] = 30;
+ start[125] = 63;
+ start[61] = 64;
+ start[42] = 65;
+ start[124] = 66;
+ start[8660] = 33;
+ start[8658] = 35;
+ start[8656] = 36;
+ start[38] = 37;
+ start[8743] = 39;
+ start[8744] = 41;
+ start[33] = 67;
+ start[8800] = 45;
+ start[8804] = 46;
+ start[8805] = 47;
+ start[43] = 68;
+ start[45] = 49;
+ start[47] = 50;
+ start[172] = 52;
+ start[8704] = 55;
+ start[8707] = 56;
+ start[955] = 57;
+ start[8226] = 59;
start[Buffer.EOF] = -1;
}
@@ -503,48 +503,48 @@ public class Scanner {
void CheckLiteral() {
switch (t.val) {
- case "var": t.kind = 7; break;
- case "where": t.kind = 13; break;
- case "int": t.kind = 14; break;
- case "real": t.kind = 15; break;
- case "bool": t.kind = 16; break;
- case "const": t.kind = 21; break;
- case "unique": t.kind = 22; break;
- case "extends": t.kind = 23; break;
- case "complete": t.kind = 24; break;
- case "function": t.kind = 25; break;
- case "returns": t.kind = 26; break;
- case "axiom": t.kind = 29; break;
- case "type": t.kind = 30; break;
- case "procedure": t.kind = 32; break;
- case "implementation": t.kind = 33; break;
- case "modifies": t.kind = 34; break;
- case "free": t.kind = 35; break;
- case "requires": t.kind = 36; break;
- case "ensures": t.kind = 37; break;
- case "goto": t.kind = 38; break;
- case "return": t.kind = 39; break;
- case "if": t.kind = 40; break;
- case "else": t.kind = 41; break;
- case "while": t.kind = 42; break;
- case "invariant": t.kind = 43; break;
- case "break": t.kind = 45; break;
- case "assert": t.kind = 46; break;
- case "assume": t.kind = 47; break;
- case "havoc": t.kind = 48; break;
- case "yield": t.kind = 49; break;
- case "async": t.kind = 51; break;
- case "call": t.kind = 52; break;
- case "par": t.kind = 53; break;
- case "div": t.kind = 76; break;
- case "mod": t.kind = 77; break;
- case "false": t.kind = 82; break;
- case "true": t.kind = 83; break;
- case "old": t.kind = 84; break;
- case "then": t.kind = 87; break;
- case "forall": t.kind = 88; break;
- case "exists": t.kind = 90; break;
- case "lambda": t.kind = 92; break;
+ case "var": t.kind = 8; break;
+ case "where": t.kind = 14; break;
+ case "int": t.kind = 15; break;
+ case "real": t.kind = 16; break;
+ case "bool": t.kind = 17; break;
+ case "const": t.kind = 22; break;
+ case "unique": t.kind = 23; break;
+ case "extends": t.kind = 24; break;
+ case "complete": t.kind = 25; break;
+ case "function": t.kind = 26; break;
+ case "returns": t.kind = 27; break;
+ case "axiom": t.kind = 30; break;
+ case "type": t.kind = 31; break;
+ case "procedure": t.kind = 33; break;
+ case "implementation": t.kind = 34; break;
+ case "modifies": t.kind = 35; break;
+ case "free": t.kind = 36; break;
+ case "requires": t.kind = 37; break;
+ case "ensures": t.kind = 38; break;
+ case "goto": t.kind = 39; break;
+ case "return": t.kind = 40; break;
+ case "if": t.kind = 41; break;
+ case "else": t.kind = 42; break;
+ case "while": t.kind = 43; break;
+ case "invariant": t.kind = 44; break;
+ case "break": t.kind = 46; break;
+ case "assert": t.kind = 47; break;
+ case "assume": t.kind = 48; break;
+ case "havoc": t.kind = 49; break;
+ case "yield": t.kind = 50; break;
+ case "async": t.kind = 52; break;
+ case "call": t.kind = 53; break;
+ case "par": t.kind = 54; break;
+ case "div": t.kind = 77; break;
+ case "mod": t.kind = 78; break;
+ case "false": t.kind = 83; break;
+ case "true": t.kind = 84; break;
+ case "old": t.kind = 85; break;
+ case "then": t.kind = 88; break;
+ case "forall": t.kind = 89; break;
+ case "exists": t.kind = 91; break;
+ case "lambda": t.kind = 93; break;
default: break;
}
}
@@ -597,182 +597,201 @@ public class Scanner {
case 6:
if (ch == '"') {AddCh(); goto case 7;}
else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}
- else if (ch == 92) {AddCh(); goto case 17;}
+ else if (ch == 92) {AddCh(); goto case 20;}
else {goto case 0;}
case 7:
{t.kind = 4; break;}
case 8:
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;}
- else if (ch == '-') {AddCh(); goto case 9;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;}
else {goto case 0;}
case 9:
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;}
- else {goto case 0;}
- case 10:
recEnd = pos; recKind = 5;
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;}
else {t.kind = 5; break;}
- case 11:
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;}
+ case 10:
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 11;}
else {goto case 0;}
- case 12:
+ case 11:
recEnd = pos; recKind = 6;
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;}
- else if (ch == 'e') {AddCh(); goto case 13;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 11;}
+ else if (ch == 'e') {AddCh(); goto case 12;}
else {t.kind = 6; break;}
+ case 12:
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 14;}
+ else if (ch == '-') {AddCh(); goto case 13;}
+ else {goto case 0;}
case 13:
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;}
- else if (ch == '-') {AddCh(); goto case 14;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 14;}
else {goto case 0;}
case 14:
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;}
- else {goto case 0;}
- case 15:
recEnd = pos; recKind = 6;
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 14;}
else {t.kind = 6; break;}
+ case 15:
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;}
+ else {goto case 0;}
case 16:
- recEnd = pos; recKind = 3;
if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;}
+ else if (ch == 'e') {AddCh(); goto case 17;}
+ else {goto case 0;}
+ case 17:
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;}
+ else {goto case 0;}
+ case 18:
+ recEnd = pos; recKind = 7;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;}
+ else {t.kind = 7; break;}
+ case 19:
+ recEnd = pos; recKind = 3;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 19;}
else if (ch == 'b') {AddCh(); goto case 3;}
- else if (ch == 'e') {AddCh(); goto case 8;}
- else if (ch == '.') {AddCh(); goto case 11;}
+ else if (ch == 'e') {AddCh(); goto case 21;}
+ else if (ch == '.') {AddCh(); goto case 10;}
else {t.kind = 3; break;}
- case 17:
- if (ch == '"') {AddCh(); goto case 18;}
+ case 20:
+ if (ch == '"') {AddCh(); goto case 22;}
else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}
- else if (ch == 92) {AddCh(); goto case 17;}
+ else if (ch == 92) {AddCh(); goto case 20;}
else {goto case 0;}
- case 18:
+ case 21:
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 23;}
+ else if (ch == '-') {AddCh(); goto case 8;}
+ else {goto case 0;}
+ case 22:
recEnd = pos; recKind = 4;
if (ch == '"') {AddCh(); goto case 7;}
else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}
- else if (ch == 92) {AddCh(); goto case 17;}
+ else if (ch == 92) {AddCh(); goto case 20;}
else {t.kind = 4; break;}
- case 19:
- {t.kind = 8; break;}
- case 20:
- {t.kind = 9; break;}
- case 21:
- {t.kind = 10; break;}
- case 22:
- {t.kind = 12; break;}
case 23:
- {t.kind = 17; break;}
+ recEnd = pos; recKind = 5;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 23;}
+ else if (ch == 'f') {AddCh(); goto case 15;}
+ else {t.kind = 5; break;}
case 24:
- {t.kind = 18; break;}
+ {t.kind = 9; break;}
case 25:
- {t.kind = 27; break;}
+ {t.kind = 10; break;}
case 26:
- {t.kind = 50; break;}
+ {t.kind = 11; break;}
case 27:
- {t.kind = 55; break;}
+ {t.kind = 13; break;}
case 28:
- {t.kind = 56; break;}
+ {t.kind = 18; break;}
case 29:
- {t.kind = 57; break;}
+ {t.kind = 19; break;}
case 30:
- {t.kind = 58; break;}
+ {t.kind = 28; break;}
case 31:
- {t.kind = 60; break;}
+ {t.kind = 51; break;}
case 32:
- if (ch == '&') {AddCh(); goto case 33;}
- else {goto case 0;}
+ {t.kind = 56; break;}
case 33:
- {t.kind = 61; break;}
+ {t.kind = 57; break;}
case 34:
- {t.kind = 62; break;}
+ {t.kind = 58; break;}
case 35:
- {t.kind = 63; break;}
+ {t.kind = 59; break;}
case 36:
- {t.kind = 64; break;}
+ {t.kind = 61; break;}
case 37:
- {t.kind = 67; break;}
+ if (ch == '&') {AddCh(); goto case 38;}
+ else {goto case 0;}
case 38:
- {t.kind = 68; break;}
+ {t.kind = 62; break;}
case 39:
- {t.kind = 69; break;}
+ {t.kind = 63; break;}
case 40:
- {t.kind = 70; break;}
+ {t.kind = 64; break;}
case 41:
- {t.kind = 71; break;}
+ {t.kind = 65; break;}
case 42:
- {t.kind = 72; break;}
+ {t.kind = 68; break;}
case 43:
- {t.kind = 73; break;}
+ {t.kind = 69; break;}
case 44:
- {t.kind = 75; break;}
+ {t.kind = 70; break;}
case 45:
- {t.kind = 78; break;}
+ {t.kind = 71; break;}
case 46:
- {t.kind = 79; break;}
+ {t.kind = 72; break;}
case 47:
- {t.kind = 81; break;}
+ {t.kind = 73; break;}
case 48:
- {t.kind = 85; break;}
+ {t.kind = 74; break;}
case 49:
- {t.kind = 86; break;}
+ {t.kind = 76; break;}
case 50:
- {t.kind = 89; break;}
+ {t.kind = 79; break;}
case 51:
- {t.kind = 91; break;}
+ {t.kind = 80; break;}
case 52:
- {t.kind = 93; break;}
+ {t.kind = 82; break;}
case 53:
- {t.kind = 94; break;}
+ {t.kind = 86; break;}
case 54:
- {t.kind = 95; break;}
+ {t.kind = 87; break;}
case 55:
- recEnd = pos; recKind = 11;
- if (ch == '=') {AddCh(); goto case 26;}
- else if (ch == ':') {AddCh(); goto case 53;}
- else {t.kind = 11; break;}
+ {t.kind = 90; break;}
case 56:
- recEnd = pos; recKind = 19;
- if (ch == '=') {AddCh(); goto case 64;}
- else if (ch == ':') {AddCh(); goto case 39;}
- else {t.kind = 19; break;}
+ {t.kind = 92; break;}
case 57:
- recEnd = pos; recKind = 20;
- if (ch == '=') {AddCh(); goto case 37;}
- else {t.kind = 20; break;}
+ {t.kind = 94; break;}
case 58:
- recEnd = pos; recKind = 28;
- if (ch == '|') {AddCh(); goto case 49;}
- else {t.kind = 28; break;}
+ {t.kind = 95; break;}
case 59:
- recEnd = pos; recKind = 31;
- if (ch == '=') {AddCh(); goto case 65;}
- else {t.kind = 31; break;}
+ {t.kind = 96; break;}
case 60:
- recEnd = pos; recKind = 44;
- if (ch == '*') {AddCh(); goto case 46;}
- else {t.kind = 44; break;}
+ recEnd = pos; recKind = 12;
+ if (ch == '=') {AddCh(); goto case 31;}
+ else if (ch == ':') {AddCh(); goto case 58;}
+ else {t.kind = 12; break;}
case 61:
- recEnd = pos; recKind = 54;
- if (ch == '|') {AddCh(); goto case 35;}
- else if (ch == '{') {AddCh(); goto case 48;}
- else {t.kind = 54; break;}
+ recEnd = pos; recKind = 20;
+ if (ch == '=') {AddCh(); goto case 69;}
+ else if (ch == ':') {AddCh(); goto case 44;}
+ else {t.kind = 20; break;}
case 62:
- recEnd = pos; recKind = 80;
- if (ch == '=') {AddCh(); goto case 38;}
- else {t.kind = 80; break;}
+ recEnd = pos; recKind = 21;
+ if (ch == '=') {AddCh(); goto case 42;}
+ else {t.kind = 21; break;}
case 63:
- recEnd = pos; recKind = 74;
- if (ch == '+') {AddCh(); goto case 43;}
- else {t.kind = 74; break;}
+ recEnd = pos; recKind = 29;
+ if (ch == '|') {AddCh(); goto case 54;}
+ else {t.kind = 29; break;}
case 64:
- recEnd = pos; recKind = 66;
- if (ch == '=') {AddCh(); goto case 66;}
- else {t.kind = 66; break;}
+ recEnd = pos; recKind = 32;
+ if (ch == '=') {AddCh(); goto case 70;}
+ else {t.kind = 32; break;}
case 65:
- recEnd = pos; recKind = 65;
- if (ch == '>') {AddCh(); goto case 29;}
- else {t.kind = 65; break;}
+ recEnd = pos; recKind = 45;
+ if (ch == '*') {AddCh(); goto case 51;}
+ else {t.kind = 45; break;}
case 66:
- recEnd = pos; recKind = 59;
- if (ch == '>') {AddCh(); goto case 27;}
- else {t.kind = 59; break;}
+ recEnd = pos; recKind = 55;
+ if (ch == '|') {AddCh(); goto case 40;}
+ else if (ch == '{') {AddCh(); goto case 53;}
+ else {t.kind = 55; break;}
+ case 67:
+ recEnd = pos; recKind = 81;
+ if (ch == '=') {AddCh(); goto case 43;}
+ else {t.kind = 81; break;}
+ case 68:
+ recEnd = pos; recKind = 75;
+ if (ch == '+') {AddCh(); goto case 48;}
+ else {t.kind = 75; break;}
+ case 69:
+ recEnd = pos; recKind = 67;
+ if (ch == '=') {AddCh(); goto case 71;}
+ else {t.kind = 67; break;}
+ case 70:
+ recEnd = pos; recKind = 66;
+ if (ch == '>') {AddCh(); goto case 34;}
+ else {t.kind = 66; break;}
+ case 71:
+ recEnd = pos; recKind = 60;
+ if (ch == '>') {AddCh(); goto case 32;}
+ else {t.kind = 60; break;}
}
t.val = new String(tval, 0, tlen);
diff --git a/Test/floats/float0.bpl b/Test/floats/float0.bpl
index 1a642835..d7faa4b0 100644
--- a/Test/floats/float0.bpl
+++ b/Test/floats/float0.bpl
@@ -4,11 +4,11 @@ procedure foo(x : real) returns (r : float8e24)
{
r := 15; // Error
r := 15.0; // Error
- r := fp(false, 1bv8, 0bv22); // Error
- r := fp<8, 23>(1bv31); // Error
+ r := 0e1f22e8; // Error
+ r := 1e0f23e8; // Error
r := x; // Error
- r := fp<8, 23>(1bv31) + fp<8, 23>(1bv31); // Error
- r := fp<8, 24>(1bv32) + fp<8, 23>(1bv31); // Error
+ r := 1e0f23e8 + 1e0f23e8; // Error
+ r := 1e0f24e8 + 1e0f23e8; // Error
return;
} \ No newline at end of file
diff --git a/Test/floats/float1.bpl b/Test/floats/float1.bpl
index 9ed62579..2b901c94 100644
--- a/Test/floats/float1.bpl
+++ b/Test/floats/float1.bpl
@@ -1,13 +1,13 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure foo(x : float<8, 24>) returns (r : float<8, 24>)
-{
- r := fp(false, 1bv8, 0bv23);
- r := fp<8, 24>(1bv32);
- r := x;
- r := x + fp<8, 24>(1bv32);
- r := fp<8, 24>(1bv32) + fp<8, 24>(1bv32);
- assert(r == fp<8, 24>(2bv32));
-
- return;
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo(x : float24e8) returns (r : float24e8)
+{
+ r := 0e1f24e8;
+ r := 1e0f24e8;
+ r := x;
+ r := x + 1e0f24e8;
+ r := 0e0f24e8 + 0e0f24e8;
+ assert(r == 0e1f24e8);
+
+ return;
} \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-21 11:49:04 +0000