From 6ac996211d6f42f0c7f61ea108388d6bb798ecf8 Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Sat, 20 Feb 2016 20:53:08 -0700 Subject: Modified BigFloat and parser to accept correct SMT-LIB syntax --- Source/Basetypes/BigFloat.cs | 250 ++++++++++++++---------------- Source/Core/Parser.cs | 90 +++++++---- Source/Provers/SMTLib/SMTLibLineariser.cs | 4 +- fp_documentation.txt | 19 ++- 4 files changed, 192 insertions(+), 171 deletions(-) diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs index 5b169263..8cde2cb9 100644 --- a/Source/Basetypes/BigFloat.cs +++ b/Source/Basetypes/BigFloat.cs @@ -17,7 +17,7 @@ namespace Microsoft.Basetypes /// /// A representation of a 32-bit floating point value - /// Note that this value has a 1-bit sign, 8-bit exponent, and 24-bit mantissa + /// Note that this value has a 1-bit sign, 8-bit exponent, and 24-bit significand /// public struct BigFloat { @@ -25,33 +25,33 @@ namespace Microsoft.Basetypes // the internal representation [Rep] - internal readonly long mantissa; //Note that the mantissa arrangement matches standard fp arrangement (most significant bit is farthest left) + internal readonly BigNum significand; //Note that the significand arrangement matches standard fp arrangement (most significant bit is farthest left) [Rep] - internal readonly int mantissaSize; + internal readonly int significandSize; [Rep] - internal readonly int exponent; //The value of the exponent is always positive as per fp representation requirements + 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 dec_value; + internal readonly String value; //Only used with second syntax [Rep] - internal readonly bool isDec; + internal readonly bool isNeg; - public long Mantissa { + public BigNum Significand { get { - return mantissa; + return significand; } } - public int Exponent { + public BigNum Exponent { get { return exponent; } } - public int MantissaSize { + public int SignificandSize { get { - return mantissaSize; + return significandSize; } } @@ -61,25 +61,26 @@ namespace Microsoft.Basetypes } } - public String Decimal { + public bool IsNegative { get { - return dec_value; + return this.isNeg; } } - public bool IsDec { + public String Value { get { - return isDec; + return value; } } - public static BigFloat ZERO(int mantissaSize, int exponentSize) { return new BigFloat(0, 0, mantissaSize, exponentSize); } //Does not include negative zero + 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 BIM two = new BIM(2); - private static long two_n(int n) { - long toReturn = 1; + 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 * 2; + toReturn = toReturn * two; return toReturn; } @@ -95,18 +96,18 @@ namespace Microsoft.Basetypes return new BigFloat(v.ToString(), 8, 24); } - public static BigFloat FromInt(int v, int exponentSize, int mantissaSize) + public static BigFloat FromInt(int v, int exponentSize, int significandSize) { - return new BigFloat(v.ToString(), exponentSize, mantissaSize); + 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 mantissaSize) + public static BigFloat FromBigInt(BIM v, int exponentSize, int significandSize) { - return new BigFloat(v.ToString(), exponentSize, mantissaSize); + return new BigFloat(v.ToString(), exponentSize, significandSize); } public static BigFloat FromBigDec(BigDec v) @@ -114,84 +115,67 @@ namespace Microsoft.Basetypes return new BigFloat(v.ToDecimalString(), 8, 24); } - public static BigFloat FromBigDec(BigDec v, int exponentSize, int mantissaSize) + public static BigFloat FromBigDec(BigDec v, int exponentSize, int significandSize) { - return new BigFloat(v.ToDecimalString(), exponentSize, mantissaSize); + return new BigFloat(v.ToDecimalString(), exponentSize, significandSize); } [Pure] - public static BigFloat FromString(string v) { - String[] vals = v.Split(' '); - if (vals.Length == 0 || vals.Length > 4) - throw new FormatException(); - try - { - switch (vals.Length) { - case 1: - return new BigFloat(vals[0], 8, 24); - case 2: - return new BigFloat(Int32.Parse(vals[0]), Int64.Parse(vals[1]), 8, 24); - case 3: - return new BigFloat(vals[0], Int32.Parse(vals[1]), Int32.Parse(vals[2])); - case 4: - return new BigFloat(Int32.Parse(vals[0]), Int64.Parse(vals[1]), Int32.Parse(vals[2]), Int32.Parse(vals[3])); - default: - throw new FormatException(); //Unreachable - } - } - catch (Exception) { //Catch parsing errors - throw new FormatException(); - } + public static BigFloat FromString(String v, int exp, int sig) { //String must be + return new BigFloat(v, exp, sig); } - internal BigFloat(int exponent, long mantissa, int exponentSize, int mantissaSize) { + public BigFloat(bool sign, BigNum exponent, BigNum significand, int exponentSize, int significandSize) { this.exponentSize = exponentSize; this.exponent = exponent; - this.mantissa = mantissa; - this.mantissaSize = mantissaSize; - this.isDec = false; - this.dec_value = ""; + this.significand = significand; + this.significandSize = significandSize; + this.isNeg = sign; + this.value = ""; } - internal BigFloat(String dec_value, int exponentSize, int mantissaSize) { + public BigFloat(String value, int exponentSize, int significandSize) { this.exponentSize = exponentSize; - this.mantissaSize = mantissaSize; - this.exponent = 0; - this.mantissa = 0; - this.isDec = true; - this.dec_value = dec_value; + this.significandSize = significandSize; + this.exponent = BigNum.ZERO; + this.significand = BigNum.ZERO; + this.value = value; + this.isNeg = value[0] == '-'; //Special cases: - if (this.dec_value.Equals("+oo") || this.dec_value.Equals("-oo") || this.dec_value.Equals("-zero")) + if (this.value.Equals("+oo") || this.value.Equals("-oo") || this.value.Equals("-zero")) return; - if (this.dec_value.ToLower().Equals("nan")) { - this.dec_value = "NaN"; + if (this.value.ToLower().Equals("nan")) { + this.value = "NaN"; return; } - if (this.dec_value.Equals("INF") || this.dec_value.Equals("+INF")) { - this.dec_value = "+oo"; + if (this.value.Equals("INF") || this.value.Equals("+INF")) + { + this.value = "+oo"; return; } - if (this.dec_value.Equals("-INF")) { - this.dec_value = "-oo"; + if (this.value.Equals("-INF")) + { + this.value = "-oo"; return; } - if (this.dec_value.Equals("+zero")) { - this.dec_value = "0.0"; + if (this.value.Equals("+zero")) + { + this.value = "0.0"; return; } //End special cases - if (this.dec_value.IndexOf('.') == -1 && this.dec_value.IndexOf('e') == -1) - this.dec_value += ".0"; //Assures that the decimal value is a "real" number - if (this.dec_value.IndexOf('.') == 0) - this.dec_value = "0" + this.dec_value; //Assures that decimals always have a 0 in front + if (this.value.IndexOf('.') == -1 && this.value.IndexOf('e') == -1) + this.value += ".0"; //Assures that the decimal value is a "real" number + if (this.value.IndexOf('.') == 0) + this.value = "0" + this.value; //Assures that decimals always have a 0 in front } - private BIM maxMantissa() + private BigNum maxsignificand() { - BIM result = new BIM(1); - for (int i = 0; i < mantissaSize; i++) + BigNum result = one; + for (int i = 0; i < significandSize; i++) result = result * two; - return result - 1; + return result - one; } private int maxExponent() { return (int)Math.Pow(2, exponentSize) - 1; } @@ -213,13 +197,13 @@ namespace Microsoft.Basetypes [Pure] public override int GetHashCode() { - return Mantissa.GetHashCode() * 13 + Exponent.GetHashCode(); + return significand.GetHashCode() * 13 + Exponent.GetHashCode(); } [Pure] public override string/*!*/ ToString() { Contract.Ensures(Contract.Result() != null); - return isDec ? dec_value : String.Format("{0}x2^{1}", Mantissa.ToString(), Exponent.ToString()); + return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value; } @@ -229,41 +213,41 @@ namespace Microsoft.Basetypes /// /// 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 mantissa and exponent size + /// the returned fp assumes the given significand and exponent size /// /// - /// + /// /// /// - public static BigFloat Round(String value, int exponentSize, int mantissaSize) + public static BigFloat Round(String value, int exponentSize, int significandSize) { int i = value.IndexOf('.'); if (i == -1) - return Round(BIM.Parse(value), 0, exponentSize, mantissaSize); - return Round(i == 0 ? 0 : BIM.Parse(value.Substring(0, i)), BIM.Parse(value.Substring(i + 1, value.Length - i - 1)), exponentSize, mantissaSize); + 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); } /// /// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!!! - /// Converts value.dec_value to a the closest float approximation with the given mantissaSize, exponentSize + /// Converts value.dec_value to a the closest float approximation with the given significandSize, exponentSize /// Returns the result of this calculation /// /// /// - /// + /// /// /// - public static BigFloat Round(BIM value, BIM dec_value, int exponentSize, int mantissaSize) + public static BigFloat Round(BigNum value, BigNum 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 + 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 BIM(10); + dec_max = new BigNum(10); while (dec_max < dec_value) dec_max = dec_max * ten; dec_value = dec_value + dec_max; @@ -275,7 +259,7 @@ namespace Microsoft.Basetypes exp++; } if (value.IsZero && !dec_value.IsZero) { - dec_max = new BIM(10); + 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 @@ -288,12 +272,12 @@ namespace Microsoft.Basetypes } } - //Second, calculate the mantissa - value = new BIM(0); //remove implicit bit - dec_max = new BIM(10); + //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 = mantissaSize; i > 0 && !dec_value.IsZero; i--) { //Multiply by two until the mantissa is fully calculated + 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; @@ -301,7 +285,7 @@ namespace Microsoft.Basetypes } } - return new BigFloat(exp, Int64.Parse(value.ToString()), exponentSize, mantissaSize); + 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). @@ -312,30 +296,32 @@ namespace Microsoft.Basetypes /// /// The Floor (rounded towards negative infinity) /// Ceiling (rounded towards positive infinity) - public void FloorCeiling(out BIM floor, out BIM ceiling) { + public void FloorCeiling(out BigNum floor, out BigNum ceiling) { //TODO: fix for fp functionality - BIM n = Mantissa; - int e = Exponent; + BigNum n = Significand; + BigNum e = Exponent; if (n.IsZero) { floor = ceiling = n; - } else if (0 <= e) { + } else if (BigNum.ZERO <= e) { // it's an integer - for (; 0 < e; e--) { + 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 (; e < 0 && !n.IsZero; e++) { + for (; BigNum.ZERO < e && !n.IsZero; e = e + one) + { n = n / two; // Division rounds towards negative infinity } if (!IsNegative) { floor = n; - ceiling = n + 1; + ceiling = n + one; } else { ceiling = n; - floor = n - 1; + floor = n - one; } } Debug.Assert(floor <= ceiling, "Invariant was not maintained"); @@ -352,7 +338,7 @@ namespace Microsoft.Basetypes [Pure] public string ToDecimalString() { Contract.Ensures(Contract.Result() != null); - return isDec ? dec_value : String.Format("{0}x2^{1}", Mantissa.ToString(), Exponent.ToString()); + return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value; } [Pure] @@ -380,18 +366,16 @@ namespace Microsoft.Basetypes [Pure] public BigFloat Abs { get { - if (IsDec) - return dec_value[0] == '-' ? new BigFloat(dec_value.Remove(0, 1), ExponentSize, MantissaSize) : this; - return new BigFloat(Exponent, Math.Abs(Mantissa), ExponentSize, MantissaSize); + return new BigFloat(true, Exponent, Significand, ExponentSize, SignificandSize); } } [Pure] public BigFloat Negate { get { - if (IsDec) - return dec_value[0] == '-' ? new BigFloat(dec_value.Remove(0, 1), ExponentSize, MantissaSize) : new BigFloat("-" + dec_value, ExponentSize, MantissaSize); - return new BigFloat(Exponent, -Mantissa, ExponentSize, MantissaSize); + 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); } } @@ -404,26 +388,26 @@ namespace Microsoft.Basetypes public static BigFloat operator +(BigFloat x, BigFloat y) { //TODO: Modify for correct fp functionality Contract.Requires(x.ExponentSize == y.ExponentSize); - Contract.Requires(x.MantissaSize == y.MantissaSize); - long m1 = x.Mantissa; - int e1 = x.Exponent; - long m2 = y.Mantissa; - int e2 = y.Exponent; - m1 = m1 + two_n(x.mantissaSize + 1); //Add implicit bit - m2 = m2 + two_n(y.mantissaSize + 1); + 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.Mantissa; + m1 = y.significand; e1 = y.Exponent; - m2 = x.Mantissa; + m2 = x.significand; e2 = x.Exponent; } while (e2 < e1) { - m2 = m2 / 2; - e2++; + m2 = m2 / two; + e2 = e2 + one; } - return new BigFloat(e1, m1 + m2, x.MantissaSize, x.ExponentSize); + return new BigFloat(false, e1, m1 + m2, x.significandSize, x.ExponentSize); } [Pure] @@ -434,8 +418,8 @@ namespace Microsoft.Basetypes [Pure] public static BigFloat operator *(BigFloat x, BigFloat y) { Contract.Requires(x.ExponentSize == y.ExponentSize); - Contract.Requires(x.MantissaSize == y.MantissaSize); - return new BigFloat(x.Exponent + y.Exponent, x.Mantissa * y.Mantissa, x.MantissaSize, x.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); } @@ -444,9 +428,9 @@ namespace Microsoft.Basetypes public bool IsSpecialType { get { - if (!IsDec) + if (value == "") return false; - return (dec_value.Equals("NaN") || dec_value.Equals("+oo") || dec_value.Equals("-oo") || dec_value.Equals("-zero")); + return (value.Equals("NaN") || value.Equals("+oo") || value.Equals("-oo") || value.Equals("-zero")); } } @@ -456,15 +440,9 @@ namespace Microsoft.Basetypes } } - public bool IsNegative { - get { - return (isDec && dec_value[0] == '-') || mantissa < 0; - } - } - public bool IsZero { get { - return Mantissa == 0 && Exponent == 0; + return significand.Equals(BigNum.ZERO) && Exponent == BigNum.ZERO; } } @@ -474,9 +452,9 @@ namespace Microsoft.Basetypes return 1; if (this.exponent < that.exponent) return -1; - if (this.Mantissa == that.Mantissa) + if (this.significand == that.significand) return 0; - return this.Mantissa > that.Mantissa ? 1 : -1; + return this.significand > that.significand ? 1 : -1; } [Pure] diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 5fcb1cdc..bf35ccbe 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -668,17 +668,35 @@ private class BvBounds : Expr { ty = new BasicType(t, SimpleType.Real); } else if (la.kind == 98) { Get(); - if (la.kind == 9) { - Get(); - Expect(3); - int exp = Int32.Parse(t.val); - Expect(3); - int man = Int32.Parse(t.val); - ty = new FloatType(t, exp, man); - Expect(10); + if (la.kind == 3) { + Expect(3); + switch (Int32.Parse(t.val)) { + case 16: + ty = new FloatType(t, 5, 11); + break; + case 32: + ty = new FloatType(t, 8, 24); + break; + case 64: + ty = new FloatType(t, 11, 53); + break; + case 128: + ty = new FloatType(t, 15, 113); + break; + default: + SynErr(3); + break; + } + } + else { + Expect(19); + Expect(3); + int exp = Int32.Parse(t.val); + Expect(3); + int man = Int32.Parse(t.val); + ty = new FloatType(t, exp, man); + Expect(20); } - else - ty = new FloatType(t, 8, 24); } else if (la.kind == 16) { Get(); ty = new BasicType(t, SimpleType.Bool); @@ -1813,9 +1831,9 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { case 98: { Get(); x = t; - Expect(9); + Expect(19); Expression(out e); - Expect(10); + Expect(20); e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToFloat), new List { e }); break; } @@ -1887,29 +1905,45 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { /// void Float(out BigFloat n) { - //To be modified - string s = ""; try { - if (la.kind == 97) - { - //Expected format = fp (a b) || fp (a b c d) + if (la.kind == 97) { + bool negative = false; + int exp, sig; + BigNum exp_val, sig_val, value; + //Expected format = fp(sign exp_val sig_val) || fp(value) Get(); //Skip the fp token Get(); - if (t.val != "(") { throw new FormatException(); } - while (la.kind == 1 || la.kind == 3 || la.kind == 6 || la.kind == 4 || la.kind == 74 || la.kind == 75) { //Get values between the parens + if (t.val == "(") { Get(); - if (t.val == "-" || t.val == "+") //special sign case (la.kind == 74 or 75) - s += t.val; - else - s += t.val + " "; + negative = Boolean.Parse(t.val); + BvLit(out exp_val, out exp); + BvLit(out sig_val, out sig); + n = new BigFloat(negative, exp_val, sig_val, exp, sig); + } + else if (t.val == "<") { + Expect(14); + exp = Int32.Parse(t.val); + Expect(14); + sig = Int32.Parse(t.val); + int size; + BvLit(out value, out size); + if (size != exp + sig) + { + this.SemErr("The given bitvector size of " + size + "does not match the provided floating-point size of " + (exp + sig)); + n = BigFloat.ZERO(8, 24); + return; + } + n = new BigFloat(t.val, exp, sig); + } + else { + throw new FormatException(); } - Get(); - if (t.val != ")") { throw new FormatException(); } } - else SynErr(137); - - n = BigFloat.FromString(s.Trim()); + else { + n = BigFloat.ZERO(8, 24); + SynErr(137); + } } catch (FormatException) { diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 7c3ae960..59b6b7e7 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -205,10 +205,10 @@ namespace Microsoft.Boogie.SMTLib { BigFloat lit = ((VCExprFloatLit)node).Val; if (lit.IsSpecialType) { - wr.Write("(_ " + lit.Decimal + " " + lit.ExponentSize.ToString() + " " + lit.MantissaSize.ToString() + ")"); + wr.Write("(_ " + lit.Decimal + " " + lit.ExponentSize.ToString() + " " + lit.SignificandSize.ToString() + ")"); return true; } - wr.Write("((_ to_fp " + lit.ExponentSize.ToString() + " " + lit.MantissaSize.ToString() + ") RNE "); + wr.Write("((_ to_fp " + lit.ExponentSize.ToString() + " " + lit.SignificandSize.ToString() + ") RNE "); if (lit.IsNegative) // In SMT2 "-42" is an identifier (SMT2, Sect. 3.2 "Symbols") wr.Write("(- 0.0 {0})", lit.Abs.ToDecimalString()); diff --git a/fp_documentation.txt b/fp_documentation.txt index 09e60b9a..d3fafdcb 100644 --- a/fp_documentation.txt +++ b/fp_documentation.txt @@ -10,7 +10,9 @@ Declaring Variables: The syntax for declaring a floating point variable is as follows: var name: float(exp man); Where exp is the size of the float exponent and man is the size of the float mantissa +Please note that +**REMOVE THIS SYNTAX** It is also acceptable to use the following syntax: var name: float(); This syntax assumes the float exponent to be size 8 and the mantissa to be size 24 @@ -23,10 +25,11 @@ Declares a variable called x with a exponent sized 11 and mantissa sized 53 Declaring Constants: All of the following syntax are viable for declaring a floating point constant: -float(dec) -float(exp_val man_val) -float(dec exp man) -float(exp_val man_val exp man) +**REMOVE THE FIRST OF THESE TWO SYNTAXES** +fp(dec) +fp(exp_val man_val) +fp(dec exp man) +fp(exp_val man_val exp man) Where dec is the decimal value of the constant, exp_val/man_value are the integer values of their respective fields, @@ -68,6 +71,8 @@ Where exp and man are the sizes of the exponent and mantissa respectively -------------------------------------------------------------------------------- Known Issues: +float16, float32, float64, and float128 still need to be added + There is currently no way to convert from a floating point to any other data type There is currently no way to convert the value of a variable to a floating point type @@ -76,4 +81,8 @@ var x : real; fp(x); Statements of the following form cause a parser error (parenthesis followed by fp constant) -... (fp(1) + fp(1)); \ No newline at end of file +... (fp(1) + fp(1)); + +Attempts by Boogie to infer the behavior of loops fail when floating points are involved + +Describing loop behavior manually is untested (using loop unroll appears to work) \ No newline at end of file -- cgit v1.2.3