summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@mit.edu>2016-10-29 17:35:13 -0400
committerGravatar Benjamin Barenblat <bbaren@mit.edu>2016-10-29 17:35:13 -0400
commit1f2d6c15cc587e9e1b91be70186ee9a26d5e1928 (patch)
tree1b6cd99944efbba2c993327bb49f2d544d50b1eb
parent41082463d783d6f8d8a5aaf69bf459b57bca6000 (diff)
parentba4f9fa1fbd923bfce1363566af08624c5c6fe38 (diff)
Merge branch 'upstream' into dfsg_freedfsg_free
-rw-r--r--Binaries/Boogie.vshost.exe.manifest11
-rw-r--r--Binaries/PrepareBoogieZip.bat32
-rw-r--r--README.md6
-rw-r--r--Source/AbsInt/AbsInt.csproj4
-rw-r--r--Source/AbsInt/IntervalDomain.cs34
-rw-r--r--Source/Basetypes/Basetypes.csproj9
-rw-r--r--Source/Basetypes/BigFloat.cs509
-rw-r--r--Source/CodeContractsExtender/CodeContractsExtender.csproj8
-rw-r--r--Source/Concurrency/Concurrency.csproj6
-rw-r--r--Source/Core/AbsyExpr.cs98
-rw-r--r--Source/Core/AbsyType.cs238
-rw-r--r--Source/Core/BoogiePL.atg31
-rw-r--r--Source/Core/Core.csproj6
-rw-r--r--Source/Core/Parser.cs887
-rw-r--r--Source/Core/Scanner.cs486
-rw-r--r--Source/Core/StandardVisitor.cs6
-rw-r--r--Source/Doomed/Doomed.csproj2
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.cs4
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.csproj3
-rw-r--r--Source/ExecutionEngine/ThreadTaskScheduler.cs58
-rw-r--r--Source/Graph/Graph.csproj8
-rw-r--r--Source/Houdini/Houdini.csproj2
-rw-r--r--Source/Model/Model.csproj8
-rw-r--r--Source/ModelViewer/ModelViewer.csproj4
-rw-r--r--Source/ParserHelper/ParserHelper.csproj8
-rw-r--r--Source/Predication/Predication.csproj4
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs81
-rw-r--r--Source/Provers/SMTLib/TypeDeclCollector.cs2
-rw-r--r--Source/UnitTests/CoreTests/CoreTests.csproj2
-rw-r--r--Source/UnitTests/CoreTests/ExprImmutability.cs3
-rw-r--r--Source/VCExpr/Boogie2VCExpr.cs46
-rw-r--r--Source/VCExpr/SimplifyLikeLineariser.cs130
-rw-r--r--Source/VCExpr/TypeErasure.cs91
-rw-r--r--Source/VCExpr/VCExpr.csproj8
-rw-r--r--Source/VCExpr/VCExprAST.cs134
-rw-r--r--Source/VCExpr/VCExprASTPrinter.cs72
-rw-r--r--Source/VCExpr/VCExprASTVisitors.cs154
-rw-r--r--Source/VCGeneration/VCGeneration.csproj8
-rw-r--r--Test/civl/ticket.bpl25
-rw-r--r--Test/civl/ticket.bpl.expect2
-rw-r--r--Test/floats/float0.bpl14
-rw-r--r--Test/floats/float0.bpl.expect8
-rw-r--r--Test/floats/float1.bpl13
-rw-r--r--Test/floats/float1.bpl.expect2
-rw-r--r--Test/floats/float10.bpl18
-rw-r--r--Test/floats/float10.bpl.expect5
-rw-r--r--Test/floats/float11.bpl22
-rw-r--r--Test/floats/float11.bpl.expect7
-rw-r--r--Test/floats/float12.bpl16
-rw-r--r--Test/floats/float12.bpl.expect2
-rw-r--r--Test/floats/float13.bpl34
-rw-r--r--Test/floats/float13.bpl.expect2
-rw-r--r--Test/floats/float14.bpl22
-rw-r--r--Test/floats/float14.bpl.expect9
-rw-r--r--Test/floats/float2.bpl15
-rw-r--r--Test/floats/float2.bpl.expect7
-rw-r--r--Test/floats/float3.bpl27
-rw-r--r--Test/floats/float3.bpl.expect2
-rw-r--r--Test/floats/float4.bpl19
-rw-r--r--Test/floats/float4.bpl.expect2
-rw-r--r--Test/floats/float5.bpl23
-rw-r--r--Test/floats/float5.bpl.expect6
-rw-r--r--Test/floats/float6.bpl30
-rw-r--r--Test/floats/float6.bpl.expect2
-rw-r--r--Test/floats/float7.bpl13
-rw-r--r--Test/floats/float7.bpl.expect2
-rw-r--r--Test/floats/float8.bpl13
-rw-r--r--Test/floats/float8.bpl.expect5
-rw-r--r--Test/floats/float9.bpl17
-rw-r--r--Test/floats/float9.bpl.expect2
70 files changed, 2878 insertions, 711 deletions
diff --git a/Binaries/Boogie.vshost.exe.manifest b/Binaries/Boogie.vshost.exe.manifest
new file mode 100644
index 00000000..061c9ca9
--- /dev/null
+++ b/Binaries/Boogie.vshost.exe.manifest
@@ -0,0 +1,11 @@
+<?xml version="1.0" encoding="UTF-8" standalone="yes"?>
+<assembly xmlns="urn:schemas-microsoft-com:asm.v1" manifestVersion="1.0">
+ <assemblyIdentity version="1.0.0.0" name="MyApplication.app"/>
+ <trustInfo xmlns="urn:schemas-microsoft-com:asm.v2">
+ <security>
+ <requestedPrivileges xmlns="urn:schemas-microsoft-com:asm.v3">
+ <requestedExecutionLevel level="asInvoker" uiAccess="false"/>
+ </requestedPrivileges>
+ </security>
+ </trustInfo>
+</assembly>
diff --git a/Binaries/PrepareBoogieZip.bat b/Binaries/PrepareBoogieZip.bat
index 5a1b267f..99a7a0a6 100644
--- a/Binaries/PrepareBoogieZip.bat
+++ b/Binaries/PrepareBoogieZip.bat
@@ -7,22 +7,22 @@ if exist %DEST_DIR% del /q %DEST_DIR%\*
if not exist %DEST_DIR% mkdir %DEST_DIR%
for %%f in (
- AbsInt.dll AbsInt.pdb
- Basetypes.dll Basetypes.pdb
- Boogie.exe Boogie.pdb
- BVD.exe BVD.pdb
- CodeContractsExtender.dll CodeContractsExtender.pdb
- Core.dll Core.pdb
- Doomed.dll Doomed.pdb
- Graph.dll Graph.pdb
- Houdini.dll Houdini.pdb
- Model.dll Model.pdb
- ParserHelper.dll ParserHelper.pdb
- Predication.dll Predication.pdb
- Provers.SMTLib.dll Provers.SMTLib.pdb
- UnivBackPred2.smt UnivBackPred2.smt2
- VCExpr.dll VCExpr.pdb
- VCGeneration.dll VCGeneration.pdb
+ BoogieAbsInt.dll BoogieAbsInt.pdb
+ BoogieBasetypes.dll BoogieBasetypes.pdb
+ Boogie.exe Boogie.pdb
+ BVD.exe BVD.pdb
+ BoogieCodeContractsExtender.dll BoogieCodeContractsExtender.pdb
+ BoogieCore.dll BoogieCore.pdb
+ BoogieDoomed.dll BoogieDoomed.pdb
+ BoogieGraph.dll BoogieGraph.pdb
+ BoogieHoudini.dll BoogieHoudini.pdb
+ BoogieModel.dll BoogieModel.pdb
+ BoogieParserHelper.dll BoogieParserHelper.pdb
+ BoogiePredication.dll BoogiePredication.pdb
+ Provers.SMTLib.dll Provers.SMTLib.pdb
+ UnivBackPred2.smt UnivBackPred2.smt2
+ BoogieVCExpr.dll BoogieVCExpr.pdb
+ BoogieVCGeneration.dll BoogieVCGeneration.pdb
) do (
copy %%f %DEST_DIR%
)
diff --git a/README.md b/README.md
index 1dd0ba5a..beb217fd 100644
--- a/README.md
+++ b/README.md
@@ -33,9 +33,13 @@ several other institutions make the open-source Boogie tool what it is.
![boogie architecture](http://research.microsoft.com/en-us/projects/boogie/boogie.png)
+More documentation can be found at http://boogie-docs.readthedocs.org/en/latest/ .
+
## Language Reference
-[This is Boogie2](http://research.microsoft.com/en-us/um/people/leino/papers/krml178.pdf) details
+See [Language reference](http://boogie-docs.readthedocs.org/en/latest/LangRef.html).
+
+Note: [This is Boogie2](http://research.microsoft.com/en-us/um/people/leino/papers/krml178.pdf) details
many aspects of the Boogie IVL but is slightly out of date.
## Getting help
diff --git a/Source/AbsInt/AbsInt.csproj b/Source/AbsInt/AbsInt.csproj
index 47f45f58..359eb146 100644
--- a/Source/AbsInt/AbsInt.csproj
+++ b/Source/AbsInt/AbsInt.csproj
@@ -9,7 +9,7 @@
<OutputType>Library</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>AbsInt</RootNamespace>
- <AssemblyName>AbsInt</AssemblyName>
+ <AssemblyName>BoogieAbsInt</AssemblyName>
<TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
<CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
@@ -34,7 +34,7 @@
<IsWebBootstrapper>false</IsWebBootstrapper>
<UseApplicationTrust>false</UseApplicationTrust>
<BootstrapperEnabled>true</BootstrapperEnabled>
- <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile>
+ <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index 2fd37463..1d35b735 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -180,8 +180,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
}
}
return e;
- } else {
- Contract.Assert(V.TypedIdent.Type.IsReal);
+ } else if (V.TypedIdent.Type.IsReal){
Expr e = Expr.True;
if (Lo != null && Hi != null && Lo == Hi) {
// produce an equality
@@ -199,6 +198,30 @@ namespace Microsoft.Boogie.AbstractInterpretation
}
}
return e;
+ } else {
+ Contract.Assert(V.TypedIdent.Type.IsFloat);
+ Expr e = Expr.True;
+ if (Lo != null && Hi != null && Lo == Hi)
+ {
+ // produce an equality
+ var ide = new IdentifierExpr(Token.NoToken, V);
+ e = Expr.And(e, BplEq(ide, NumberToExpr((BigInteger)Lo, V.TypedIdent.Type)));
+ }
+ else
+ {
+ // produce a (possibly empty) conjunction of inequalities
+ if (Lo != null)
+ {
+ var ide = new IdentifierExpr(Token.NoToken, V);
+ e = Expr.And(e, BplLe(NumberToExpr((BigInteger)Lo, V.TypedIdent.Type), ide));
+ }
+ if (Hi != null)
+ {
+ var ide = new IdentifierExpr(Token.NoToken, V);
+ e = Expr.And(e, BplLe(ide, NumberToExpr((BigInteger)Hi, V.TypedIdent.Type)));
+ }
+ }
+ return e;
}
}
}
@@ -208,6 +231,8 @@ namespace Microsoft.Boogie.AbstractInterpretation
return null;
} else if (ty.IsReal) {
return Expr.Literal(Basetypes.BigDec.FromBigInt(n));
+ } else if (ty.IsFloat) {
+ return Expr.Literal(Basetypes.BigFloat.FromBigInt(n, ty.FloatExponent, ty.FloatSignificand));
} else {
Contract.Assume(ty.IsInt);
return Expr.Literal(Basetypes.BigNum.FromBigInt(n));
@@ -669,6 +694,11 @@ namespace Microsoft.Boogie.AbstractInterpretation
((BigDec)node.Val).FloorCeiling(out floor, out ceiling);
Lo = floor;
Hi = ceiling;
+ } else if (node.Val is BigFloat) {
+ BigInteger floor, ceiling;
+ ((BigFloat)node.Val).FloorCeiling(out floor, out ceiling);
+ Lo = floor;
+ Hi = ceiling;
} else if (node.Val is bool) {
if ((bool)node.Val) {
// true
diff --git a/Source/Basetypes/Basetypes.csproj b/Source/Basetypes/Basetypes.csproj
index 5e46877a..5b425bc5 100644
--- a/Source/Basetypes/Basetypes.csproj
+++ b/Source/Basetypes/Basetypes.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
@@ -9,7 +9,7 @@
<OutputType>Library</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>Basetypes</RootNamespace>
- <AssemblyName>Basetypes</AssemblyName>
+ <AssemblyName>BoogieBasetypes</AssemblyName>
<TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
<CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
@@ -34,7 +34,7 @@
<IsWebBootstrapper>false</IsWebBootstrapper>
<UseApplicationTrust>false</UseApplicationTrust>
<BootstrapperEnabled>true</BootstrapperEnabled>
- <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile>
+ <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
@@ -163,6 +163,7 @@
</Compile>
<Compile Include="BigDec.cs" />
<Compile Include="BigNum.cs" />
+ <Compile Include="BigFloat.cs" />
<Compile Include="Rational.cs" />
<Compile Include="Set.cs" />
</ItemGroup>
@@ -200,4 +201,4 @@
<Target Name="AfterBuild">
</Target>
-->
-</Project>
+</Project> \ No newline at end of file
diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs
new file mode 100644
index 00000000..cb248340
--- /dev/null
+++ b/Source/Basetypes/BigFloat.cs
@@ -0,0 +1,509 @@
+//-----------------------------------------------------------------------------
+//
+// 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));
+ isNeg = s[0] == '-'; //We do this so that -0 is parsed correctly
+
+ 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
+ sig = BIM.Abs(sig); //sig must be positive
+ //Uncomment if you want to shift the exponent for the user (i.e. 0e-1f24e8 --> 0e126f24e8)
+ //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-1) + 1;
+
+ while (exp > BIM.Zero) {
+ exp--;
+ sig = sig << 1;
+ }
+
+ sig = sig >> SignificandSize;
+
+ 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/CodeContractsExtender/CodeContractsExtender.csproj b/Source/CodeContractsExtender/CodeContractsExtender.csproj
index 05701c12..38535dc4 100644
--- a/Source/CodeContractsExtender/CodeContractsExtender.csproj
+++ b/Source/CodeContractsExtender/CodeContractsExtender.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
@@ -9,7 +9,7 @@
<OutputType>Library</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>CodeContractsExtender</RootNamespace>
- <AssemblyName>CodeContractsExtender</AssemblyName>
+ <AssemblyName>BoogieCodeContractsExtender</AssemblyName>
<TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
<SignAssembly>true</SignAssembly>
@@ -34,7 +34,7 @@
<IsWebBootstrapper>false</IsWebBootstrapper>
<UseApplicationTrust>false</UseApplicationTrust>
<BootstrapperEnabled>true</BootstrapperEnabled>
- <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile>
+ <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
@@ -199,4 +199,4 @@
<Target Name="AfterBuild">
</Target>
-->
-</Project>
+</Project> \ No newline at end of file
diff --git a/Source/Concurrency/Concurrency.csproj b/Source/Concurrency/Concurrency.csproj
index 113019fd..ac90077c 100644
--- a/Source/Concurrency/Concurrency.csproj
+++ b/Source/Concurrency/Concurrency.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
<PropertyGroup>
@@ -8,7 +8,7 @@
<OutputType>Library</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>Concurrency</RootNamespace>
- <AssemblyName>Concurrency</AssemblyName>
+ <AssemblyName>BoogieConcurrency</AssemblyName>
<TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
<TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>
@@ -112,4 +112,4 @@
<Target Name="AfterBuild">
</Target>
-->
-</Project>
+</Project> \ No newline at end of file
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 7ffd5f7f..409254d0 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -313,6 +313,13 @@ namespace Microsoft.Boogie {
Contract.Ensures(Contract.Result<NAryExpr>() != null);
return Binary(BinaryOperator.Opcode.RealDiv, e1, e2);
}
+ public static NAryExpr FloatDiv(Expr e1, Expr e2)
+ {
+ Contract.Requires(e2 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+ return Binary(BinaryOperator.Opcode.FloatDiv, e1, e2);
+ }
public static NAryExpr Pow(Expr e1, Expr e2) {
Contract.Requires(e2 != null);
Contract.Requires(e1 != null);
@@ -356,6 +363,11 @@ namespace Microsoft.Boogie {
Contract.Ensures(Contract.Result<LiteralExpr>() != null);
return new LiteralExpr(Token.NoToken, value);
}
+ public static LiteralExpr Literal(BigFloat value)
+ {
+ Contract.Ensures(Contract.Result<LiteralExpr>() != null);
+ return new LiteralExpr(Token.NoToken, value);
+ }
private static LiteralExpr/*!*/ true_ = Literal(true);
public static LiteralExpr/*!*/ True {
@@ -514,7 +526,7 @@ namespace Microsoft.Boogie {
}
public class LiteralExpr : Expr {
- public readonly object/*!*/ Val; // false, true, a BigNum, a BigDec, or a BvConst
+ public readonly object/*!*/ Val; // false, true, a BigNum, a BigDec, a BigFloat, or a BvConst
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Val != null);
@@ -563,6 +575,21 @@ namespace Microsoft.Boogie {
}
/// <summary>
+ /// Creates a literal expression for the floating point value "v".
+ /// </summary>
+ /// <param name="tok"></param>
+ /// <param name="v"></param>
+ public LiteralExpr(IToken/*!*/ tok, BigFloat v, bool immutable = false)
+ : base(tok, immutable)
+ {
+ Contract.Requires(tok != null);
+ Val = v;
+ Type = Type.GetFloatType(v.SignificandSize, v.ExponentSize);
+ if (immutable)
+ CachedHashCode = ComputeHashCode();
+ }
+
+ /// <summary>
/// Creates a literal expression for the bitvector value "v".
/// </summary>
public LiteralExpr(IToken/*!*/ tok, BigNum v, int b, bool immutable=false)
@@ -633,6 +660,9 @@ namespace Microsoft.Boogie {
return Type.Int;
} else if (Val is BigDec) {
return Type.Real;
+ } else if (Val is BigFloat) {
+ BigFloat temp = (BigFloat)Val;
+ return Type.GetFloatType(temp.SignificandSize, temp.ExponentSize);
} else if (Val is BvConst) {
return Type.GetBvType(((BvConst)Val).Bits);
} else {
@@ -681,6 +711,14 @@ namespace Microsoft.Boogie {
}
}
+ public bool isBigFloat
+ {
+ get
+ {
+ return Val is BigFloat;
+ }
+ }
+
public BigDec asBigDec {
get {
Contract.Assert(isBigDec);
@@ -688,6 +726,13 @@ namespace Microsoft.Boogie {
}
}
+ public BigFloat asBigFloat {
+ get {
+ Contract.Assert(isBigFloat);
+ return (BigFloat)cce.NonNull(Val);
+ }
+ }
+
public bool isBool {
get {
return Val is bool;
@@ -1355,6 +1400,9 @@ namespace Microsoft.Boogie {
if (arg0type.Unify(Type.Real)) {
return Type.Real;
}
+ //if (arg0type.Unify(Type.Float)) {
+ //return Type.Float;
+ //}
goto BAD_TYPE;
case Opcode.Not:
if (arg0type.Unify(Type.Bool)) {
@@ -1399,6 +1447,9 @@ namespace Microsoft.Boogie {
if (argument is BigDec) {
return -((BigDec)argument);
}
+ if (argument is BigFloat) {
+ return -((BigFloat)argument);
+ }
break;
case Opcode.Not:
if (argument is bool) {
@@ -1431,6 +1482,7 @@ namespace Microsoft.Boogie {
Div,
Mod,
RealDiv,
+ FloatDiv,
Pow,
Eq,
Neq,
@@ -1671,6 +1723,12 @@ namespace Microsoft.Boogie {
if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {
return Type.Real;
}
+ if (arg0type.IsFloat && arg0type.Unify(arg1type)) {
+ return Type.GetFloatType(arg0.Type.FloatSignificand, arg0.Type.FloatExponent);
+ }
+ if (arg1type.IsFloat && arg1type.Unify(arg0type)) {
+ return Type.GetFloatType(arg1.Type.FloatSignificand, arg1.Type.FloatExponent);
+ }
goto BAD_TYPE;
case Opcode.Div:
case Opcode.Mod:
@@ -1683,6 +1741,12 @@ namespace Microsoft.Boogie {
(arg1type.Unify(Type.Int) || arg1type.Unify(Type.Real))) {
return Type.Real;
}
+ if (arg0type.IsFloat && arg0type.Unify(arg1type)) {
+ return Type.GetFloatType(arg0.Type.FloatSignificand, arg0.Type.FloatExponent);
+ }
+ if (arg1type.IsFloat && arg1type.Unify(arg0type)) {
+ return Type.GetFloatType(arg1.Type.FloatSignificand, arg1.Type.FloatExponent);
+ }
goto BAD_TYPE;
case Opcode.Pow:
if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {
@@ -1715,6 +1779,9 @@ namespace Microsoft.Boogie {
if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {
return Type.Bool;
}
+ if ((arg0type.IsFloat && arg0type.Unify(arg1type)) || (arg1type.IsFloat && arg1type.Unify(arg0type))) {
+ return Type.Bool;
+ }
goto BAD_TYPE;
case Opcode.And:
case Opcode.Or:
@@ -1825,6 +1892,9 @@ namespace Microsoft.Boogie {
if (e1 is BigDec && e2 is BigDec) {
return ((BigDec)e1) + ((BigDec)e2);
}
+ if (e1 is BigFloat && e2 is BigFloat) {
+ return ((BigFloat)e1) + ((BigFloat)e2);
+ }
break;
case Opcode.Sub:
if (e1 is BigNum && e2 is BigNum) {
@@ -1833,6 +1903,9 @@ namespace Microsoft.Boogie {
if (e1 is BigDec && e2 is BigDec) {
return ((BigDec)e1) - ((BigDec)e2);
}
+ if (e1 is BigFloat && e2 is BigFloat) {
+ return ((BigFloat)e1) - ((BigFloat)e2);
+ }
break;
case Opcode.Mul:
if (e1 is BigNum && e2 is BigNum) {
@@ -1841,6 +1914,9 @@ namespace Microsoft.Boogie {
if (e1 is BigDec && e2 is BigDec) {
return ((BigDec)e1) * ((BigDec)e2);
}
+ if (e1 is BigFloat && e2 is BigFloat) {
+ return ((BigFloat)e1) * ((BigFloat)e2);
+ }
break;
case Opcode.Div:
if (e1 is BigNum && e2 is BigNum) {
@@ -1855,6 +1931,9 @@ namespace Microsoft.Boogie {
case Opcode.RealDiv:
// TODO: add partial evaluation fro real division
break;
+ case Opcode.FloatDiv:
+ //TODO: add float division
+ break;
case Opcode.Pow:
// TODO: add partial evaluation fro real exponentiation
break;
@@ -1865,6 +1944,9 @@ namespace Microsoft.Boogie {
if (e1 is BigDec && e2 is BigDec) {
return ((BigDec)e1) < ((BigDec)e2);
}
+ if (e1 is BigFloat && e2 is BigFloat) {
+ return ((BigFloat)e1) < ((BigFloat)e2);
+ }
break;
case Opcode.Le:
if (e1 is BigNum && e2 is BigNum) {
@@ -1873,6 +1955,9 @@ namespace Microsoft.Boogie {
if (e1 is BigDec && e2 is BigDec) {
return ((BigDec)e1) <= ((BigDec)e2);
}
+ if (e1 is BigFloat && e2 is BigFloat) {
+ return ((BigFloat)e1) <= ((BigFloat)e2);
+ }
break;
case Opcode.Gt:
if (e1 is BigNum && e2 is BigNum) {
@@ -1881,6 +1966,9 @@ namespace Microsoft.Boogie {
if (e1 is BigDec && e2 is BigDec) {
return ((BigDec)e1) > ((BigDec)e2);
}
+ if (e1 is BigFloat && e2 is BigFloat) {
+ return ((BigFloat)e1) > ((BigFloat)e2);
+ }
break;
case Opcode.Ge:
if (e1 is BigNum && e2 is BigNum) {
@@ -1889,6 +1977,9 @@ namespace Microsoft.Boogie {
if (e1 is BigDec && e2 is BigDec) {
return ((BigDec)e1) >= ((BigDec)e2);
}
+ if (e1 is BigFloat && e2 is BigFloat) {
+ return ((BigFloat)e1) >= ((BigFloat)e2);
+ }
break;
case Opcode.And:
@@ -1990,7 +2081,7 @@ namespace Microsoft.Boogie {
}
else
{
- this.name.Emit(stream, 0xF0, false);
+ this.name.Emit(stream, 0xF0, false);
}
if (stream.UseForComputingChecksums)
{
@@ -2177,7 +2268,8 @@ namespace Microsoft.Boogie {
public class ArithmeticCoercion : IAppliable {
public enum CoercionType {
ToInt,
- ToReal
+ ToReal,
+ ToFloat
}
private IToken/*!*/ tok;
diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index 2953f15e..ab6ef5e9 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -244,6 +244,11 @@ namespace Microsoft.Boogie {
return false;
}
}
+ public virtual bool IsFloat {
+ get {
+ return false;
+ }
+ }
public virtual bool IsBool {
get {
return false;
@@ -320,6 +325,29 @@ namespace Microsoft.Boogie {
}
}
+ public virtual bool isFloat {
+ get {
+ return false;
+ }
+ }
+ public virtual int FloatExponent
+ {
+ get
+ {
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // Type.FloatExponent should never be called
+ }
+ }
+ public virtual int FloatSignificand {
+ get {
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // Type.FloatSignificand should never be called
+ }
+ }
public virtual bool IsBv {
get {
return false;
@@ -358,6 +386,14 @@ namespace Microsoft.Boogie {
}
}
+ static public FloatType GetFloatType(int sig, int exp) {
+ Contract.Requires(0 <= exp);
+ Contract.Requires(0 <= sig);
+ Contract.Ensures(Contract.Result<FloatType>() != null);
+
+ return new FloatType(sig, exp);
+ }
+
//------------ Match formal argument types on actual argument types
//------------ and return the resulting substitution of type variables
@@ -1008,6 +1044,165 @@ namespace Microsoft.Boogie {
//=====================================================================
+ //Note that the functions in this class were directly copied from the BV class just below
+ public class FloatType : Type {
+ public readonly int Significand; //Size of Significand in bits
+ public readonly int Exponent; //Size of exponent in bits
+
+ public FloatType(IToken token, int significand, int exponent)
+ : base(token) {
+ Contract.Requires(token != null);
+ Significand = significand;
+ Exponent = exponent;
+ }
+
+ public FloatType(int significand, int exponent)
+ : base(Token.NoToken) {
+ Significand = significand;
+ Exponent = exponent;
+ }
+
+ //----------- Cloning ----------------------------------
+ // We implement our own clone-method, because bound type variables
+ // have to be created in the right way. It is /not/ ok to just clone
+ // everything recursively.
+
+ public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap)
+ {
+ //Contract.Requires(cce.NonNullElements(varMap));
+ Contract.Ensures(Contract.Result<Type>() != null);
+ // FloatTypes are immutable anyway, we do not clone
+ return this;
+ }
+
+ public override Type CloneUnresolved()
+ {
+ Contract.Ensures(Contract.Result<Type>() != null);
+ return this;
+ }
+
+ //----------- Linearisation ----------------------------------
+
+ public override void Emit(TokenTextWriter stream, int contextBindingStrength)
+ {
+ //Contract.Requires(stream != null);
+ // no parentheses are necessary for bitvector-types
+ stream.SetToken(this);
+ stream.Write("{0}", this);
+ }
+
+ public override string ToString()
+ {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return "float" + Significand + "e" + Exponent;
+ }
+
+ //----------- Equality ----------------------------------
+
+ [Pure]
+ public override bool Equals(Type/*!*/ that,
+ List<TypeVariable>/*!*/ thisBoundVariables,
+ List<TypeVariable>/*!*/ thatBoundVariables)
+ {
+ FloatType thatFloatType = TypeProxy.FollowProxy(that.Expanded) as FloatType;
+ return thatFloatType != null && this.Significand == thatFloatType.Significand && this.Exponent == thatFloatType.Exponent;
+ }
+
+ //----------- Unification of types -----------
+
+ public override bool Unify(Type/*!*/ that,
+ List<TypeVariable>/*!*/ unifiableVariables,
+ // an idempotent substitution that describes the
+ // unification result up to a certain point
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier)
+ {
+ //Contract.Requires(that != null);
+ //Contract.Requires(unifiableVariables != null);
+ //Contract.Requires(cce.NonNullElements(unifier));
+ that = that.Expanded;
+ if (that is TypeProxy || that is TypeVariable) {
+ return that.Unify(this, unifiableVariables, unifier);
+ }
+ else {
+ return this.Equals(that);
+ }
+ }
+
+ //----------- Substitution of free variables with types not containing bound variables -----------------
+
+ public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst)
+ {
+ Contract.Ensures(Contract.Result<Type>() != null);
+ return this;
+ }
+
+ //----------- Hashcodes ----------------------------------
+
+ [Pure]
+ public override int GetHashCode(List<TypeVariable> boundVariables)
+ {
+ return this.Significand.GetHashCode() + this.Exponent.GetHashCode();
+ }
+
+ //----------- Resolution ----------------------------------
+
+ public override Type ResolveType(ResolutionContext rc)
+ {
+ //Contract.Requires(rc != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
+ // nothing to resolve
+ return this;
+ }
+
+ // determine the free variables in a type, in the order in which the variables occur
+ public override List<TypeVariable>/*!*/ FreeVariables
+ {
+ get
+ {
+ Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);
+
+ return new List<TypeVariable>(); // bitvector-type are closed
+ }
+ }
+
+ public override List<TypeProxy/*!*/>/*!*/ FreeProxies
+ {
+ get
+ {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeProxy>>()));
+ return new List<TypeProxy/*!*/>();
+ }
+ }
+
+ //----------- Getters/Issers ----------------------------------
+
+ public override bool IsFloat {
+ get {
+ return true;
+ }
+ }
+ public override int FloatSignificand {
+ get {
+ return Significand;
+ }
+ }
+ public override int FloatExponent {
+ get {
+ return Exponent;
+ }
+ }
+
+ public override Absy StdDispatch(StandardVisitor visitor)
+ {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
+ return visitor.VisitFloatType(this);
+ }
+
+ }
+
+ //=====================================================================
+
public class BvType : Type {
public readonly int Bits;
@@ -1286,7 +1481,7 @@ Contract.Requires(that != null);
public override Type ResolveType(ResolutionContext rc) {
//Contract.Requires(rc != null);
Contract.Ensures(Contract.Result<Type>() != null);
- // first case: the type name denotes a bitvector-type
+ // first case: the type name denotes a bitvector-type or float-type
if (Name.StartsWith("bv") && Name.Length > 2) {
bool is_bv = true;
for (int i = 2; i < Name.Length; ++i) {
@@ -1305,6 +1500,28 @@ Contract.Requires(that != null);
}
}
+ if (Name.StartsWith("float") && Name.Length > 5)
+ {
+ bool is_float = true;
+ int i = 5;
+ for (; is_float && Name[i] != 'e'; i++)
+ if (i >= Name.Length-1 || !char.IsDigit(Name[i])) //There must be an e
+ is_float = false;
+ int mid = i;
+ i++;
+ for (; i < Name.Length && is_float; i++)
+ if (!char.IsDigit(Name[i]))
+ is_float = false;
+ if (is_float) {
+ if (Arguments.Count > 0) {
+ rc.Error(this,
+ "float types must not be applied to arguments: {0}",
+ Name);
+ }
+ return new FloatType(tok, int.Parse(Name.Substring(5, mid-5)), int.Parse(Name.Substring(mid+1)));
+ }
+ }
+
// second case: the identifier is resolved to a type variable
TypeVariable var = rc.LookUpTypeBinder(Name);
if (var != null) {
@@ -1899,6 +2116,12 @@ Contract.Requires(that != null);
return p != null && p.IsReal;
}
}
+ public override bool IsFloat {
+ get {
+ Type p = ProxyFor;
+ return p != null && p.IsFloat;
+ }
+ }
public override bool IsBool {
get {
Type p = ProxyFor;
@@ -2747,11 +2970,20 @@ Contract.Requires(that != null);
return ExpandedType.IsInt;
}
}
- public override bool IsReal {
- get {
+ public override bool IsReal
+ {
+ get
+ {
return ExpandedType.IsReal;
}
}
+ public override bool IsFloat
+ {
+ get
+ {
+ return ExpandedType.IsFloat;
+ }
+ }
public override bool IsBool {
get {
return ExpandedType.IsBool;
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 091ceeb0..f74f8bff 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -144,7 +144,12 @@ 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}
+ | '0' 'N' 'a' 'N' digit {digit} 'e' digit {digit}
+ | '0' 'n' 'a' 'n' digit {digit} 'e' digit {digit}
+ | '0' '+' 'o' 'o' digit {digit} 'e' digit {digit}
+ | '0' '-' 'o' 'o' digit {digit} 'e' digit {digit} .
COMMENTS FROM "/*" TO "*/" NESTED
COMMENTS FROM "//" TO lf
@@ -330,7 +335,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 +1257,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 +1270,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; .)
@@ -1290,7 +1296,7 @@ AtomExpression<out Expr/*!*/ e>
Expression<out e>
")" (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List<Expr>{ e }); .)
- | "(" ( Expression<out e> (. if (e is BvBounds)
+ | "(" ( Expression<out e> (. if (e is BvBounds)
this.SemErr("parentheses around bitvector bounds " +
"are not allowed"); .)
| Forall (. x = t; .)
@@ -1479,7 +1485,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 +1514,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 e) {
+ this.SemErr("incorrectly formatted floating point, " + e.Message);
+ n = BigFloat.ZERO;
+ }
+ .)
+ .
+
END BoogiePL.
diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj
index 36bcc6c3..7c4cb7ae 100644
--- a/Source/Core/Core.csproj
+++ b/Source/Core/Core.csproj
@@ -9,7 +9,7 @@
<OutputType>Library</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>Core</RootNamespace>
- <AssemblyName>Core</AssemblyName>
+ <AssemblyName>BoogieCore</AssemblyName>
<TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
<CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
@@ -34,7 +34,7 @@
<IsWebBootstrapper>false</IsWebBootstrapper>
<UseApplicationTrust>false</UseApplicationTrust>
<BootstrapperEnabled>true</BootstrapperEnabled>
- <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile>
+ <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
@@ -186,7 +186,7 @@
</ItemGroup>
<ItemGroup>
<ProjectReference Include="..\Basetypes\Basetypes.csproj">
- <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
+ <Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project>
<Name>Basetypes</Name>
</ProjectReference>
<ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj">
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 793bb96e..c91de177 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;
@@ -132,7 +133,8 @@ 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();
}
}
@@ -219,7 +221,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);
@@ -228,7 +230,7 @@ private class BvBounds : Expr {
break;
}
- case 25: {
+ case 26: {
Function(out ds);
foreach(Bpl.Declaration/*!*/ d in ds){
Contract.Assert(d != null);
@@ -237,12 +239,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);
@@ -251,7 +253,7 @@ private class BvBounds : Expr {
break;
}
- case 7: {
+ case 8: {
GlobalVars(out vs);
foreach(Bpl.Variable/*!*/ v in vs){
Contract.Assert(v != null);
@@ -260,7 +262,7 @@ private class BvBounds : Expr {
break;
}
- case 32: {
+ case 33: {
Procedure(out pr, out im);
Pgm.AddTopLevelDeclaration(pr);
if (im != null) {
@@ -269,7 +271,7 @@ private class BvBounds : Expr {
break;
}
- case 33: {
+ case 34: {
Implementation(out nnim);
Pgm.AddTopLevelDeclaration(nnim);
break;
@@ -285,17 +287,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;
@@ -319,7 +321,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) {
@@ -336,44 +338,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));
@@ -428,30 +430,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) {
@@ -460,12 +462,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) {
@@ -481,9 +483,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);
@@ -496,7 +498,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);
}
@@ -508,7 +510,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);
@@ -522,7 +524,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);
}
@@ -532,12 +534,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) {
@@ -546,16 +548,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);
}
@@ -574,7 +576,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){
@@ -588,7 +590,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);
@@ -606,14 +608,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;
@@ -627,9 +629,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) {
@@ -649,7 +651,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);
@@ -659,20 +661,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) {
@@ -699,10 +701,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) {
@@ -712,16 +714,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);
@@ -729,10 +731,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);
@@ -744,7 +746,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);
@@ -756,21 +758,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;
}
@@ -779,7 +781,7 @@ private class BvBounds : Expr {
new IdentifierExpr(parent, parent.val), u));
}
}
- if (la.kind == 24) {
+ if (la.kind == 25) {
Get();
ChildrenComplete = true;
}
@@ -792,12 +794,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) {
@@ -823,7 +825,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;
@@ -855,15 +857,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);
}
@@ -871,7 +873,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);
@@ -881,19 +883,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);
@@ -901,25 +903,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) {
@@ -956,7 +958,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>(); }
@@ -976,7 +978,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>();
@@ -1004,33 +1006,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);
@@ -1040,25 +1042,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;
}
}
@@ -1066,16 +1068,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) {
@@ -1083,7 +1085,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);
@@ -1092,11 +1094,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) {
@@ -1106,21 +1108,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);
}
@@ -1132,18 +1134,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);
@@ -1154,9 +1156,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);
}
@@ -1165,27 +1167,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) {
@@ -1198,40 +1200,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) {
@@ -1242,17 +1244,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);
@@ -1266,19 +1268,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);
}
@@ -1286,18 +1288,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) {
@@ -1309,53 +1311,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);
@@ -1366,7 +1368,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);
@@ -1378,7 +1380,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);
@@ -1389,23 +1391,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);
@@ -1416,7 +1418,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);
@@ -1427,19 +1429,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) {
@@ -1453,25 +1455,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);
@@ -1482,64 +1484,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);
@@ -1558,19 +1560,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);
@@ -1580,46 +1582,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) {
@@ -1628,7 +1630,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)) {
@@ -1643,7 +1645,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);
}
}
@@ -1654,7 +1656,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);
@@ -1667,7 +1669,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)
@@ -1675,7 +1677,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)
@@ -1689,7 +1691,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)
@@ -1714,7 +1716,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;
@@ -1724,12 +1726,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;
@@ -1744,6 +1746,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);
@@ -1752,65 +1759,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);
@@ -1818,20 +1825,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;
}
}
@@ -1843,7 +1850,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) {
@@ -1853,6 +1860,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");
@@ -1870,11 +1890,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,
@@ -1885,35 +1905,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) {
@@ -1921,12 +1941,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 });
}
@@ -1935,8 +1955,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);
@@ -1945,7 +1965,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) {
@@ -1958,7 +1978,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) {
@@ -1970,7 +1990,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
}
}
- if (la.kind == 38) {
+ if (la.kind == 39) {
Get();
y = t;
Idents(out xs);
@@ -1979,12 +1999,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) {
@@ -1992,16 +2012,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);
@@ -2029,7 +2049,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);
@@ -2040,8 +2060,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) {
@@ -2055,15 +2075,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);
}
@@ -2079,23 +2099,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
@@ -2126,135 +2146,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..46a3c419 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,42 @@ 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 = 49; i <= 57; ++i) start[i] = 45;
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[45] = 87;
+ start[48] = 46;
+ start[59] = 52;
+ start[40] = 53;
+ start[41] = 54;
+ start[58] = 88;
+ start[44] = 55;
+ start[91] = 56;
+ start[93] = 57;
+ start[60] = 89;
+ start[62] = 90;
+ start[123] = 58;
+ start[125] = 91;
+ start[61] = 92;
+ start[42] = 93;
+ start[124] = 94;
+ start[8660] = 61;
+ start[8658] = 63;
+ start[8656] = 64;
+ start[38] = 65;
+ start[8743] = 67;
+ start[8744] = 69;
+ start[33] = 95;
+ start[8800] = 73;
+ start[8804] = 74;
+ start[8805] = 75;
+ start[43] = 96;
+ start[47] = 77;
+ start[172] = 79;
+ start[8704] = 82;
+ start[8707] = 83;
+ start[955] = 84;
+ start[8226] = 86;
start[Buffer.EOF] = -1;
}
@@ -503,48 +504,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 +598,305 @@ 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 47;}
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;}
+ recEnd = pos; recKind = 6;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;}
+ else if (ch == 'e') {AddCh(); goto case 10;}
+ else {t.kind = 6; break;}
case 10:
- recEnd = pos; recKind = 5;
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;}
- else {t.kind = 5; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;}
+ else if (ch == '-') {AddCh(); goto case 11;}
+ else {goto case 0;}
case 11:
if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;}
else {goto case 0;}
case 12:
recEnd = pos; recKind = 6;
if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;}
- else if (ch == 'e') {AddCh(); goto case 13;}
else {t.kind = 6; break;}
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 13;}
+ else if (ch == 'e') {AddCh(); goto case 14;}
else {goto case 0;}
case 14:
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;}
+ else if (ch == '-') {AddCh(); goto case 15;}
else {goto case 0;}
case 15:
- recEnd = pos; recKind = 6;
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;}
- else {t.kind = 6; break;}
+ 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 == 'b') {AddCh(); goto case 3;}
- else if (ch == 'e') {AddCh(); goto case 8;}
- else if (ch == '.') {AddCh(); goto case 11;}
- else {t.kind = 3; break;}
+ else if (ch == 'f') {AddCh(); goto case 17;}
+ else {goto case 0;}
case 17:
- if (ch == '"') {AddCh(); goto case 18;}
- 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;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;}
else {goto case 0;}
case 18:
- 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 {t.kind = 4; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;}
+ else if (ch == 'e') {AddCh(); goto case 19;}
+ else {goto case 0;}
case 19:
- {t.kind = 8; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 20;}
+ else {goto case 0;}
case 20:
- {t.kind = 9; break;}
+ recEnd = pos; recKind = 7;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 20;}
+ else {t.kind = 7; break;}
case 21:
- {t.kind = 10; break;}
+ if (ch == 'a') {AddCh(); goto case 22;}
+ else {goto case 0;}
case 22:
- {t.kind = 12; break;}
+ if (ch == 'N') {AddCh(); goto case 23;}
+ else {goto case 0;}
case 23:
- {t.kind = 17; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 24;}
+ else {goto case 0;}
case 24:
- {t.kind = 18; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 24;}
+ else if (ch == 'e') {AddCh(); goto case 25;}
+ else {goto case 0;}
case 25:
- {t.kind = 27; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 26;}
+ else {goto case 0;}
case 26:
- {t.kind = 50; break;}
+ recEnd = pos; recKind = 7;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 26;}
+ else {t.kind = 7; break;}
case 27:
- {t.kind = 55; break;}
+ if (ch == 'a') {AddCh(); goto case 28;}
+ else {goto case 0;}
case 28:
- {t.kind = 56; break;}
+ if (ch == 'n') {AddCh(); goto case 29;}
+ else {goto case 0;}
case 29:
- {t.kind = 57; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 30;}
+ else {goto case 0;}
case 30:
- {t.kind = 58; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 30;}
+ else if (ch == 'e') {AddCh(); goto case 31;}
+ else {goto case 0;}
case 31:
- {t.kind = 60; break;}
- case 32:
- if (ch == '&') {AddCh(); goto case 33;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 32;}
else {goto case 0;}
+ case 32:
+ recEnd = pos; recKind = 7;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 32;}
+ else {t.kind = 7; break;}
case 33:
- {t.kind = 61; break;}
+ if (ch == 'o') {AddCh(); goto case 34;}
+ else {goto case 0;}
case 34:
- {t.kind = 62; break;}
+ if (ch == 'o') {AddCh(); goto case 35;}
+ else {goto case 0;}
case 35:
- {t.kind = 63; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 36;}
+ else {goto case 0;}
case 36:
- {t.kind = 64; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 36;}
+ else if (ch == 'e') {AddCh(); goto case 37;}
+ else {goto case 0;}
case 37:
- {t.kind = 67; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 38;}
+ else {goto case 0;}
case 38:
- {t.kind = 68; break;}
+ recEnd = pos; recKind = 7;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 38;}
+ else {t.kind = 7; break;}
case 39:
- {t.kind = 69; break;}
+ if (ch == 'o') {AddCh(); goto case 40;}
+ else {goto case 0;}
case 40:
- {t.kind = 70; break;}
+ if (ch == 'o') {AddCh(); goto case 41;}
+ else {goto case 0;}
case 41:
- {t.kind = 71; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 42;}
+ else {goto case 0;}
case 42:
- {t.kind = 72; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 42;}
+ else if (ch == 'e') {AddCh(); goto case 43;}
+ else {goto case 0;}
case 43:
- {t.kind = 73; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 44;}
+ else {goto case 0;}
case 44:
- {t.kind = 75; break;}
+ recEnd = pos; recKind = 7;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 44;}
+ else {t.kind = 7; break;}
case 45:
- {t.kind = 78; break;}
+ recEnd = pos; recKind = 3;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 45;}
+ else if (ch == 'b') {AddCh(); goto case 3;}
+ else if (ch == 'e') {AddCh(); goto case 48;}
+ else if (ch == '.') {AddCh(); goto case 8;}
+ else {t.kind = 3; break;}
case 46:
- {t.kind = 79; break;}
+ recEnd = pos; recKind = 3;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 45;}
+ else if (ch == 'b') {AddCh(); goto case 3;}
+ else if (ch == 'e') {AddCh(); goto case 48;}
+ else if (ch == '.') {AddCh(); goto case 8;}
+ else if (ch == 'N') {AddCh(); goto case 21;}
+ else if (ch == 'n') {AddCh(); goto case 27;}
+ else if (ch == '+') {AddCh(); goto case 33;}
+ else if (ch == '-') {AddCh(); goto case 39;}
+ else {t.kind = 3; break;}
case 47:
- {t.kind = 81; break;}
+ if (ch == '"') {AddCh(); goto case 49;}
+ 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 47;}
+ else {goto case 0;}
case 48:
- {t.kind = 85; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 50;}
+ else if (ch == '-') {AddCh(); goto case 51;}
+ else {goto case 0;}
case 49:
- {t.kind = 86; break;}
+ 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 47;}
+ else {t.kind = 4; break;}
case 50:
- {t.kind = 89; break;}
+ recEnd = pos; recKind = 5;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 50;}
+ else if (ch == 'f') {AddCh(); goto case 17;}
+ else {t.kind = 5; break;}
case 51:
- {t.kind = 91; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 50;}
+ else {goto case 0;}
case 52:
- {t.kind = 93; break;}
+ {t.kind = 9; break;}
case 53:
- {t.kind = 94; break;}
+ {t.kind = 10; break;}
case 54:
- {t.kind = 95; break;}
+ {t.kind = 11; 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 = 13; 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 = 18; break;}
case 57:
- recEnd = pos; recKind = 20;
- if (ch == '=') {AddCh(); goto case 37;}
- else {t.kind = 20; break;}
+ {t.kind = 19; break;}
case 58:
- recEnd = pos; recKind = 28;
- if (ch == '|') {AddCh(); goto case 49;}
- else {t.kind = 28; break;}
+ {t.kind = 28; break;}
case 59:
- recEnd = pos; recKind = 31;
- if (ch == '=') {AddCh(); goto case 65;}
- else {t.kind = 31; break;}
+ {t.kind = 51; break;}
case 60:
- recEnd = pos; recKind = 44;
- if (ch == '*') {AddCh(); goto case 46;}
- else {t.kind = 44; break;}
+ {t.kind = 56; 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;}
+ {t.kind = 57; break;}
case 62:
- recEnd = pos; recKind = 80;
- if (ch == '=') {AddCh(); goto case 38;}
- else {t.kind = 80; break;}
+ {t.kind = 58; break;}
case 63:
- recEnd = pos; recKind = 74;
- if (ch == '+') {AddCh(); goto case 43;}
- else {t.kind = 74; break;}
+ {t.kind = 59; break;}
case 64:
- recEnd = pos; recKind = 66;
- if (ch == '=') {AddCh(); goto case 66;}
- else {t.kind = 66; break;}
+ {t.kind = 61; break;}
case 65:
- recEnd = pos; recKind = 65;
- if (ch == '>') {AddCh(); goto case 29;}
- else {t.kind = 65; break;}
+ if (ch == '&') {AddCh(); goto case 66;}
+ else {goto case 0;}
case 66:
- recEnd = pos; recKind = 59;
- if (ch == '>') {AddCh(); goto case 27;}
- else {t.kind = 59; break;}
+ {t.kind = 62; break;}
+ case 67:
+ {t.kind = 63; break;}
+ case 68:
+ {t.kind = 64; break;}
+ case 69:
+ {t.kind = 65; break;}
+ case 70:
+ {t.kind = 68; break;}
+ case 71:
+ {t.kind = 69; break;}
+ case 72:
+ {t.kind = 70; break;}
+ case 73:
+ {t.kind = 71; break;}
+ case 74:
+ {t.kind = 72; break;}
+ case 75:
+ {t.kind = 73; break;}
+ case 76:
+ {t.kind = 74; break;}
+ case 77:
+ {t.kind = 79; break;}
+ case 78:
+ {t.kind = 80; break;}
+ case 79:
+ {t.kind = 82; break;}
+ case 80:
+ {t.kind = 86; break;}
+ case 81:
+ {t.kind = 87; break;}
+ case 82:
+ {t.kind = 90; break;}
+ case 83:
+ {t.kind = 92; break;}
+ case 84:
+ {t.kind = 94; break;}
+ case 85:
+ {t.kind = 95; break;}
+ case 86:
+ {t.kind = 96; break;}
+ case 87:
+ recEnd = pos; recKind = 76;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 13;}
+ else {t.kind = 76; break;}
+ case 88:
+ recEnd = pos; recKind = 12;
+ if (ch == '=') {AddCh(); goto case 59;}
+ else if (ch == ':') {AddCh(); goto case 85;}
+ else {t.kind = 12; break;}
+ case 89:
+ recEnd = pos; recKind = 20;
+ if (ch == '=') {AddCh(); goto case 97;}
+ else if (ch == ':') {AddCh(); goto case 72;}
+ else {t.kind = 20; break;}
+ case 90:
+ recEnd = pos; recKind = 21;
+ if (ch == '=') {AddCh(); goto case 70;}
+ else {t.kind = 21; break;}
+ case 91:
+ recEnd = pos; recKind = 29;
+ if (ch == '|') {AddCh(); goto case 81;}
+ else {t.kind = 29; break;}
+ case 92:
+ recEnd = pos; recKind = 32;
+ if (ch == '=') {AddCh(); goto case 98;}
+ else {t.kind = 32; break;}
+ case 93:
+ recEnd = pos; recKind = 45;
+ if (ch == '*') {AddCh(); goto case 78;}
+ else {t.kind = 45; break;}
+ case 94:
+ recEnd = pos; recKind = 55;
+ if (ch == '|') {AddCh(); goto case 68;}
+ else if (ch == '{') {AddCh(); goto case 80;}
+ else {t.kind = 55; break;}
+ case 95:
+ recEnd = pos; recKind = 81;
+ if (ch == '=') {AddCh(); goto case 71;}
+ else {t.kind = 81; break;}
+ case 96:
+ recEnd = pos; recKind = 75;
+ if (ch == '+') {AddCh(); goto case 76;}
+ else {t.kind = 75; break;}
+ case 97:
+ recEnd = pos; recKind = 67;
+ if (ch == '=') {AddCh(); goto case 99;}
+ else {t.kind = 67; break;}
+ case 98:
+ recEnd = pos; recKind = 66;
+ if (ch == '>') {AddCh(); goto case 62;}
+ else {t.kind = 66; break;}
+ case 99:
+ recEnd = pos; recKind = 60;
+ if (ch == '>') {AddCh(); goto case 60;}
+ else {t.kind = 60; break;}
}
t.val = new String(tval, 0, tlen);
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index c845a589..c3d8a672 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -103,6 +103,12 @@ namespace Microsoft.Boogie {
Contract.Ensures(Contract.Result<Type>() != null);
return this.VisitType(node);
}
+ public virtual Type VisitFloatType(FloatType node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
+ return this.VisitType(node);
+ }
public virtual Expr VisitBvConcatExpr(BvConcatExpr node) {
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Expr>() != null);
diff --git a/Source/Doomed/Doomed.csproj b/Source/Doomed/Doomed.csproj
index c8fb83ad..f055d2c9 100644
--- a/Source/Doomed/Doomed.csproj
+++ b/Source/Doomed/Doomed.csproj
@@ -8,7 +8,7 @@
<OutputType>Library</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>Doomed</RootNamespace>
- <AssemblyName>Doomed</AssemblyName>
+ <AssemblyName>BoogieDoomed</AssemblyName>
<TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
<TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 9bc855be..5a22cc15 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -443,6 +443,8 @@ namespace Microsoft.Boogie
static readonly ConcurrentDictionary<string, CancellationTokenSource> RequestIdToCancellationTokenSource = new ConcurrentDictionary<string, CancellationTokenSource>();
+ static ThreadTaskScheduler Scheduler = new ThreadTaskScheduler(16 * 1024 * 1024);
+
public static void ProcessFiles(List<string> fileNames, bool lookForSnapshots = true, string programId = null)
{
Contract.Requires(cce.NonNullElements(fileNames));
@@ -977,7 +979,7 @@ namespace Microsoft.Boogie
{
break;
}
- tasks[j].Start(TaskScheduler.Default);
+ tasks[j].Start(Scheduler);
}
// Don't wait for tasks that haven't been started yet.
diff --git a/Source/ExecutionEngine/ExecutionEngine.csproj b/Source/ExecutionEngine/ExecutionEngine.csproj
index b0f77125..c715a631 100644
--- a/Source/ExecutionEngine/ExecutionEngine.csproj
+++ b/Source/ExecutionEngine/ExecutionEngine.csproj
@@ -8,7 +8,7 @@
<OutputType>Library</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>ExecutionEngine</RootNamespace>
- <AssemblyName>ExecutionEngine</AssemblyName>
+ <AssemblyName>BoogieExecutionEngine</AssemblyName>
<TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
<TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">
@@ -131,6 +131,7 @@
<ItemGroup>
<Compile Include="ExecutionEngine.cs" />
<Compile Include="Properties\AssemblyInfo.cs" />
+ <Compile Include="ThreadTaskScheduler.cs" />
<Compile Include="VerificationResultCache.cs" />
</ItemGroup>
<ItemGroup>
diff --git a/Source/ExecutionEngine/ThreadTaskScheduler.cs b/Source/ExecutionEngine/ThreadTaskScheduler.cs
new file mode 100644
index 00000000..58c4c6d4
--- /dev/null
+++ b/Source/ExecutionEngine/ThreadTaskScheduler.cs
@@ -0,0 +1,58 @@
+using System;
+using System.Collections.Generic;
+using System.Collections.Concurrent;
+using System.Diagnostics.Contracts;
+using System.Linq;
+using System.Text;
+using System.Threading;
+using System.Threading.Tasks;
+
+namespace Microsoft.Boogie
+{
+ // Implementation of System.Threading.Tasks.TaskScheduler which creates a unique thread per
+ // task, and allows each thread to have its own custom stack size. The standard
+ // scheduler uses the .NET threadpool, which in turn inherits stack size from the EXE.
+ public class ThreadTaskScheduler : TaskScheduler
+ {
+ private int stackSize;
+
+ public ThreadTaskScheduler(int StackReserveSize)
+ {
+ Contract.Requires(StackReserveSize >= 0);
+
+ stackSize = StackReserveSize;
+ }
+
+ protected override IEnumerable<Task> GetScheduledTasks()
+ {
+ // There is never a queue of scheduled, but not running, tasks.
+ // So return an empty list.
+ return new List<Task>();
+ }
+
+ protected override void QueueTask(Task task)
+ {
+ // Each queued task runs on a newly-created thread with the required
+ // stack size. The default .NET task scheduler is built on the .NET
+ // ThreadPool. Its policy allows it to create thousands of threads
+ // if it chooses.
+ //
+ // Boogie creates tasks which in turn create tasks and wait on them.
+ // So throttling tasks via a queue risks deadlock.
+
+ Thread th = new Thread(TaskMain, stackSize);
+ th.Start(task);
+ }
+
+ protected override bool TryExecuteTaskInline(Task task, bool taskWasPreviouslyQueued)
+ {
+ return false;
+ }
+
+ private void TaskMain(object data)
+ {
+ Task t = (Task)data;
+ TryExecuteTask(t);
+ }
+ }
+}
diff --git a/Source/Graph/Graph.csproj b/Source/Graph/Graph.csproj
index 66759719..7e610d46 100644
--- a/Source/Graph/Graph.csproj
+++ b/Source/Graph/Graph.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
@@ -9,7 +9,7 @@
<OutputType>Library</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>Graph</RootNamespace>
- <AssemblyName>Graph</AssemblyName>
+ <AssemblyName>BoogieGraph</AssemblyName>
<TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
<CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
@@ -34,7 +34,7 @@
<IsWebBootstrapper>false</IsWebBootstrapper>
<UseApplicationTrust>false</UseApplicationTrust>
<BootstrapperEnabled>true</BootstrapperEnabled>
- <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile>
+ <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
@@ -196,4 +196,4 @@
<Target Name="AfterBuild">
</Target>
-->
-</Project>
+</Project> \ No newline at end of file
diff --git a/Source/Houdini/Houdini.csproj b/Source/Houdini/Houdini.csproj
index 68ea62e3..43612142 100644
--- a/Source/Houdini/Houdini.csproj
+++ b/Source/Houdini/Houdini.csproj
@@ -9,7 +9,7 @@
<OutputType>Library</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>Microsoft.Boogie.Houdini</RootNamespace>
- <AssemblyName>Houdini</AssemblyName>
+ <AssemblyName>BoogieHoudini</AssemblyName>
<TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
<CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
diff --git a/Source/Model/Model.csproj b/Source/Model/Model.csproj
index dc0ae5e1..c024975f 100644
--- a/Source/Model/Model.csproj
+++ b/Source/Model/Model.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
@@ -9,10 +9,10 @@
<OutputType>Library</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>Microsoft.Boogie</RootNamespace>
- <AssemblyName>Model</AssemblyName>
+ <AssemblyName>BoogieModel</AssemblyName>
<TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
- <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile>
+ <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>
<CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
@@ -106,4 +106,4 @@
<Target Name="AfterBuild">
</Target>
-->
-</Project>
+</Project> \ No newline at end of file
diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj
index b6f47b00..78601afd 100644
--- a/Source/ModelViewer/ModelViewer.csproj
+++ b/Source/ModelViewer/ModelViewer.csproj
@@ -9,9 +9,9 @@
<OutputType>Library</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>Microsoft.Boogie.ModelViewer</RootNamespace>
- <AssemblyName>ModelViewer</AssemblyName>
+ <AssemblyName>BoogieModelViewer</AssemblyName>
<TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
- <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile>
+ <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>
<FileAlignment>512</FileAlignment>
<PublishUrl>publish\</PublishUrl>
<Install>true</Install>
diff --git a/Source/ParserHelper/ParserHelper.csproj b/Source/ParserHelper/ParserHelper.csproj
index 262ca9b7..b5ed2744 100644
--- a/Source/ParserHelper/ParserHelper.csproj
+++ b/Source/ParserHelper/ParserHelper.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
@@ -9,10 +9,10 @@
<OutputType>Library</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>ParserHelper</RootNamespace>
- <AssemblyName>ParserHelper</AssemblyName>
+ <AssemblyName>BoogieParserHelper</AssemblyName>
<TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
- <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile>
+ <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>
<CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
@@ -139,4 +139,4 @@
<Target Name="AfterBuild">
</Target>
-->
-</Project>
+</Project> \ No newline at end of file
diff --git a/Source/Predication/Predication.csproj b/Source/Predication/Predication.csproj
index 803525b3..1319d7f7 100644
--- a/Source/Predication/Predication.csproj
+++ b/Source/Predication/Predication.csproj
@@ -8,7 +8,7 @@
<OutputType>Library</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>Predication</RootNamespace>
- <AssemblyName>Predication</AssemblyName>
+ <AssemblyName>BoogiePredication</AssemblyName>
<TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
<TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>
@@ -171,4 +171,4 @@
<Target Name="AfterBuild">
</Target>
-->
-</Project>
+</Project> \ No newline at end of file
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 06aa5bbe..7b2525f7 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -121,7 +121,7 @@ namespace Microsoft.Boogie.SMTLib
}
sb.Append(']');
TypeToStringHelper(m.Result, sb);
- } else if (t.IsBool || t.IsInt || t.IsReal || t.IsBv) {
+ } else if (t.IsBool || t.IsInt || t.IsReal || t.IsFloat || t.IsBv) {
sb.Append(TypeToString(t));
} else {
System.IO.StringWriter buffer = new System.IO.StringWriter();
@@ -145,6 +145,8 @@ namespace Microsoft.Boogie.SMTLib
return "Int";
else if (t.IsReal)
return "Real";
+ else if (t.IsFloat)
+ return "(_ FloatingPoint " + t.FloatExponent + " " + t.FloatSignificand + ")";
else if (t.IsBv) {
return "(_ BitVec " + t.BvBits + ")";
} else {
@@ -204,6 +206,11 @@ namespace Microsoft.Boogie.SMTLib
else
wr.Write(lit.ToDecimalString());
}
+ else if (node is VCExprFloatLit)
+ {
+ BigFloat lit = ((VCExprFloatLit)node).Val;
+ wr.Write("(" + lit.ToBVString() + ")");
+ }
else {
Contract.Assert(false);
throw new cce.UnreachableException();
@@ -630,6 +637,78 @@ namespace Microsoft.Boogie.SMTLib
return true;
}
+ public bool VisitFloatAddOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.add RNE", node, options);
+ return true;
+ }
+
+ public bool VisitFloatSubOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.sub RNE", node, options);
+ return true;
+ }
+
+ public bool VisitFloatMulOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.mul RNE", node, options);
+ return true;
+ }
+
+ public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.div RNE", node, options);
+ return true;
+ }
+
+ public bool VisitFloatRemOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.rem RNE", node, options);
+ return true;
+ }
+
+ public bool VisitFloatMinOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.min", node, options);
+ return true;
+ }
+
+ public bool VisitFloatMaxOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.max", node, options);
+ return true;
+ }
+
+ public bool VisitFloatLeqOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.leq", node, options);
+ return true;
+ }
+
+ public bool VisitFloatLtOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.lt", node, options);
+ return true;
+ }
+
+ public bool VisitFloatGeqOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.geq", node, options);
+ return true;
+ }
+
+ public bool VisitFloatGtOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.gt", node, options);
+ return true;
+ }
+
+ public bool VisitFloatEqOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.eq", node, options);
+ return true;
+ }
+
static char[] hex = { '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'a', 'b', 'c', 'd', 'e', 'f' };
public bool VisitBvOp(VCExprNAry node, LineariserOptions options)
{
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index eaed83e9..1d63fa5d 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -311,7 +311,7 @@ void ObjectInvariant()
return;
}
- if (type.IsBool || type.IsInt || type.IsReal || type.IsBv)
+ if (type.IsBool || type.IsInt || type.IsReal || type.IsBv || type.IsFloat)
return;
CtorType ctorType = type as CtorType;
diff --git a/Source/UnitTests/CoreTests/CoreTests.csproj b/Source/UnitTests/CoreTests/CoreTests.csproj
index 61215d48..24fd8c45 100644
--- a/Source/UnitTests/CoreTests/CoreTests.csproj
+++ b/Source/UnitTests/CoreTests/CoreTests.csproj
@@ -54,7 +54,7 @@
</ItemGroup>
<ItemGroup>
<ProjectReference Include="..\..\Basetypes\Basetypes.csproj">
- <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
+ <Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project>
<Name>Basetypes</Name>
</ProjectReference>
<ProjectReference Include="..\..\Core\Core.csproj">
diff --git a/Source/UnitTests/CoreTests/ExprImmutability.cs b/Source/UnitTests/CoreTests/ExprImmutability.cs
index b83983b6..86018d9b 100644
--- a/Source/UnitTests/CoreTests/ExprImmutability.cs
+++ b/Source/UnitTests/CoreTests/ExprImmutability.cs
@@ -29,6 +29,9 @@ namespace CoreTests
var literal4 = new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(0), 8, /*immutable=*/true);
Assert.AreEqual(literal4.ComputeHashCode(), literal4.GetHashCode());
+
+ var literal5 = new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigFloat.FromInt(0), /*immutable=*/true);
+ Assert.AreEqual(literal5.ComputeHashCode(), literal5.GetHashCode());
}
[Test()]
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 0c817756..1bcb6afc 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -334,7 +334,10 @@ namespace Microsoft.Boogie.VCExprAST {
return Gen.Integer(node.asBigNum);
} else if (node.Val is BigDec) {
return Gen.Real(node.asBigDec);
- } else if (node.Val is BvConst) {
+ } else if (node.Val is BigFloat) {
+ return Gen.Float(node.asBigFloat);
+ }
+ else if (node.Val is BvConst) {
return Gen.Bitvector((BvConst)node.Val);
} else {
System.Diagnostics.Debug.Assert(false, "unknown kind of literal " + node.tok.ToString());
@@ -1002,9 +1005,12 @@ namespace Microsoft.Boogie.VCExprAST {
if (cce.NonNull(e.Type).IsInt) {
return Gen.Function(VCExpressionGenerator.SubIOp, Gen.Integer(BigNum.ZERO), e);
}
- else {
+ else {// if (cce.NonNull(e.Type).IsReal) {
return Gen.Function(VCExpressionGenerator.SubROp, Gen.Real(BigDec.ZERO), e);
}
+ //else {//is float
+ //return Gen.Function(VCExpressionGenerator.SubFOp, Gen.Float(BigFloat.ZERO(8, 23)), e);
+ //}
}
else {
return Gen.Not(this.args);
@@ -1070,34 +1076,48 @@ namespace Microsoft.Boogie.VCExprAST {
Contract.Requires(cce.NonNullElements(args));
Contract.Ensures(Contract.Result<VCExpr>() != null);
Contract.Assert(args.Count == 2);
+ Type t = cce.NonNull(cce.NonNull(args[0]).Type);
switch (app.Op) {
case BinaryOperator.Opcode.Add:
- if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) {
+ if (t.IsInt) {
return Gen.Function(VCExpressionGenerator.AddIOp, args);
}
- else {
+ else if (t.IsReal) {
return Gen.Function(VCExpressionGenerator.AddROp, args);
}
+ else { //t is float
+ return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "+"), args);
+ }
case BinaryOperator.Opcode.Sub:
- if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) {
+ if (t.IsInt) {
return Gen.Function(VCExpressionGenerator.SubIOp, args);
}
- else {
+ else if (t.IsReal) {
return Gen.Function(VCExpressionGenerator.SubROp, args);
}
+ else { //t is float
+ return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "-"), args);
+ }
case BinaryOperator.Opcode.Mul:
- if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) {
+ if (t.IsInt) {
return Gen.Function(VCExpressionGenerator.MulIOp, args);
}
- else {
+ else if (t.IsReal) {
return Gen.Function(VCExpressionGenerator.MulROp, args);
}
+ else
+ { //t is float
+ return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "*"), args);
+ }
case BinaryOperator.Opcode.Div:
return Gen.Function(VCExpressionGenerator.DivIOp, args);
case BinaryOperator.Opcode.Mod:
return Gen.Function(VCExpressionGenerator.ModOp, args);
case BinaryOperator.Opcode.RealDiv:
+ if (t.IsFloat) {
+ return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "/"), args);
+ }
VCExpr arg0 = cce.NonNull(args[0]);
VCExpr arg1 = cce.NonNull(args[1]);
if (cce.NonNull(arg0.Type).IsInt) {
@@ -1112,16 +1132,26 @@ namespace Microsoft.Boogie.VCExprAST {
case BinaryOperator.Opcode.Eq:
case BinaryOperator.Opcode.Iff:
// we don't distinguish between equality and equivalence at this point
+ if (t.IsFloat)
+ return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "=="), args);
return Gen.Function(VCExpressionGenerator.EqOp, args);
case BinaryOperator.Opcode.Neq:
return Gen.Function(VCExpressionGenerator.NeqOp, args);
case BinaryOperator.Opcode.Lt:
+ if (t.IsFloat)
+ return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "<"), args);
return Gen.Function(VCExpressionGenerator.LtOp, args);
case BinaryOperator.Opcode.Le:
+ if (t.IsFloat)
+ return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "<="), args);
return Gen.Function(VCExpressionGenerator.LeOp, args);
case BinaryOperator.Opcode.Ge:
+ if (t.IsFloat)
+ return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, ">="), args);
return Gen.Function(VCExpressionGenerator.GeOp, args);
case BinaryOperator.Opcode.Gt:
+ if (t.IsFloat)
+ return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, ">"), args);
return Gen.Function(VCExpressionGenerator.GtOp, args);
case BinaryOperator.Opcode.Imp:
return Gen.Function(VCExpressionGenerator.ImpliesOp, args);
diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs
index b554c331..1a4374f8 100644
--- a/Source/VCExpr/SimplifyLikeLineariser.cs
+++ b/Source/VCExpr/SimplifyLikeLineariser.cs
@@ -380,9 +380,22 @@ namespace Microsoft.Boogie.VCExprAST {
internal const string realSubName = "realSub";
internal const string realMulName = "realMul";
internal const string realDivName = "realDiv";
+ internal const string floatAddName = "floatAdd";
+ internal const string floatSubName = "floatSub";
+ internal const string floatMulName = "floatMul";
+ internal const string floatDivName = "floatDiv";
+ internal const string floatRemName = "floatRem";
+ internal const string floatMinName = "floatMin";
+ internal const string floatMaxName = "floatMax";
+ internal const string floatLeqName = "floatLeq";
+ internal const string floatLtName = "floatLt";
+ internal const string floatGeqName = "floatGeq";
+ internal const string floatGtName = "floatGt";
+ internal const string floatEqName = "floatEq";
internal const string realPowName = "realPow";
internal const string toIntName = "toIntCoercion";
internal const string toRealName = "toRealCoercion";
+ internal const string toFloatName = "toFloatCoercion";
internal void AssertAsTerm(string x, LineariserOptions options) {
Contract.Requires(options != null);
@@ -883,7 +896,104 @@ namespace Microsoft.Boogie.VCExprAST {
return true;
}
- public bool VisitBvOp(VCExprNAry node, LineariserOptions options) {
+ public bool VisitFloatAddOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatAddName, node, options);
+ return true;
+ }
+
+ public bool VisitFloatSubOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatSubName, node, options);
+ return true;
+ }
+
+ public bool VisitFloatMulOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatMulName, node, options);
+ return true;
+ }
+
+ public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatDivName, node, options);
+ return true;
+ }
+
+ public bool VisitFloatRemOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatRemName, node, options);
+ return true;
+ }
+
+ public bool VisitFloatMinOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatMinName, node, options);
+ return true;
+ }
+
+ public bool VisitFloatMaxOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatMaxName, node, options);
+ return true;
+ }
+
+ public bool VisitFloatLeqOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatLeqName, node, options);
+ return true;
+ }
+
+ public bool VisitFloatLtOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatLtName, node, options);
+ return true;
+ }
+
+ public bool VisitFloatGeqOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatGeqName, node, options);
+ return true;
+ }
+
+ public bool VisitFloatGtOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatGtName, node, options);
+ return true;
+ }
+
+ public bool VisitFloatEqOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatEqName, node, options);
+ return true;
+ }
+
+ public bool VisitBvOp(VCExprNAry node, LineariserOptions options)
+ {
//Contract.Requires(options != null);
//Contract.Requires(node != null);
WriteTermApplication("$make_bv" + node.Type.BvBits, node, options);
@@ -955,9 +1065,12 @@ namespace Microsoft.Boogie.VCExprAST {
if (node.Type.IsInt) {
WriteTermApplication(intSubName, node, options);
}
- else {
+ else if (node.Type.IsReal) {
WriteTermApplication(realSubName, node, options);
}
+ else {
+ WriteTermApplication(floatSubName, node, options);
+ }
return true;
}
@@ -967,9 +1080,12 @@ namespace Microsoft.Boogie.VCExprAST {
if (node.Type.IsInt) {
WriteTermApplication(intMulName, node, options);
}
- else {
+ else if (node.Type.IsReal) {
WriteTermApplication(realMulName, node, options);
}
+ else {
+ WriteTermApplication(floatMulName, node, options);
+ }
return true;
}
@@ -1057,6 +1173,14 @@ namespace Microsoft.Boogie.VCExprAST {
return true;
}
+ public bool VisitToFloatOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteApplication(toFloatName, node, options);
+ return true;
+ }
+
public bool VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options) {
//Contract.Requires(options != null);
//Contract.Requires(node != null);
diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index 76340f97..c2d99d77 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -1424,6 +1424,13 @@ namespace Microsoft.Boogie.TypeErasure {
Contract.Ensures(Contract.Result<VCExpr>() != null);
return CastArguments(node, Type.Real, bindings, 0);
}
+ /*public override VCExpr VisitFloatDivOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArguments(node, Type.Float, bindings, 0);
+ }*/
public override VCExpr VisitPowOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
Contract.Requires((node != null));
@@ -1472,6 +1479,90 @@ namespace Microsoft.Boogie.TypeErasure {
Contract.Ensures(Contract.Result<VCExpr>() != null);
return CastArgumentsToOldType(node, bindings, 0);
}
+ public override VCExpr VisitFloatAddOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr VisitFloatSubOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr VisitFloatMulOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr VisitFloatDivOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr VisitFloatRemOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr VisitFloatMinOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr VisitFloatMaxOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr VisitFloatLeqOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr VisitFloatLtOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr VisitFloatGeqOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr VisitFloatGtOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr VisitFloatEqOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
public override VCExpr VisitBvOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
Contract.Requires((node != null));
diff --git a/Source/VCExpr/VCExpr.csproj b/Source/VCExpr/VCExpr.csproj
index 1ad99bc1..efac274e 100644
--- a/Source/VCExpr/VCExpr.csproj
+++ b/Source/VCExpr/VCExpr.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
@@ -9,7 +9,7 @@
<OutputType>Library</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>VCExpr</RootNamespace>
- <AssemblyName>VCExpr</AssemblyName>
+ <AssemblyName>BoogieVCExpr</AssemblyName>
<TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
<CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
@@ -34,7 +34,7 @@
<IsWebBootstrapper>false</IsWebBootstrapper>
<UseApplicationTrust>false</UseApplicationTrust>
<BootstrapperEnabled>true</BootstrapperEnabled>
- <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile>
+ <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
@@ -220,4 +220,4 @@
<Target Name="AfterBuild">
</Target>
-->
-</Project>
+</Project> \ No newline at end of file
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 2c77a252..b5d4dfb5 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -55,6 +55,13 @@ namespace Microsoft.Boogie {
return new VCExprRealLit(x);
}
+ public VCExpr/*!*/ Float(BigFloat x)
+ {
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ return new VCExprFloatLit(x);
+ }
+
public VCExpr/*!*/ Function(VCExprOp/*!*/ op,
List<VCExpr/*!*/>/*!*/ arguments,
List<Type/*!*/>/*!*/ typeArguments) {
@@ -319,10 +326,13 @@ namespace Microsoft.Boogie {
public static readonly VCExprOp AddROp = new VCExprNAryOp(2, Type.Real);
public static readonly VCExprOp SubIOp = new VCExprNAryOp(2, Type.Int);
public static readonly VCExprOp SubROp = new VCExprNAryOp(2, Type.Real);
+ // public static readonly VCExprOp SubFOp = new VCExprNAryOp(2, Type.Float);
public static readonly VCExprOp MulIOp = new VCExprNAryOp(2, Type.Int);
public static readonly VCExprOp MulROp = new VCExprNAryOp(2, Type.Real);
+ //public static readonly VCExprOp MulFOp = new VCExprNAryOp(2, Type.Float);
public static readonly VCExprOp DivIOp = new VCExprNAryOp(2, Type.Int);
public static readonly VCExprOp DivROp = new VCExprNAryOp(2, Type.Real);
+ //public static readonly VCExprOp DivFOp = new VCExprNAryOp(2, Type.Float);
public static readonly VCExprOp ModOp = new VCExprNAryOp(2, Type.Int);
public static readonly VCExprOp PowOp = new VCExprNAryOp(2, Type.Real);
public static readonly VCExprOp LtOp = new VCExprNAryOp(2, Type.Bool);
@@ -336,6 +346,7 @@ namespace Microsoft.Boogie {
public static readonly VCExprOp IfThenElseOp = new VCExprIfThenElseOp();
public static readonly VCExprOp ToIntOp = new VCExprNAryOp(1, Type.Int);
public static readonly VCExprOp ToRealOp = new VCExprNAryOp(1, Type.Real);
+ //public static readonly VCExprOp ToFloatOp = new VCExprNAryOp(1, Type.Float);
public static readonly VCExprOp TickleBoolOp = new VCExprCustomOp("tickleBool", 1, Type.Bool);
@@ -351,6 +362,17 @@ namespace Microsoft.Boogie {
return new VCExprBoogieFunctionOp(func);
}
+ // Float nodes
+
+ public VCExprOp BinaryFloatOp(int exp, int man, string op)
+ {
+ Contract.Requires(exp > 0);
+ Contract.Requires(man > 0);
+ Contract.Requires(op != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return new VCExprBinaryFloatOp(exp, man, op);
+ }
+
// Bitvector nodes
public VCExpr Bitvector(BvConst bv) {
@@ -406,7 +428,8 @@ namespace Microsoft.Boogie {
Subtype3Op,
BvConcatOp,
ToIntOp,
- ToRealOp
+ ToRealOp,
+ ToFloatOp
};
internal static Dictionary<VCExprOp/*!*/, SingletonOp>/*!*/ SingletonOpDict;
[ContractInvariantMethod]
@@ -427,10 +450,13 @@ namespace Microsoft.Boogie {
SingletonOpDict.Add(AddROp, SingletonOp.AddOp);
SingletonOpDict.Add(SubIOp, SingletonOp.SubOp);
SingletonOpDict.Add(SubROp, SingletonOp.SubOp);
+ //SingletonOpDict.Add(SubFOp, SingletonOp.SubOp);
SingletonOpDict.Add(MulIOp, SingletonOp.MulOp);
SingletonOpDict.Add(MulROp, SingletonOp.MulOp);
+ //SingletonOpDict.Add(MulFOp, SingletonOp.MulOp);
SingletonOpDict.Add(DivIOp, SingletonOp.DivOp);
SingletonOpDict.Add(DivROp, SingletonOp.RealDivOp);
+ //SingletonOpDict.Add(DivFOp, SingletonOp.FloatDivOp);
SingletonOpDict.Add(ModOp, SingletonOp.ModOp);
SingletonOpDict.Add(PowOp, SingletonOp.PowOp);
SingletonOpDict.Add(LtOp, SingletonOp.LtOp);
@@ -441,6 +467,7 @@ namespace Microsoft.Boogie {
SingletonOpDict.Add(Subtype3Op, SingletonOp.Subtype3Op);
SingletonOpDict.Add(ToIntOp, SingletonOp.ToIntOp);
SingletonOpDict.Add(ToRealOp, SingletonOp.ToRealOp);
+ //SingletonOpDict.Add(ToFloatOp, SingletonOp.ToFloatOp);
}
////////////////////////////////////////////////////////////////////////////////
@@ -862,6 +889,31 @@ namespace Microsoft.Boogie.VCExprAST {
}
}
+ public class VCExprFloatLit : VCExprLiteral
+ {
+ public readonly BigFloat Val;
+ internal VCExprFloatLit(BigFloat val)
+ : base(Type.GetFloatType(val.ExponentSize, val.SignificandSize))
+ {
+ this.Val = val;
+ }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that)
+ {
+ if (Object.ReferenceEquals(this, that))
+ return true;
+ if (that is VCExprFloatLit)
+ return Val == ((VCExprFloatLit)that).Val;
+ return false;
+ }
+ [Pure]
+ public override int GetHashCode()
+ {
+ return Val.GetHashCode() * 72321;
+ }
+ }
+
/////////////////////////////////////////////////////////////////////////////////
// Operator expressions with fixed arity
[ContractClassFor(typeof(VCExprNAry))]
@@ -1639,6 +1691,86 @@ namespace Microsoft.Boogie.VCExprAST {
}
/////////////////////////////////////////////////////////////////////////////////
+ // Float operators
+
+ public class VCExprBinaryFloatOp : VCExprOp {
+ public readonly int Mantissa;
+ public readonly int Exponent;
+ private string op;
+
+ public override int Arity {
+ get {
+ return 2;
+ }
+ }
+ public override int TypeParamArity {
+ get {
+ return 2;
+ }
+ }
+ public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
+ //Contract.Requires(cce.NonNullElements(typeArgs));
+ //Contract.Requires(cce.NonNullElements(args));
+ Contract.Ensures(Contract.Result<Type>() != null);
+ return Type.GetFloatType(Exponent, Mantissa);
+ }
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ if (Object.ReferenceEquals(this, that))
+ return true;
+ if (that is VCExprBinaryFloatOp)
+ return this.Exponent == ((VCExprBinaryFloatOp)that).Exponent && this.Mantissa == ((VCExprBinaryFloatOp)that).Mantissa;
+ return false;
+ }
+ [Pure]
+ public override int GetHashCode() {
+ return Exponent * 81748912 + Mantissa * 67867979;
+ }
+
+ internal VCExprBinaryFloatOp(int exp, int man, string op) {
+ this.Exponent = exp;
+ this.Mantissa = man;
+ this.op = op;
+ }
+ public override Result Accept<Result, Arg>
+ (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
+ //Contract.Requires(visitor != null);
+ //Contract.Requires(expr != null);
+ switch (op) {
+ case ("+"):
+ return visitor.VisitFloatAddOp(expr, arg);
+ case ("-"):
+ return visitor.VisitFloatSubOp(expr, arg);
+ case ("*"):
+ return visitor.VisitFloatMulOp(expr, arg);
+ case ("/"):
+ return visitor.VisitFloatDivOp(expr, arg);
+ case ("rem"):
+ return visitor.VisitFloatRemOp(expr, arg);
+ case ("min"):
+ return visitor.VisitFloatMinOp(expr, arg);
+ case ("max"):
+ return visitor.VisitFloatMaxOp(expr, arg);
+ case ("<="):
+ return visitor.VisitFloatLeqOp(expr, arg);
+ case ("<"):
+ return visitor.VisitFloatLtOp(expr, arg);
+ case (">="):
+ return visitor.VisitFloatGeqOp(expr, arg);
+ case (">"):
+ return visitor.VisitFloatGtOp(expr, arg);
+ case ("=="):
+ return visitor.VisitFloatEqOp(expr, arg);
+ default:
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
+ }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////
// Bitvector operators
public class VCExprBvOp : VCExprOp {
diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs
index 2af4708d..dac9604c 100644
--- a/Source/VCExpr/VCExprASTPrinter.cs
+++ b/Source/VCExpr/VCExprASTPrinter.cs
@@ -242,6 +242,78 @@ namespace Microsoft.Boogie.VCExprAST {
//Contract.Requires(node != null);
return PrintNAry("Store", node, wr);
}
+ public bool VisitFloatAddOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.add", node, wr);
+ }
+ public bool VisitFloatSubOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.sub", node, wr);
+ }
+ public bool VisitFloatMulOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.mul", node, wr);
+ }
+ public bool VisitFloatDivOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.div", node, wr);
+ }
+ public bool VisitFloatRemOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.rem", node, wr);
+ }
+ public bool VisitFloatMinOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.min", node, wr);
+ }
+ public bool VisitFloatMaxOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.max", node, wr);
+ }
+ public bool VisitFloatLeqOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.leq", node, wr);
+ }
+ public bool VisitFloatLtOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.lt", node, wr);
+ }
+ public bool VisitFloatGeqOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.geq", node, wr);
+ }
+ public bool VisitFloatGtOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.gt", node, wr);
+ }
+ public bool VisitFloatEqOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.eq", node, wr);
+ }
public bool VisitBvOp(VCExprNAry node, TextWriter wr) {
//Contract.Requires(wr != null);
//Contract.Requires(node != null);
diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index fc1bdd65..a23aaf8a 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -68,6 +68,18 @@ namespace Microsoft.Boogie.VCExprAST {
Result VisitLabelOp(VCExprNAry node, Arg arg);
Result VisitSelectOp(VCExprNAry node, Arg arg);
Result VisitStoreOp(VCExprNAry node, Arg arg);
+ Result VisitFloatAddOp(VCExprNAry node, Arg arg);
+ Result VisitFloatSubOp(VCExprNAry node, Arg arg);
+ Result VisitFloatMulOp(VCExprNAry node, Arg arg);
+ Result VisitFloatDivOp(VCExprNAry node, Arg arg);
+ Result VisitFloatRemOp(VCExprNAry node, Arg arg);
+ Result VisitFloatMinOp(VCExprNAry node, Arg arg);
+ Result VisitFloatMaxOp(VCExprNAry node, Arg arg);
+ Result VisitFloatLeqOp(VCExprNAry node, Arg arg);
+ Result VisitFloatLtOp(VCExprNAry node, Arg arg);
+ Result VisitFloatGeqOp(VCExprNAry node, Arg arg);
+ Result VisitFloatGtOp(VCExprNAry node, Arg arg);
+ Result VisitFloatEqOp(VCExprNAry node, Arg arg);
Result VisitBvOp(VCExprNAry node, Arg arg);
Result VisitBvExtractOp(VCExprNAry node, Arg arg);
Result VisitBvConcatOp(VCExprNAry node, Arg arg);
@@ -144,6 +156,78 @@ namespace Microsoft.Boogie.VCExprAST {
throw new NotImplementedException();
}
+ public Result VisitFloatAddOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitFloatSubOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitFloatMulOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitFloatDivOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitFloatRemOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitFloatMinOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitFloatMaxOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitFloatLeqOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitFloatLtOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitFloatGeqOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitFloatGtOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitFloatEqOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
public Result VisitBvOp(VCExprNAry node, Arg arg) {
Contract.Requires(node != null);
throw new NotImplementedException();
@@ -234,6 +318,12 @@ namespace Microsoft.Boogie.VCExprAST {
throw new NotImplementedException();
}
+ public Result VisitToFloat(VCExprNAry node, Arg arg) //TODO: modify later
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
public Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) {
Contract.Requires(node != null);
throw new NotImplementedException();
@@ -1438,6 +1528,65 @@ namespace Microsoft.Boogie.VCExprAST {
//Contract.Requires(node != null);
return StandardResult(node, arg);
}
+ public virtual Result VisitFloatAddOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitFloatSubOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitFloatMulOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitFloatDivOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitFloatRemOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitFloatMinOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitFloatMaxOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitFloatLeqOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitFloatLtOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitFloatGeqOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitFloatGtOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitFloatEqOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
public virtual Result VisitBvOp(VCExprNAry node, Arg arg) {
//Contract.Requires(node != null);
return StandardResult(node, arg);
@@ -1518,6 +1667,11 @@ namespace Microsoft.Boogie.VCExprAST {
//Contract.Requires(node != null);
return StandardResult(node, arg);
}
+ public virtual Result VisitToFloatOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
public virtual Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) {
//Contract.Requires(node != null);
return StandardResult(node, arg);
diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj
index 9bd3fb1a..4d4fc374 100644
--- a/Source/VCGeneration/VCGeneration.csproj
+++ b/Source/VCGeneration/VCGeneration.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
@@ -9,7 +9,7 @@
<OutputType>Library</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>VCGeneration</RootNamespace>
- <AssemblyName>VCGeneration</AssemblyName>
+ <AssemblyName>BoogieVCGeneration</AssemblyName>
<TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
<CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
@@ -34,7 +34,7 @@
<IsWebBootstrapper>false</IsWebBootstrapper>
<UseApplicationTrust>false</UseApplicationTrust>
<BootstrapperEnabled>true</BootstrapperEnabled>
- <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile>
+ <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
@@ -227,4 +227,4 @@
<Target Name="AfterBuild">
</Target>
-->
-</Project>
+</Project> \ No newline at end of file
diff --git a/Test/civl/ticket.bpl b/Test/civl/ticket.bpl
index df19aae4..2e0c6cd1 100644
--- a/Test/civl/ticket.bpl
+++ b/Test/civl/ticket.bpl
@@ -7,7 +7,7 @@ axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x);
type X;
const nil: X;
-var {:layer 0,2} t: int;
+var {:layer 0,1} t: int;
var {:layer 0,2} s: int;
var {:layer 0,2} cs: X;
var {:layer 0,2} T: [int]bool;
@@ -41,14 +41,15 @@ ensures {:layer 1} {:layer 2} xl != nil;
}
procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool)
-requires {:layer 2} xls' == MapConstBool(true);
+requires {:layer 1} Inv1(T, t);
+requires {:layer 2} xls' == MapConstBool(true) && Inv2(T, s, cs);
{
var {:linear "tid"} tid: X;
var {:linear "tid"} xls: [X]bool;
- yield;
+ par Yield1() | Yield2();
- call Init(xls');
+ call InitAbstract(xls');
xls := xls';
par Yield1() | Yield2();
@@ -96,10 +97,20 @@ ensures {:layer 2} Inv2(T, s, cs) && cs == tid;
par Yield1() | Yield2() | YieldSpec(tid);
}
+procedure {:yields} {:layer 1,2} InitAbstract({:linear "tid"} xls:[X]bool)
+requires {:layer 1} Inv1(T, t);
+ensures {:layer 1} Inv1(T, t);
+ensures {:atomic} |{ A: assert xls == MapConstBool(true); cs := nil; s := 0; T := RightOpen(0); return true; }|;
+{
+ par Yield1();
+ call Init(xls);
+ par Yield1();
+}
+
procedure {:yields} {:layer 1,2} GetTicketAbstract({:linear "tid"} tid: X) returns (m: int)
requires {:layer 1} Inv1(T, t);
ensures {:layer 1} Inv1(T, t);
-ensures {:right} |{ A: havoc m, t; assume !T[m]; T[m] := true; return true; }|;
+ensures {:right} |{ A: havoc m; assume !T[m]; T[m] := true; return true; }|;
{
par Yield1();
call m := GetTicket(tid);
@@ -130,7 +141,7 @@ ensures {:layer 1} Inv1(T,t);
assert {:layer 1} Inv1(T,t);
}
-procedure {:yields} {:layer 0,2} Init({:linear "tid"} xls:[X]bool);
+procedure {:yields} {:layer 0,1} Init({:linear "tid"} xls:[X]bool);
ensures {:atomic} |{ A: assert xls == MapConstBool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;
procedure {:yields} {:layer 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int);
@@ -140,7 +151,7 @@ procedure {:yields} {:layer 0,2} WaitAndEnter({:linear "tid"} tid: X, m:int);
ensures {:atomic} |{ A: assume m <= s; cs := tid; return true; }|;
procedure {:yields} {:layer 0,2} Leave({:linear "tid"} tid: X);
-ensures {:atomic} |{ A: s := s + 1; cs := nil; return true; }|;
+ensures {:atomic} |{ A: assert cs == tid; s := s + 1; cs := nil; return true; }|;
procedure {:yields} {:layer 0,2} AllocateLow({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);
ensures {:atomic} |{ A: assume xl != nil; return true; }|;
diff --git a/Test/civl/ticket.bpl.expect b/Test/civl/ticket.bpl.expect
index dc45a0ee..6696bdbd 100644
--- a/Test/civl/ticket.bpl.expect
+++ b/Test/civl/ticket.bpl.expect
@@ -1,2 +1,2 @@
-Boogie program verifier finished with 24 verified, 0 errors
+Boogie program verifier finished with 26 verified, 0 errors
diff --git a/Test/floats/float0.bpl b/Test/floats/float0.bpl
new file mode 100644
index 00000000..d7faa4b0
--- /dev/null
+++ b/Test/floats/float0.bpl
@@ -0,0 +1,14 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo(x : real) returns (r : float8e24)
+{
+ r := 15; // Error
+ r := 15.0; // Error
+ r := 0e1f22e8; // Error
+ r := 1e0f23e8; // Error
+ r := x; // Error
+ r := 1e0f23e8 + 1e0f23e8; // Error
+ r := 1e0f24e8 + 1e0f23e8; // Error
+
+ return;
+} \ No newline at end of file
diff --git a/Test/floats/float0.bpl.expect b/Test/floats/float0.bpl.expect
new file mode 100644
index 00000000..f657a846
--- /dev/null
+++ b/Test/floats/float0.bpl.expect
@@ -0,0 +1,8 @@
+float0.bpl(5,1): Error: mismatched types in assignment command (cannot assign int to float8e24)
+float0.bpl(6,1): Error: mismatched types in assignment command (cannot assign real to float8e24)
+float0.bpl(7,1): Error: mismatched types in assignment command (cannot assign float22e8 to float8e24)
+float0.bpl(8,1): Error: mismatched types in assignment command (cannot assign float23e8 to float8e24)
+float0.bpl(9,1): Error: mismatched types in assignment command (cannot assign real to float8e24)
+float0.bpl(10,1): Error: mismatched types in assignment command (cannot assign float23e8 to float8e24)
+float0.bpl(11,15): Error: invalid argument types (float24e8 and float23e8) to binary operator +
+7 type checking errors detected in float0.bpl
diff --git a/Test/floats/float1.bpl b/Test/floats/float1.bpl
new file mode 100644
index 00000000..d7fc7837
--- /dev/null
+++ b/Test/floats/float1.bpl
@@ -0,0 +1,13 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo(x : float24e8) returns (r : float24e8)
+{
+ r := 0e128f24e8;
+ r := 1e127f24e8;
+ r := x;
+ r := x + 1e127f24e8;
+ r := 0e127f24e8 + 0e127f24e8;
+ assert(r == 0e128f24e8);
+
+ return;
+} \ No newline at end of file
diff --git a/Test/floats/float1.bpl.expect b/Test/floats/float1.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/floats/float1.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/floats/float10.bpl b/Test/floats/float10.bpl
new file mode 100644
index 00000000..ec9b4895
--- /dev/null
+++ b/Test/floats/float10.bpl
@@ -0,0 +1,18 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float53e11);
+
+procedure double_range_true() returns () {
+ var x : float53e11;
+ havoc x;
+ if (x >= TO_FLOAT64_REAL(-1e307) && x <= TO_FLOAT64_REAL(1e307)) {
+ assert(x==x);
+ }
+}
+
+procedure double_range_false() returns () {
+ var x : float53e11;
+ havoc x;
+ assert(x==x);
+} \ No newline at end of file
diff --git a/Test/floats/float10.bpl.expect b/Test/floats/float10.bpl.expect
new file mode 100644
index 00000000..b60994d4
--- /dev/null
+++ b/Test/floats/float10.bpl.expect
@@ -0,0 +1,5 @@
+float10.bpl(17,2): Error BP5001: This assertion might not hold.
+Execution trace:
+ float10.bpl(16,2): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
diff --git a/Test/floats/float11.bpl b/Test/floats/float11.bpl
new file mode 100644
index 00000000..de148424
--- /dev/null
+++ b/Test/floats/float11.bpl
@@ -0,0 +1,22 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float24e8);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float24e8);
+
+procedure main() returns () {
+ var tick : float24e8;
+ var time : float24e8;
+ var i: int;
+
+ tick := TO_FLOAT32_INT(1)/TO_FLOAT32_INT(10);
+ time := TO_FLOAT32_INT(0);
+
+ i := 0;
+ while (i < 10)
+ {
+ time := time + tick;
+ i := i + 1;
+ }
+ assert time == TO_FLOAT32_INT(1);
+} \ No newline at end of file
diff --git a/Test/floats/float11.bpl.expect b/Test/floats/float11.bpl.expect
new file mode 100644
index 00000000..213345cb
--- /dev/null
+++ b/Test/floats/float11.bpl.expect
@@ -0,0 +1,7 @@
+float11.bpl(21,2): Error BP5001: This assertion might not hold.
+Execution trace:
+ float11.bpl(12,7): anon0
+ float11.bpl(16,2): anon3_LoopHead
+ float11.bpl(16,2): anon3_LoopDone
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/floats/float12.bpl b/Test/floats/float12.bpl
new file mode 100644
index 00000000..914286bb
--- /dev/null
+++ b/Test/floats/float12.bpl
@@ -0,0 +1,16 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_FLOAT32(float24e8) returns (float53e11);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT64(float53e11) returns (float24e8);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_INT(int) returns (float53e11);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float53e11);
+
+procedure main() returns () {
+ var x : float53e11;
+ var y : float24e8;
+
+ x := TO_FLOAT64_REAL(1e20)+TO_FLOAT64_INT(1);
+ y := TO_FLOAT32_FLOAT64(x);
+ assert x != TO_FLOAT64_FLOAT32(y);
+} \ No newline at end of file
diff --git a/Test/floats/float12.bpl.expect b/Test/floats/float12.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/floats/float12.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/floats/float13.bpl b/Test/floats/float13.bpl
new file mode 100644
index 00000000..9c99a30b
--- /dev/null
+++ b/Test/floats/float13.bpl
@@ -0,0 +1,34 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float24e8);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float24e8);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_INT(int) returns (float53e11);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float53e11);
+
+procedure main() returns () {
+ var f : float24e8;
+ var fc : float24e8;
+ var d : float53e11;
+ var dc : float53e11;
+
+ f := 2097152e129f24e8;
+ fc := TO_FLOAT32_INT(5);
+ assert(f == fc);
+
+ f := -0e126f24e8;
+ fc := TO_FLOAT32_REAL(-0.5);
+ assert(f == fc);
+
+ f := 1048576e128f24e8;
+ fc := TO_FLOAT32_REAL(2.25);
+ assert(f == fc);
+
+ d := 1125899906842624e1025f53e11;
+ dc := TO_FLOAT64_INT(5);
+ assert(d == dc);
+
+ d := 562949953421312e1024f53e11;
+ dc := TO_FLOAT64_REAL(2.25);
+ assert(d == dc);
+} \ No newline at end of file
diff --git a/Test/floats/float13.bpl.expect b/Test/floats/float13.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/floats/float13.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/floats/float14.bpl b/Test/floats/float14.bpl
new file mode 100644
index 00000000..1752ef0d
--- /dev/null
+++ b/Test/floats/float14.bpl
@@ -0,0 +1,22 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure main() returns () {
+ var f : float24e8;
+ var d : float53e11;
+
+ f := 0e-1f24e8; //Error
+ f := 0e256f24e8; //Error
+ f := 0e255f24e8; //No Error
+
+ f := 8388608e0f24e8; //Error
+ f := -8388608e0f24e8; //Error
+ f := 8388607e0f24e8; //No Error
+
+ d := 0e-1f53e11; //Error
+ d := 0e2048f53e11; //Error
+ d := 0e2047f53e11; //No Error
+
+ d := 4503599627370496e0f53e11; //Error
+ d := -4503599627370496e0f53e11; //Error
+ d := 4503599627370495e0f53e11; //No Error
+} \ No newline at end of file
diff --git a/Test/floats/float14.bpl.expect b/Test/floats/float14.bpl.expect
new file mode 100644
index 00000000..f42b0286
--- /dev/null
+++ b/Test/floats/float14.bpl.expect
@@ -0,0 +1,9 @@
+float14.bpl(7,7): error: incorrectly formatted floating point, The given exponent -1 cannot fit in the bit size 8
+float14.bpl(8,7): error: incorrectly formatted floating point, The given exponent 256 cannot fit in the bit size 8
+float14.bpl(11,7): error: incorrectly formatted floating point, The given significand 8388608 cannot fit in the bit size 24
+float14.bpl(12,7): error: incorrectly formatted floating point, The given significand 8388608 cannot fit in the bit size 24
+float14.bpl(15,7): error: incorrectly formatted floating point, The given exponent -1 cannot fit in the bit size 11
+float14.bpl(16,7): error: incorrectly formatted floating point, The given exponent 2048 cannot fit in the bit size 11
+float14.bpl(19,7): error: incorrectly formatted floating point, The given significand 4503599627370496 cannot fit in the bit size 53
+float14.bpl(20,7): error: incorrectly formatted floating point, The given significand 4503599627370496 cannot fit in the bit size 53
+8 parse errors detected in float14.bpl
diff --git a/Test/floats/float2.bpl b/Test/floats/float2.bpl
new file mode 100644
index 00000000..ed9e60f0
--- /dev/null
+++ b/Test/floats/float2.bpl
@@ -0,0 +1,15 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo(x : float11e5) returns(r : float24e8) {
+ var y : float53e11;
+ var z : float113e15;
+
+ r := x; // Error
+ r := y; // Error
+ r := z; // Error
+ y := x; // Error
+ y := z; // Error
+ z := x; // Error
+
+ return;
+} \ No newline at end of file
diff --git a/Test/floats/float2.bpl.expect b/Test/floats/float2.bpl.expect
new file mode 100644
index 00000000..3132c514
--- /dev/null
+++ b/Test/floats/float2.bpl.expect
@@ -0,0 +1,7 @@
+float2.bpl(7,1): Error: mismatched types in assignment command (cannot assign float11e5 to float24e8)
+float2.bpl(8,1): Error: mismatched types in assignment command (cannot assign float53e11 to float24e8)
+float2.bpl(9,1): Error: mismatched types in assignment command (cannot assign float113e15 to float24e8)
+float2.bpl(10,1): Error: mismatched types in assignment command (cannot assign float11e5 to float53e11)
+float2.bpl(11,1): Error: mismatched types in assignment command (cannot assign float113e15 to float53e11)
+float2.bpl(12,1): Error: mismatched types in assignment command (cannot assign float11e5 to float113e15)
+6 type checking errors detected in float2.bpl
diff --git a/Test/floats/float3.bpl b/Test/floats/float3.bpl
new file mode 100644
index 00000000..507c4127
--- /dev/null
+++ b/Test/floats/float3.bpl
@@ -0,0 +1,27 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure main() returns () {
+ var x : float24e8;
+ var y : float24e8;
+ var z : float24e8;
+
+ z := x + y;
+ z := x - y;
+ z := x * y;
+ assume(y != 0e0f24e8);
+ z := x / y;
+
+ z := (0e127f24e8 + 0e127f24e8 + 0e0f24e8);
+ assert(z == 0e128f24e8);
+
+ z := 0e128f24e8 - 0e127f24e8;
+ assert(z == 0e127f24e8);
+
+ z := 0e127f24e8 * 0e127f24e8;
+ assert(z == 0e127f24e8);
+
+ z := 0e127f24e8 / 0e127f24e8;
+ assert(z == 0e127f24e8);
+
+ return;
+} \ No newline at end of file
diff --git a/Test/floats/float3.bpl.expect b/Test/floats/float3.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/floats/float3.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/floats/float4.bpl b/Test/floats/float4.bpl
new file mode 100644
index 00000000..1c2df42e
--- /dev/null
+++ b/Test/floats/float4.bpl
@@ -0,0 +1,19 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo() returns (r : float8e24) {
+ var d : float53e11;
+
+ r := 0NaN8e24;
+ r := 0nan8e24;
+ r := 0+oo8e24;
+ r := 0-oo8e24;
+ r := -5e255f8e24;
+
+ d := 0NaN53e11;
+ d := 0nan53e11;
+ d := 0+oo53e11;
+ d := 0-oo53e11;
+ d := -200e2000f53e11;
+
+ return;
+} \ No newline at end of file
diff --git a/Test/floats/float4.bpl.expect b/Test/floats/float4.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/floats/float4.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/floats/float5.bpl b/Test/floats/float5.bpl
new file mode 100644
index 00000000..12b19cf5
--- /dev/null
+++ b/Test/floats/float5.bpl
@@ -0,0 +1,23 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_INT(int) returns (float23e8);
+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_REAL(real) returns (float23e8);
+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_BV31(bv31) returns (float23e8);
+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_BV32(bv32) returns (float23e8);
+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_FLOAT824(float24e8) returns (float24e8);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_FLOAT823(float23e8) returns (float24e8);
+
+procedure foo(x : float24e8) returns (r : float24e8) {
+ r := TO_FLOAT823_INT(5); // Error
+ r := TO_FLOAT823_REAL(5.0); // Error
+ r := TO_FLOAT823_BV31(0bv31); // Error
+ r := TO_FLOAT823_BV32(0bv32); // Error
+ r := TO_FLOAT823_FLOAT824(0e0f24e8); // Error
+ r := TO_FLOAT824_FLOAT823(0e0f23e8); // Error
+
+ r := TO_FLOAT823_FLOAT824(x); // Error
+ r := TO_FLOAT824_FLOAT823(x); // Error
+
+ return;
+} \ No newline at end of file
diff --git a/Test/floats/float5.bpl.expect b/Test/floats/float5.bpl.expect
new file mode 100644
index 00000000..74649769
--- /dev/null
+++ b/Test/floats/float5.bpl.expect
@@ -0,0 +1,6 @@
+float5.bpl(12,1): Error: mismatched types in assignment command (cannot assign float23e8 to float24e8)
+float5.bpl(13,1): Error: mismatched types in assignment command (cannot assign float23e8 to float24e8)
+float5.bpl(14,1): Error: mismatched types in assignment command (cannot assign float23e8 to float24e8)
+float5.bpl(15,1): Error: mismatched types in assignment command (cannot assign float23e8 to float24e8)
+float5.bpl(20,27): Error: invalid type for argument 0 in application of TO_FLOAT824_FLOAT823: float24e8 (expected: float23e8)
+5 type checking errors detected in float5.bpl
diff --git a/Test/floats/float6.bpl b/Test/floats/float6.bpl
new file mode 100644
index 00000000..fecf0385
--- /dev/null
+++ b/Test/floats/float6.bpl
@@ -0,0 +1,30 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float24e8);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float24e8);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_BV32(bv32) returns (float24e8);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_BV64(bv64) returns (float53e11);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT64(float53e11) returns (float24e8);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_FLOAT32(float24e8) returns (float53e11);
+
+procedure main() returns () {
+ var i : int;
+ var r : real;
+ var f32 : float24e8;
+ var f64 : float53e11;
+
+ f32 := TO_FLOAT32_INT(5);
+ f32 := TO_FLOAT32_REAL(5.0);
+
+ f32 := TO_FLOAT32_BV32(0bv32);
+ f64 := TO_FLOAT64_BV64(0bv64);
+
+ f32 := TO_FLOAT32_FLOAT64(0e0f53e11);
+ f64 := TO_FLOAT64_FLOAT32(0e0f24e8);
+
+ f32 := TO_FLOAT32_FLOAT64(f64);
+ f64 := TO_FLOAT64_FLOAT32(f32);
+
+ return;
+} \ No newline at end of file
diff --git a/Test/floats/float6.bpl.expect b/Test/floats/float6.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/floats/float6.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/floats/float7.bpl b/Test/floats/float7.bpl
new file mode 100644
index 00000000..39fca79e
--- /dev/null
+++ b/Test/floats/float7.bpl
@@ -0,0 +1,13 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure main() returns () {
+ var x : float53e11;
+ var y : float53e11;
+ var z : float53e11;
+ var r : float53e11;
+ x := 0e1063f53e11;
+ y := x + 0e1023f53e11;
+ z := x - 0e1023f53e11;
+ r := y - z;
+ assert r == 0e1024f53e11;
+} \ No newline at end of file
diff --git a/Test/floats/float7.bpl.expect b/Test/floats/float7.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/floats/float7.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/floats/float8.bpl b/Test/floats/float8.bpl
new file mode 100644
index 00000000..bfb3b9e9
--- /dev/null
+++ b/Test/floats/float8.bpl
@@ -0,0 +1,13 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure main() returns () {
+ var x : float24e8;
+ var y : float24e8;
+ var z : float24e8;
+ var r : float24e8;
+ x := 0e167f24e8;
+ y := x + 0e127f24e8;
+ z := x - 0e127f24e8;
+ r := y - z;
+ assert r == 0e128f24e8;
+} \ No newline at end of file
diff --git a/Test/floats/float8.bpl.expect b/Test/floats/float8.bpl.expect
new file mode 100644
index 00000000..c55c4619
--- /dev/null
+++ b/Test/floats/float8.bpl.expect
@@ -0,0 +1,5 @@
+float8.bpl(12,2): Error BP5001: This assertion might not hold.
+Execution trace:
+ float8.bpl(8,4): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/floats/float9.bpl b/Test/floats/float9.bpl
new file mode 100644
index 00000000..b1e46ae4
--- /dev/null
+++ b/Test/floats/float9.bpl
@@ -0,0 +1,17 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float24e8);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float24e8);
+
+procedure main() returns () {
+ var x : float24e8;
+ var y : float24e8;
+ var z : float24e8;
+ var r : float24e8;
+ x := TO_FLOAT32_REAL(1e7);
+ y := x + TO_FLOAT32_INT(1);
+ z := x - TO_FLOAT32_INT(1);
+ r := y - z;
+ assert r == TO_FLOAT32_INT(2);
+} \ No newline at end of file
diff --git a/Test/floats/float9.bpl.expect b/Test/floats/float9.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/floats/float9.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors