diff options
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 25 | ||||
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 4 | ||||
| -rw-r--r-- | Source/Dafny/Compiler.cs | 52 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 12 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 84 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 508 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 32 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 54 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.cs | 72 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 348 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 2 | ||||
| -rw-r--r-- | Test/codeexpr/Answer | 2 | ||||
| -rw-r--r-- | Test/inline/Answer | 124 | ||||
| -rw-r--r-- | Test/lazyinline/Answer | 4 | ||||
| -rw-r--r-- | Test/stratifiedinline/Answer | 4 | ||||
| -rw-r--r-- | Test/test2/Answer | 30 |
16 files changed, 769 insertions, 588 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 88e45767..ad4dcbae 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -210,7 +210,6 @@ const unique class.bool: ClassName; const unique class.object: ClassName;
const unique class.set: ClassName;
const unique class.seq: ClassName;
-const unique class.array: ClassName;
function dtype(ref) returns (ClassName);
function TypeParams(ref, int) returns (ClassName);
@@ -249,34 +248,40 @@ const $InMethodContext: bool; type Field alpha;
-type FieldCategory;
-const unique $NamedField: FieldCategory;
-const unique $IndexedField: FieldCategory;
-function FCat<T>(Field T): FieldCategory;
+function FDim<T>(Field T): int;
const unique alloc: Field bool;
-axiom FCat(alloc) == $NamedField;
+axiom FDim(alloc) == 0;
function IndexField(int): Field BoxType;
-axiom (forall i: int :: { IndexField(i) } FCat(IndexField(i)) == $IndexedField);
+axiom (forall i: int :: { IndexField(i) } FDim(IndexField(i)) == 1);
function IndexField_Inverse<T>(Field T): int;
axiom (forall i: int :: { IndexField(i) } IndexField_Inverse(IndexField(i)) == i);
+function MultiIndexField(Field BoxType, int): Field BoxType;
+axiom (forall f: Field BoxType, i: int :: { MultiIndexField(f,i) } FDim(MultiIndexField(f,i)) == FDim(f) + 1);
+function MultiIndexField_Inverse0<T>(Field T): Field T;
+function MultiIndexField_Inverse1<T>(Field T): int;
+axiom (forall f: Field BoxType, i: int :: { MultiIndexField(f,i) }
+ MultiIndexField_Inverse0(MultiIndexField(f,i)) == f &&
+ MultiIndexField_Inverse1(MultiIndexField(f,i)) == i);
+
+
function DeclType<T>(Field T) returns (ClassName);
// ---------------------------------------------------------------
// -- Arrays -----------------------------------------------------
// ---------------------------------------------------------------
-function Array#Length(ref): int;
-axiom (forall r: ref :: 0 <= Array#Length(r));
+function Array#Length(ref, int): int;
+axiom (forall r: ref, dim: int :: 0 <= Array#Length(r, dim));
procedure UpdateArrayRange(arr: ref, low: int, high: int, rhs: BoxType);
modifies $Heap;
ensures $HeapSucc(old($Heap), $Heap);
ensures (forall i: int :: { read($Heap, arr, IndexField(i)) } low <= i && i < high ==> read($Heap, arr, IndexField(i)) == rhs);
ensures (forall<alpha> o: ref, f: Field alpha :: { read($Heap, o, f) } read($Heap, o, f) == read(old($Heap), o, f) ||
- (o == arr && FCat(f) == $IndexedField && low <= IndexField_Inverse(f) && IndexField_Inverse(f) < high));
+ (o == arr && FDim(f) == 1 && low <= IndexField_Inverse(f) && IndexField_Inverse(f) < high));
// ---------------------------------------------------------------
// -- The heap ---------------------------------------------------
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 3bf7b624..a4635f49 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -683,7 +683,7 @@ namespace Microsoft.Boogie { if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingEnsures.ErrorMessage != null) {
ReportBplError(err.FailingEnsures, err.FailingEnsures.ErrorMessage, true, false);
} else {
- ReportBplError(err.FailingReturn, "Error BP5003: A postcondition might not hold at this return statement.", true, true);
+ ReportBplError(err.FailingReturn, "Error BP5003: A postcondition might not hold on this return path.", true, true);
ReportBplError(err.FailingEnsures, "Related location: This is the postcondition that might not hold.", false, true);
}
if (CommandLineOptions.Clo.XmlSink != null) {
@@ -751,4 +751,4 @@ namespace Microsoft.Boogie { }
}
-}
\ No newline at end of file +}
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 1726baf5..6115f026 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -19,10 +19,10 @@ namespace Microsoft.Dafny { }
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(wr!=null);
-}
+ void ObjectInvariant()
+ {
+ Contract.Invariant(wr!=null);
+ }
TextWriter wr;
@@ -236,12 +236,14 @@ void ObjectInvariant() }
}
- string FormalName(Formal formal, int i) {Contract.Requires(formal != null);Contract.Ensures(Contract.Result<string>() != null);
+ string FormalName(Formal formal, int i) {
+ Contract.Requires(formal != null);Contract.Ensures(Contract.Result<string>() != null);
return formal.Name.StartsWith("#") ? "a" + i : formal.Name;
}
- string DtCtorName(DatatypeCtor ctor) {Contract.Requires(ctor != null);Contract.Ensures(Contract.Result<string>() != null);
+ string DtCtorName(DatatypeCtor ctor) {
+ Contract.Requires(ctor != null);Contract.Ensures(Contract.Result<string>() != null);
return cce.NonNull(ctor.EnclosingDatatype).Name + "_" + ctor.Name;
}
@@ -401,8 +403,14 @@ void ObjectInvariant() } else if (type is ObjectType) {
return "object";
} else if (type.IsArrayType) {
+ ArrayClassDecl at = type.AsArrayType;
+ Contract.Assert(at != null); // follows from type.IsArrayType
Type elType = UserDefinedType.ArrayElementType(type);
- return TypeName(elType) + "[]";
+ string name = TypeName(elType) + "[";
+ for (int i = 1; i < at.Dims; i++) {
+ name += ",";
+ }
+ return name + "]";
} else if (type is UserDefinedType) {
UserDefinedType udt = (UserDefinedType)type;
string s = udt.Name;
@@ -753,18 +761,29 @@ void ObjectInvariant() } else {
TypeRhs tp = (TypeRhs)rhs;
- if (tp.ArraySize == null) {
+ if (tp.ArrayDimensions == null) {
wr.Write("new {0}()", TypeName(tp.EType));
} else {
if (tp.EType is IntType || tp.EType.IsTypeParameter) {
// Because the default constructor for BigInteger does not generate a valid BigInteger, we have
// to excplicitly initialize the elements of an integer array. This is all done in a helper routine.
+ Contract.Assume(tp.ArrayDimensions.Count == 1); // TODO: multi-dimensional arrays
wr.Write("Dafny.Helpers.InitNewArray<{0}>(", TypeName(tp.EType));
- TrExpr(tp.ArraySize);
+ string prefix = "(";
+ foreach (Expression dim in tp.ArrayDimensions) {
+ wr.Write(prefix);
+ TrExpr(dim);
+ prefix = ", ";
+ }
wr.Write(")");
} else {
- wr.Write("new {0}[(int)", TypeName(tp.EType));
- TrExpr(tp.ArraySize);
+ wr.Write("new {0}", TypeName(tp.EType));
+ string prefix = "[";
+ foreach (Expression dim in tp.ArrayDimensions) {
+ wr.Write("{0}(int)", prefix);
+ TrExpr(dim);
+ prefix = ", ";
+ }
wr.Write("]");
}
}
@@ -937,6 +956,17 @@ void ObjectInvariant() }
}
+ } else if (expr is MultiSelectExpr) {
+ MultiSelectExpr e = (MultiSelectExpr)expr;
+ TrParenExpr(e.Array);
+ string prefix = "[";
+ foreach (Expression idx in e.Indices) {
+ wr.Write("{0}(int)", prefix);
+ TrParenExpr(idx);
+ prefix = ", ";
+ }
+ wr.Write("]");
+
} else if (expr is SeqUpdateExpr) {
SeqUpdateExpr e = (SeqUpdateExpr)expr;
TrParenExpr(e.Seq);
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 85cf64fe..8845593c 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -499,7 +499,7 @@ ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty> GenericInstantiation<gt> (. if (gt.Count != 1) {
SemErr("array type expects exactly one type argument");
}
- ty = UserDefinedType.ArrayType(tok, gt[0]);
+ ty = UserDefinedType.ArrayType(tok, 1, gt[0]);
.)
| Ident<out tok> (. gt = new List<Type/*!*/>(); .)
[ GenericInstantiation<gt> ] (. ty = new UserDefinedType(tok, tok.val, gt); .)
@@ -640,7 +640,6 @@ CaseExpression<out MatchCaseExpr/*!*/ c> BlockStmt<out Statement/*!*/ block>
= (. Contract.Ensures(Contract.ValueAtReturn(out block) != null); IToken/*!*/ x;
List<Statement/*!*/> body = new List<Statement/*!*/>();
- Statement/*!*/ s;
.)
(. parseVarScope.PushMarker(); .)
"{" (. x = t; .)
@@ -703,7 +702,7 @@ AssignStmt<out Statement/*!*/ s> } else if (rhs == null) {
s = new AssignStmt(x, lhs, ty);
} else {
- s = new AssignStmt(x, lhs, ty, rhs);
+ s = new AssignStmt(x, lhs, ty, new List<Expression>(new Expression[] { rhs }));
}
.)
";"
@@ -744,7 +743,7 @@ VarDeclStmts<.List<Statement/*!*/>/*!*/ ss.> .
IdentTypeRhs<out VarDecl/*!*/ d, bool isGhost>
-= (. Contract.Ensures(Contract.ValueAtReturn(out d) != null); IToken/*!*/ id; Type/*!*/ ty; Expression/*!*/ e;
+= (. Contract.Ensures(Contract.ValueAtReturn(out d) != null); IToken/*!*/ id; Type/*!*/ ty;
Expression rhs = null; Type newType = null;
Type optionalType = null; DeterminedAssignmentRhs optionalRhs = null;
.)
@@ -760,7 +759,7 @@ IdentTypeRhs<out VarDecl/*!*/ d, bool isGhost> if (rhs == null) {
optionalRhs = new TypeRhs(newType);
} else {
- optionalRhs = new TypeRhs(newType, rhs);
+ optionalRhs = new TypeRhs(newType, new List<Expression>(new Expression[] { rhs }));
}
} else if (optionalType == null) {
optionalType = new InferredTypeProxy();
@@ -1149,7 +1148,7 @@ CallStmtSubExpr<out Expression/*!*/ e> .
SelectExpression<out Expression/*!*/ e>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ id; e = dummyExpr; .)
+= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; .)
( IdentOrFuncExpression<out e>
| ObjectExpression<out e>
)
@@ -1238,7 +1237,6 @@ QuantifierGuts<out Expression/*!*/ q> bool univ = false;
BoundVar/*!*/ bv;
List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
- IToken/*!*/ tok; Expr/*!*/ e; ExprSeq/*!*/ es;
Attributes attrs = null;
Triggers trigs = null;
Expression/*!*/ body;
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 6f607d83..8451dd67 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -95,8 +95,13 @@ namespace Microsoft.Dafny { }
public bool IsArrayType {
get {
+ return AsArrayType != null;
+ }
+ }
+ public ArrayClassDecl/*?*/ AsArrayType {
+ get {
UserDefinedType udt = UserDefinedType.DenotesClass(this);
- return udt != null && cce.NonNull((ClassDecl)udt.ResolvedClass).Name == "array"; // the cast to non-null is guaranteed by postcondition of DenotesClass
+ return udt == null ? null : udt.ResolvedClass as ArrayClassDecl;
}
}
public bool IsDatatype {
@@ -192,7 +197,7 @@ namespace Microsoft.Dafny { Contract.Invariant(tok != null);
Contract.Invariant(cce.NonNullElements(Name));
Contract.Invariant(cce.NonNullElements(TypeArgs));
- Contract.Invariant(arrayTypeDecl != null);
+ Contract.Invariant(ArrayTypeDecls != null);
}
public readonly IToken tok;
@@ -203,25 +208,23 @@ namespace Microsoft.Dafny { public TopLevelDecl ResolvedClass; // filled in by resolution, if Name denotes a class/datatype and TypeArgs match the type parameters of that class/datatype
public TypeParameter ResolvedParam; // filled in by resolution, if Name denotes an enclosing type parameter and TypeArgs is the empty list
- public static UserDefinedType ArrayType(IToken tok, Type arg) {
+ public static UserDefinedType ArrayType(IToken tok, int dims, Type arg) {
Contract.Requires(tok != null);
+ Contract.Requires(1 <= dims);
Contract.Requires(arg != null);
Contract.Ensures(Contract.Result<UserDefinedType>() != null);
List<Type/*!*/> typeArgs = new List<Type/*!*/>();
typeArgs.Add(arg);
- UserDefinedType udt = new UserDefinedType(tok, "array", typeArgs);
- udt.ResolvedClass = arrayTypeDecl;
+ UserDefinedType udt = new UserDefinedType(tok, "array" + dims, typeArgs);
+ if (!ArrayTypeDecls.ContainsKey(dims)) {
+ ArrayTypeDecls.Add(dims, new ArrayClassDecl(dims, _systemModule));
+ }
+ udt.ResolvedClass = ArrayTypeDecls[dims];
return udt;
}
- static TopLevelDecl/*!*/ arrayTypeDecl;
- static UserDefinedType() {
- List<TypeParameter> typeArgs = new List<TypeParameter>();
- typeArgs.Add(new TypeParameter(Token.NoToken, "arg"));
- ModuleDecl systemModule = new ModuleDecl(Token.NoToken, "_System", new List<string>(), null);
- arrayTypeDecl = new ClassDecl(Token.NoToken, "array", systemModule, typeArgs, new List<MemberDecl>(), null);
- }
-
+ public static Dictionary<int, ClassDecl/*!*/> ArrayTypeDecls = new Dictionary<int,ClassDecl>();
+ static readonly ModuleDecl _systemModule = new ModuleDecl(Token.NoToken, "_System", new List<string>(), null);
public UserDefinedType(IToken/*!*/ tok, string/*!*/ name, [Captured] List<Type/*!*/>/*!*/ typeArgs) {
Contract.Requires(tok != null);
@@ -284,10 +287,6 @@ namespace Microsoft.Dafny { }
}
- /// <summary>
- /// If type denotes a resolved class type, then return that class type.
- /// Otherwise, return null.
- /// </summary>
public static Type ArrayElementType(Type type) {
Contract.Requires(type.IsArrayType);
@@ -642,6 +641,20 @@ namespace Microsoft.Dafny { }
}
+ public class ArrayClassDecl : ClassDecl {
+ public readonly int Dims;
+ public ArrayClassDecl(int dims, ModuleDecl module)
+ : base(Token.NoToken, "array" + dims, module,
+ new List<TypeParameter>(new TypeParameter[]{new TypeParameter(Token.NoToken, "arg")}),
+ new List<MemberDecl>(), null)
+ {
+ Contract.Requires(1 <= dims);
+ Contract.Requires(module != null);
+
+ Dims = dims;
+ }
+ }
+
public class DatatypeDecl : TopLevelDecl {
public readonly List<DatatypeCtor/*!*/>/*!*/ Ctors;
[ContractInvariantMethod]
@@ -1253,18 +1266,19 @@ namespace Microsoft.Dafny { [ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(EType != null);
+ Contract.Invariant(ArrayDimensions == null || 1 <= ArrayDimensions.Count);
}
- public readonly Expression ArraySize;
+ public readonly List<Expression> ArrayDimensions;
public TypeRhs(Type type) {
Contract.Requires(type != null);
EType = type;
}
- public TypeRhs(Type type, Expression arraySize) {
+ public TypeRhs(Type type, List<Expression> arrayDimensions) {
Contract.Requires(type != null);
- Contract.Requires(arraySize != null);
+ Contract.Requires(arrayDimensions != null && 1 <= arrayDimensions.Count);
EType = type;
- ArraySize = arraySize;
+ ArrayDimensions = arrayDimensions;
}
}
@@ -1299,14 +1313,14 @@ namespace Microsoft.Dafny { this.Rhs = new TypeRhs(type);
}
- public AssignStmt(IToken tok, Expression lhs, Type type, Expression arraySize)
+ public AssignStmt(IToken tok, Expression lhs, Type type, List<Expression> arrayDimensions)
: base(tok) { // array alloc statement
Contract.Requires(tok != null);
Contract.Requires(lhs != null);
Contract.Requires(type != null);
- Contract.Requires(arraySize != null);
+ Contract.Requires(arrayDimensions != null && 1 <= arrayDimensions.Count);
this.Lhs = lhs;
- this.Rhs = new TypeRhs(type, arraySize);
+ this.Rhs = new TypeRhs(type, arrayDimensions);
}
public AssignStmt(IToken tok, Expression lhs)
: base(tok) { // havoc
@@ -1808,8 +1822,6 @@ namespace Microsoft.Dafny { Contract.Invariant(E0 != null || E1 != null);
}
-
-
public SeqSelectExpr(IToken tok, bool selectOne, Expression seq, Expression e0, Expression e1)
: base(tok) {
Contract.Requires(tok != null);
@@ -1821,7 +1833,27 @@ namespace Microsoft.Dafny { Seq = seq;
E0 = e0;
E1 = e1;
+ }
+ }
+
+ public class MultiSelectExpr : Expression {
+ public readonly Expression Array;
+ public readonly List<Expression> Indices;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Array != null);
+ Contract.Invariant(Indices != null && cce.NonNullElements(Indices));
+ Contract.Invariant(1 <= Indices.Count);
+ }
+
+ public MultiSelectExpr(IToken tok, Expression array, List<Expression> indices)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(array != null);
+ Contract.Requires(indices == null && cce.NonNullElements(indices) && 1 <= indices.Count);
+ Array = array;
+ Indices = indices;
}
}
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index ec029451..d6a7712d 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -9,7 +9,7 @@ using System.Text; using System;
-using Microsoft.Contracts;
+using System.Diagnostics.Contracts;
namespace Microsoft.Dafny {
@@ -213,7 +213,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! while (StartOf(1)) {
if (la.kind == 4) {
Get();
- attrs = null; theImports = new List<string/*!*/>();
+ attrs = null; theImports = new List<string/*!*/>();
while (la.kind == 6) {
Attribute(ref attrs);
}
@@ -222,25 +222,25 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Get();
Idents(theImports);
}
- module = new ModuleDecl(id, id.val, theImports, attrs);
+ module = new ModuleDecl(id, id.val, theImports, attrs);
Expect(6);
while (la.kind == 8 || la.kind == 13) {
if (la.kind == 8) {
ClassDecl(module, out c);
- module.TopLevelDecls.Add(c);
+ module.TopLevelDecls.Add(c);
} else {
DatatypeDecl(module, out dt);
- module.TopLevelDecls.Add(dt);
+ module.TopLevelDecls.Add(dt);
}
}
- theModules.Add(module);
+ theModules.Add(module);
Expect(7);
} else if (la.kind == 8) {
ClassDecl(defaultModule, out c);
- defaultModule.TopLevelDecls.Add(c);
+ defaultModule.TopLevelDecls.Add(c);
} else if (la.kind == 13) {
DatatypeDecl(defaultModule, out dt);
- defaultModule.TopLevelDecls.Add(dt);
+ defaultModule.TopLevelDecls.Add(dt);
} else {
ClassMemberDecl(membersDefaultClass);
}
@@ -269,19 +269,19 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
void Ident(out IToken/*!*/ x) {
- Contract.Ensures(Contract.ValueAtReturn(out x) != null);
+ Contract.Ensures(Contract.ValueAtReturn(out x) != null);
Expect(1);
- x = t;
+ x = t;
}
void Idents(List<string/*!*/>/*!*/ ids) {
- IToken/*!*/ id;
+ IToken/*!*/ id;
Ident(out id);
- ids.Add(id.val);
+ ids.Add(id.val);
while (la.kind == 16) {
Get();
Ident(out id);
- ids.Add(id.val);
+ ids.Add(id.val);
}
}
@@ -306,7 +306,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! if (la.kind == 9) {
Get();
Ident(out idRefined);
- optionalId = idRefined;
+ optionalId = idRefined;
}
Expect(6);
while (StartOf(2)) {
@@ -341,7 +341,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! DatatypeMemberDecl(ctors);
}
Expect(7);
- dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
+ dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
}
void ClassMemberDecl(List<MemberDecl/*!*/>/*!*/ mm) {
@@ -353,23 +353,23 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! while (la.kind == 10 || la.kind == 11 || la.kind == 12) {
if (la.kind == 10) {
Get();
- mmod.IsGhost = true;
+ mmod.IsGhost = true;
} else if (la.kind == 11) {
Get();
- mmod.IsStatic = true;
+ mmod.IsStatic = true;
} else {
Get();
- mmod.IsUnlimited = true;
+ mmod.IsUnlimited = true;
}
}
if (la.kind == 15) {
FieldDecl(mmod, mm);
} else if (la.kind == 37) {
FunctionDecl(mmod, out f);
- mm.Add(f);
+ mm.Add(f);
} else if (la.kind == 9 || la.kind == 22) {
MethodDecl(mmod, out m);
- mm.Add(m);
+ mm.Add(m);
} else if (la.kind == 17) {
CouplingInvDecl(mmod, mm);
} else SynErr(104);
@@ -377,14 +377,14 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
Contract.Requires(cce.NonNullElements(typeArgs));
- IToken/*!*/ id;
+ IToken/*!*/ id;
Expect(20);
Ident(out id);
- typeArgs.Add(new TypeParameter(id, id.val));
+ typeArgs.Add(new TypeParameter(id, id.val));
while (la.kind == 16) {
Get();
Ident(out id);
- typeArgs.Add(new TypeParameter(id, id.val));
+ typeArgs.Add(new TypeParameter(id, id.val));
}
Expect(21);
}
@@ -402,11 +402,11 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Attribute(ref attrs);
}
IdentType(out id, out ty);
- mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
+ mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
while (la.kind == 16) {
Get();
IdentType(out id, out ty);
- mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
+ mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
}
Expect(14);
}
@@ -427,7 +427,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Expect(37);
if (la.kind == 22) {
Get();
- isFunctionMethod = true;
+ isFunctionMethod = true;
}
if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }
@@ -438,7 +438,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! if (la.kind == 20) {
GenericParameters(typeArgs);
}
- parseVarScope.PushMarker();
+ parseVarScope.PushMarker();
Formals(true, false, formals);
Expect(19);
Type(out returnType);
@@ -452,7 +452,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! FunctionSpec(reqs, reads, decreases);
}
FunctionBody(out bb);
- body = bb;
+ body = bb;
} else SynErr(105);
parseVarScope.PopMarker();
f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);
@@ -477,7 +477,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Get();
} else if (la.kind == 9) {
Get();
- isRefinement = true;
+ isRefinement = true;
} else SynErr(106);
if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
@@ -488,7 +488,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! if (la.kind == 20) {
GenericParameters(typeArgs);
}
- parseVarScope.PushMarker();
+ parseVarScope.PushMarker();
Formals(true, true, ins);
if (la.kind == 23) {
Get();
@@ -504,7 +504,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! MethodSpec(req, mod, ens, dec);
}
BlockStmt(out bb);
- body = (BlockStmt)bb;
+ body = (BlockStmt)bb;
} else SynErr(107);
parseVarScope.PopMarker();
if (isRefinement)
@@ -531,11 +531,11 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Attribute(ref attrs);
}
Ident(out id);
- ids.Add(id); parseVarScope.Push(id.val, id.val);
+ ids.Add(id); parseVarScope.Push(id.val, id.val);
while (la.kind == 16) {
Get();
Ident(out id);
- ids.Add(id); parseVarScope.Push(id.val, id.val);
+ ids.Add(id); parseVarScope.Push(id.val, id.val);
}
Expect(18);
Expression(out e);
@@ -559,7 +559,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! if (la.kind == 20) {
GenericParameters(typeArgs);
}
- parseVarScope.PushMarker();
+ parseVarScope.PushMarker();
if (la.kind == 29) {
FormalsOptionalIds(formals);
}
@@ -570,15 +570,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {
- Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost;
+ Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost;
Expect(29);
if (StartOf(6)) {
TypeIdentOptional(out id, out name, out ty, out isGhost);
- formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name);
+ formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name);
while (la.kind == 16) {
Get();
TypeIdentOptional(out id, out name, out ty, out isGhost);
- formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name);
+ formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name);
}
}
Expect(30);
@@ -597,13 +597,13 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! if (la.kind == 52) {
Get();
- x = t;
+ x = t;
Expression(out e);
Expect(64);
Expression(out e0);
Expect(53);
Expression(out e1);
- e = new ITEExpr(x, e, e0, e1);
+ e = new ITEExpr(x, e, e0, e1);
} else if (StartOf(7)) {
EquivExpression(out e);
} else SynErr(108);
@@ -612,7 +612,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! void GIdentType(bool allowGhost, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost) {
Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
- isGhost = false;
+ isGhost = false;
if (la.kind == 10) {
Get();
if (allowGhost) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); }
@@ -621,7 +621,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
void Type(out Type/*!*/ ty) {
- Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok;
+ Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok;
TypeAndToken(out tok, out ty);
}
@@ -632,19 +632,19 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! if (la.kind == 19) {
Get();
Type(out ty);
- optType = ty;
+ optType = ty;
}
- var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType);
+ var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType);
}
void TypeIdentOptional(out IToken/*!*/ id, out string/*!*/ identName, out Type/*!*/ ty, out bool isGhost) {
Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
Contract.Ensures(Contract.ValueAtReturn(out identName)!=null);
- string name = null; isGhost = false;
+ string name = null; isGhost = false;
if (la.kind == 10) {
Get();
- isGhost = true;
+ isGhost = true;
}
TypeAndToken(out id, out ty);
if (la.kind == 19) {
@@ -672,13 +672,13 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! if (la.kind == 31) {
Get();
- tok = t;
+ tok = t;
} else if (la.kind == 32) {
Get();
- tok = t; ty = new IntType();
+ tok = t; ty = new IntType();
} else if (la.kind == 33) {
Get();
- tok = t; gt = new List<Type/*!*/>();
+ tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
if (gt.Count != 1) {
SemErr("set type expects exactly one type argument");
@@ -687,7 +687,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! } else if (la.kind == 34) {
Get();
- tok = t; gt = new List<Type/*!*/>();
+ tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
if (gt.Count != 1) {
SemErr("seq type expects exactly one type argument");
@@ -700,15 +700,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
void Formals(bool incoming, bool allowGhosts, List<Formal/*!*/>/*!*/ formals) {
- Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost;
+ Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost;
Expect(29);
if (la.kind == 1 || la.kind == 10) {
GIdentType(allowGhosts, out id, out ty, out isGhost);
- formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val);
+ formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val);
while (la.kind == 16) {
Get();
GIdentType(allowGhosts, out id, out ty, out isGhost);
- formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val);
+ formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val);
}
}
Expect(30);
@@ -723,29 +723,29 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
if (StartOf(8)) {
FrameExpression(out fe);
- mod.Add(fe);
+ mod.Add(fe);
while (la.kind == 16) {
Get();
FrameExpression(out fe);
- mod.Add(fe);
+ mod.Add(fe);
}
}
Expect(14);
} else if (la.kind == 25 || la.kind == 26 || la.kind == 27) {
if (la.kind == 25) {
Get();
- isFree = true;
+ isFree = true;
}
if (la.kind == 26) {
Get();
Expression(out e);
Expect(14);
- req.Add(new MaybeFreeExpression(e, isFree));
+ req.Add(new MaybeFreeExpression(e, isFree));
} else if (la.kind == 27) {
Get();
Expression(out e);
Expect(14);
- ens.Add(new MaybeFreeExpression(e, isFree));
+ ens.Add(new MaybeFreeExpression(e, isFree));
} else SynErr(110);
} else if (la.kind == 28) {
Get();
@@ -757,50 +757,49 @@ List<Expression/*!*/>/*!*/ decreases) { void BlockStmt(out Statement/*!*/ block) {
Contract.Ensures(Contract.ValueAtReturn(out block) != null); IToken/*!*/ x;
List<Statement/*!*/> body = new List<Statement/*!*/>();
- Statement/*!*/ s;
- parseVarScope.PushMarker();
+ parseVarScope.PushMarker();
Expect(6);
- x = t;
+ x = t;
while (StartOf(9)) {
Stmt(body);
}
Expect(7);
- block = new BlockStmt(x, body);
- parseVarScope.PopMarker();
+ block = new BlockStmt(x, body);
+ parseVarScope.PopMarker();
}
void FrameExpression(out FrameExpression/*!*/ fe) {
- Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null;
+ Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null;
Expression(out e);
if (la.kind == 40) {
Get();
Ident(out id);
- fieldName = id.val;
+ fieldName = id.val;
}
- fe = new FrameExpression(e, fieldName);
+ fe = new FrameExpression(e, fieldName);
}
void Expressions(List<Expression/*!*/>/*!*/ args) {
- Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e;
+ Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e;
Expression(out e);
- args.Add(e);
+ args.Add(e);
while (la.kind == 16) {
Get();
Expression(out e);
- args.Add(e);
+ args.Add(e);
}
}
void GenericInstantiation(List<Type/*!*/>/*!*/ gt) {
- Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty;
+ Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty;
Expect(20);
Type(out ty);
- gt.Add(ty);
+ gt.Add(ty);
while (la.kind == 16) {
Get();
Type(out ty);
- gt.Add(ty);
+ gt.Add(ty);
}
Expect(21);
}
@@ -812,43 +811,43 @@ List<Expression/*!*/>/*!*/ decreases) { if (la.kind == 35) {
Get();
- tok = t; ty = new ObjectType();
+ tok = t; ty = new ObjectType();
} else if (la.kind == 36) {
Get();
- tok = t; gt = new List<Type/*!*/>();
+ tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
if (gt.Count != 1) {
SemErr("array type expects exactly one type argument");
}
- ty = UserDefinedType.ArrayType(tok, gt[0]);
+ ty = UserDefinedType.ArrayType(tok, 1, gt[0]);
} else if (la.kind == 1) {
Ident(out tok);
- gt = new List<Type/*!*/>();
+ gt = new List<Type/*!*/>();
if (la.kind == 20) {
GenericInstantiation(gt);
}
- ty = new UserDefinedType(tok, tok.val, gt);
+ ty = new UserDefinedType(tok, tok.val, gt);
} else SynErr(112);
}
void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ decreases) {
Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));
- Expression/*!*/ e; FrameExpression/*!*/ fe;
+ Expression/*!*/ e; FrameExpression/*!*/ fe;
if (la.kind == 26) {
Get();
Expression(out e);
Expect(14);
- reqs.Add(e);
+ reqs.Add(e);
} else if (la.kind == 38) {
Get();
if (StartOf(10)) {
PossiblyWildFrameExpression(out fe);
- reads.Add(fe);
+ reads.Add(fe);
while (la.kind == 16) {
Get();
PossiblyWildFrameExpression(out fe);
- reads.Add(fe);
+ reads.Add(fe);
}
}
Expect(14);
@@ -860,7 +859,7 @@ List<Expression/*!*/>/*!*/ decreases) { }
void FunctionBody(out Expression/*!*/ e) {
- Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr;
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr;
Expect(6);
if (la.kind == 41) {
MatchExpression(out e);
@@ -871,10 +870,10 @@ List<Expression/*!*/>/*!*/ decreases) { }
void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) {
- Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr;
+ Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr;
if (la.kind == 39) {
Get();
- fe = new FrameExpression(new WildcardExpr(t), null);
+ fe = new FrameExpression(new WildcardExpr(t), null);
} else if (StartOf(8)) {
FrameExpression(out fe);
} else SynErr(115);
@@ -882,10 +881,10 @@ List<Expression/*!*/>/*!*/ decreases) { void PossiblyWildExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
- e = dummyExpr;
+ e = dummyExpr;
if (la.kind == 39) {
Get();
- e = new WildcardExpr(t);
+ e = new WildcardExpr(t);
} else if (StartOf(8)) {
Expression(out e);
} else SynErr(116);
@@ -896,13 +895,13 @@ List<Expression/*!*/>/*!*/ decreases) { List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
Expect(41);
- x = t;
+ x = t;
Expression(out e);
while (la.kind == 42) {
CaseExpression(out c);
- cases.Add(c);
+ cases.Add(c);
}
- e = new MatchExpr(x, e, cases);
+ e = new MatchExpr(x, e, cases);
}
void CaseExpression(out MatchCaseExpr/*!*/ c) {
@@ -911,36 +910,36 @@ List<Expression/*!*/>/*!*/ decreases) { Expression/*!*/ body;
Expect(42);
- x = t; parseVarScope.PushMarker();
+ x = t; parseVarScope.PushMarker();
Ident(out id);
if (la.kind == 29) {
Get();
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
- parseVarScope.Push(arg.val, arg.val);
+ parseVarScope.Push(arg.val, arg.val);
while (la.kind == 16) {
Get();
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
- parseVarScope.Push(arg.val, arg.val);
+ parseVarScope.Push(arg.val, arg.val);
}
Expect(30);
}
Expect(43);
Expression(out body);
c = new MatchCaseExpr(x, id.val, arguments, body);
- parseVarScope.PopMarker();
+ parseVarScope.PopMarker();
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
- Contract.Requires(cce.NonNullElements(ss)); Statement/*!*/ s;
+ Contract.Requires(cce.NonNullElements(ss)); Statement/*!*/ s;
while (la.kind == 6) {
BlockStmt(out s);
- ss.Add(s);
+ ss.Add(s);
}
if (StartOf(11)) {
OneStmt(out s);
- ss.Add(s);
+ ss.Add(s);
} else if (la.kind == 10 || la.kind == 15) {
VarDeclStmts(ss);
} else SynErr(117);
@@ -997,28 +996,28 @@ List<Expression/*!*/>/*!*/ decreases) { }
case 44: {
Get();
- x = t;
+ x = t;
Ident(out id);
Expect(19);
- s = new LabelStmt(x, id.val);
+ s = new LabelStmt(x, id.val);
break;
}
case 45: {
Get();
- x = t;
+ x = t;
if (la.kind == 1) {
Ident(out id);
- label = id.val;
+ label = id.val;
}
Expect(14);
- s = new BreakStmt(x, label);
+ s = new BreakStmt(x, label);
break;
}
case 46: {
Get();
- x = t;
+ x = t;
Expect(14);
- s = new ReturnStmt(x);
+ s = new ReturnStmt(x);
break;
}
default: SynErr(118); break;
@@ -1026,47 +1025,47 @@ List<Expression/*!*/>/*!*/ decreases) { }
void VarDeclStmts(List<Statement/*!*/>/*!*/ ss) {
- Contract.Requires(cce.NonNullElements(ss)); VarDecl/*!*/ d; bool isGhost = false;
+ Contract.Requires(cce.NonNullElements(ss)); VarDecl/*!*/ d; bool isGhost = false;
if (la.kind == 10) {
Get();
- isGhost = true;
+ isGhost = true;
}
Expect(15);
IdentTypeRhs(out d, isGhost);
- ss.Add(d); parseVarScope.Push(d.Name, d.Name);
+ ss.Add(d); parseVarScope.Push(d.Name, d.Name);
while (la.kind == 16) {
Get();
IdentTypeRhs(out d, isGhost);
- ss.Add(d); parseVarScope.Push(d.Name, d.Name);
+ ss.Add(d); parseVarScope.Push(d.Name, d.Name);
}
Expect(14);
}
void AssertStmt(out Statement/*!*/ s) {
- Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
+ Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
Expect(60);
- x = t;
+ x = t;
Expression(out e);
Expect(14);
- s = new AssertStmt(x, e);
+ s = new AssertStmt(x, e);
}
void AssumeStmt(out Statement/*!*/ s) {
- Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
+ Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
Expect(61);
- x = t;
+ x = t;
Expression(out e);
Expect(14);
- s = new AssumeStmt(x, e);
+ s = new AssumeStmt(x, e);
}
void UseStmt(out Statement/*!*/ s) {
- Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
+ Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
Expect(62);
- x = t;
+ x = t;
Expression(out e);
Expect(14);
- s = new UseStmt(x, e);
+ s = new UseStmt(x, e);
}
void PrintStmt(out Statement/*!*/ s) {
@@ -1074,16 +1073,16 @@ List<Expression/*!*/>/*!*/ decreases) { List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
Expect(63);
- x = t;
+ x = t;
AttributeArg(out arg);
- args.Add(arg);
+ args.Add(arg);
while (la.kind == 16) {
Get();
AttributeArg(out arg);
- args.Add(arg);
+ args.Add(arg);
}
Expect(14);
- s = new PrintStmt(x, args);
+ s = new PrintStmt(x, args);
}
void AssignStmt(out Statement/*!*/ s) {
@@ -1095,7 +1094,7 @@ List<Expression/*!*/>/*!*/ decreases) { LhsExpr(out lhs);
Expect(47);
- x = t;
+ x = t;
AssignRhs(out rhs, out ty);
if (ty == null) {
Contract.Assert(rhs != null);
@@ -1103,19 +1102,19 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (rhs == null) {
s = new AssignStmt(x, lhs, ty);
} else {
- s = new AssignStmt(x, lhs, ty, rhs);
+ s = new AssignStmt(x, lhs, ty, new List<Expression>(new Expression[] { rhs }));
}
Expect(14);
}
void HavocStmt(out Statement/*!*/ s) {
- Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ lhs;
+ Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ lhs;
Expect(51);
- x = t;
+ x = t;
LhsExpr(out lhs);
Expect(14);
- s = new AssignStmt(x, lhs);
+ s = new AssignStmt(x, lhs);
}
void CallStmt(out Statement/*!*/ s) {
@@ -1125,7 +1124,7 @@ List<Expression/*!*/>/*!*/ decreases) { List<AutoVarDecl/*!*/> newVars = new List<AutoVarDecl/*!*/>();
Expect(56);
- x = t;
+ x = t;
CallStmtSubExpr(out e);
if (la.kind == 16 || la.kind == 47) {
if (la.kind == 16) {
@@ -1140,11 +1139,11 @@ List<Expression/*!*/>/*!*/ decreases) { }
Ident(out id);
- RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars);
+ RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars);
while (la.kind == 16) {
Get();
Ident(out id);
- RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars);
+ RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars);
}
Expect(47);
CallStmtSubExpr(out e);
@@ -1181,20 +1180,20 @@ List<Expression/*!*/>/*!*/ decreases) { Statement els = null;
Expect(52);
- x = t;
+ x = t;
Guard(out guard);
BlockStmt(out thn);
if (la.kind == 53) {
Get();
if (la.kind == 52) {
IfStmt(out s);
- els = s;
+ els = s;
} else if (la.kind == 6) {
BlockStmt(out s);
- els = s;
+ els = s;
} else SynErr(119);
}
- ifStmt = new IfStmt(x, guard, thn, els);
+ ifStmt = new IfStmt(x, guard, thn, els);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -1206,50 +1205,50 @@ List<Expression/*!*/>/*!*/ decreases) { Statement/*!*/ body;
Expect(54);
- x = t;
+ x = t;
Guard(out guard);
- Contract.Assume(guard == null || cce.Owner.None(guard));
+ Contract.Assume(guard == null || cce.Owner.None(guard));
while (la.kind == 25 || la.kind == 28 || la.kind == 55) {
if (la.kind == 25 || la.kind == 55) {
- isFree = false;
+ isFree = false;
if (la.kind == 25) {
Get();
- isFree = true;
+ isFree = true;
}
Expect(55);
Expression(out e);
- invariants.Add(new MaybeFreeExpression(e, isFree));
+ invariants.Add(new MaybeFreeExpression(e, isFree));
Expect(14);
} else {
Get();
PossiblyWildExpression(out e);
- decreases.Add(e);
+ decreases.Add(e);
while (la.kind == 16) {
Get();
PossiblyWildExpression(out e);
- decreases.Add(e);
+ decreases.Add(e);
}
Expect(14);
}
}
BlockStmt(out body);
- stmt = new WhileStmt(x, guard, invariants, decreases, body);
+ stmt = new WhileStmt(x, guard, invariants, decreases, body);
}
void MatchStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c;
- List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>();
+ List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>();
Expect(41);
- x = t;
+ x = t;
Expression(out e);
Expect(6);
while (la.kind == 42) {
CaseStatement(out c);
- cases.Add(c);
+ cases.Add(c);
}
Expect(7);
- s = new MatchStmt(x, e, cases);
+ s = new MatchStmt(x, e, cases);
}
void ForeachStmt(out Statement/*!*/ s) {
@@ -1260,7 +1259,7 @@ List<Expression/*!*/>/*!*/ decreases) { List<PredicateStmt/*!*/> bodyPrefix = new List<PredicateStmt/*!*/>();
AssignStmt bodyAssign = null;
- parseVarScope.PushMarker();
+ parseVarScope.PushMarker();
Expect(57);
x = t;
range = new LiteralExpr(x, true);
@@ -1274,7 +1273,7 @@ List<Expression/*!*/>/*!*/ decreases) { }
Expect(58);
Expression(out collection);
- parseVarScope.Push(boundVar.val, boundVar.val);
+ parseVarScope.Push(boundVar.val, boundVar.val);
if (la.kind == 59) {
Get();
Expression(out range);
@@ -1307,7 +1306,7 @@ List<Expression/*!*/>/*!*/ decreases) { s = dummyStmt; // some error occurred in parsing the bodyAssign
}
- parseVarScope.PopMarker();
+ parseVarScope.PopMarker();
}
void LhsExpr(out Expression/*!*/ e) {
@@ -1322,22 +1321,22 @@ List<Expression/*!*/>/*!*/ decreases) { if (la.kind == 48) {
Get();
TypeAndToken(out x, out tt);
- ty = tt;
+ ty = tt;
if (la.kind == 49) {
Get();
Expression(out ee);
Expect(50);
- e = ee;
+ e = ee;
}
} else if (StartOf(8)) {
Expression(out ee);
- e = ee;
+ e = ee;
} else SynErr(121);
if (e == null && ty == null) { e = dummyExpr; }
}
void SelectExpression(out Expression/*!*/ e) {
- Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ id; e = dummyExpr;
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr;
if (la.kind == 1) {
IdentOrFuncExpression(out e);
} else if (la.kind == 29 || la.kind == 95 || la.kind == 96) {
@@ -1349,7 +1348,7 @@ List<Expression/*!*/>/*!*/ decreases) { }
void IdentTypeRhs(out VarDecl/*!*/ d, bool isGhost) {
- Contract.Ensures(Contract.ValueAtReturn(out d) != null); IToken/*!*/ id; Type/*!*/ ty; Expression/*!*/ e;
+ Contract.Ensures(Contract.ValueAtReturn(out d) != null); IToken/*!*/ id; Type/*!*/ ty;
Expression rhs = null; Type newType = null;
Type optionalType = null; DeterminedAssignmentRhs optionalRhs = null;
@@ -1357,7 +1356,7 @@ List<Expression/*!*/>/*!*/ decreases) { if (la.kind == 19) {
Get();
Type(out ty);
- optionalType = ty;
+ optionalType = ty;
}
if (la.kind == 47) {
Get();
@@ -1369,7 +1368,7 @@ List<Expression/*!*/>/*!*/ decreases) { if (rhs == null) {
optionalRhs = new TypeRhs(newType);
} else {
- optionalRhs = new TypeRhs(newType, rhs);
+ optionalRhs = new TypeRhs(newType, new List<Expression>(new Expression[] { rhs }));
}
} else if (optionalType == null) {
optionalType = new InferredTypeProxy();
@@ -1379,14 +1378,14 @@ List<Expression/*!*/>/*!*/ decreases) { }
void Guard(out Expression e) {
- Expression/*!*/ ee; e = null;
+ Expression/*!*/ ee; e = null;
Expect(29);
if (la.kind == 39) {
Get();
- e = null;
+ e = null;
} else if (StartOf(8)) {
Expression(out ee);
- e = ee;
+ e = ee;
} else SynErr(123);
Expect(30);
}
@@ -1398,33 +1397,33 @@ List<Expression/*!*/>/*!*/ decreases) { List<Statement/*!*/> body = new List<Statement/*!*/>();
Expect(42);
- x = t; parseVarScope.PushMarker();
+ x = t; parseVarScope.PushMarker();
Ident(out id);
if (la.kind == 29) {
Get();
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
- parseVarScope.Push(arg.val, arg.val);
+ parseVarScope.Push(arg.val, arg.val);
while (la.kind == 16) {
Get();
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
- parseVarScope.Push(arg.val, arg.val);
+ parseVarScope.Push(arg.val, arg.val);
}
Expect(30);
}
Expect(43);
- parseVarScope.PushMarker();
+ parseVarScope.PushMarker();
while (StartOf(9)) {
Stmt(body);
}
- parseVarScope.PopMarker();
- c = new MatchCaseStmt(x, id.val, arguments, body);
- parseVarScope.PopMarker();
+ parseVarScope.PopMarker();
+ c = new MatchCaseStmt(x, id.val, arguments, body);
+ parseVarScope.PopMarker();
}
void CallStmtSubExpr(out Expression/*!*/ e) {
- Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr;
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr;
if (la.kind == 1) {
IdentOrFuncExpression(out e);
} else if (la.kind == 29 || la.kind == 95 || la.kind == 96) {
@@ -1437,35 +1436,35 @@ List<Expression/*!*/>/*!*/ decreases) { }
void AttributeArg(out Attributes.Argument/*!*/ arg) {
- Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e; arg = dummyAttrArg;
+ Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e; arg = dummyAttrArg;
if (la.kind == 3) {
Get();
- arg = new Attributes.Argument(t.val.Substring(1, t.val.Length-2));
+ arg = new Attributes.Argument(t.val.Substring(1, t.val.Length-2));
} else if (StartOf(8)) {
Expression(out e);
- arg = new Attributes.Argument(e);
+ arg = new Attributes.Argument(e);
} else SynErr(125);
}
void EquivExpression(out Expression/*!*/ e0) {
- Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
+ Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
ImpliesExpression(out e0);
while (la.kind == 65 || la.kind == 66) {
EquivOp();
- x = t;
+ x = t;
ImpliesExpression(out e1);
- e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1);
+ e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1);
}
}
void ImpliesExpression(out Expression/*!*/ e0) {
- Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
+ Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
LogicalExpression(out e0);
if (la.kind == 67 || la.kind == 68) {
ImpliesOp();
- x = t;
+ x = t;
ImpliesExpression(out e1);
- e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1);
+ e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1);
}
}
@@ -1478,30 +1477,30 @@ List<Expression/*!*/>/*!*/ decreases) { }
void LogicalExpression(out Expression/*!*/ e0) {
- Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
+ Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
if (StartOf(13)) {
if (la.kind == 69 || la.kind == 70) {
AndOp();
- x = t;
+ x = t;
RelationalExpression(out e1);
- e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
+ e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
while (la.kind == 69 || la.kind == 70) {
AndOp();
- x = t;
+ x = t;
RelationalExpression(out e1);
- e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
+ e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
}
} else {
OrOp();
- x = t;
+ x = t;
RelationalExpression(out e1);
- e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
+ e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
while (la.kind == 71 || la.kind == 72) {
OrOp();
- x = t;
+ x = t;
RelationalExpression(out e1);
- e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
+ e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
}
}
}
@@ -1516,12 +1515,12 @@ List<Expression/*!*/>/*!*/ decreases) { }
void RelationalExpression(out Expression/*!*/ e0) {
- Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
+ Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
Term(out e0);
if (StartOf(14)) {
RelOp(out x, out op);
Term(out e1);
- e0 = new BinaryExpr(x, op, e0, e1);
+ e0 = new BinaryExpr(x, op, e0, e1);
}
}
@@ -1542,76 +1541,76 @@ List<Expression/*!*/>/*!*/ decreases) { }
void Term(out Expression/*!*/ e0) {
- Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
+ Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
Factor(out e0);
while (la.kind == 82 || la.kind == 83) {
AddOp(out x, out op);
Factor(out e1);
- e0 = new BinaryExpr(x, op, e0, e1);
+ e0 = new BinaryExpr(x, op, e0, e1);
}
}
void RelOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
- Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
+ Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
switch (la.kind) {
case 73: {
Get();
- x = t; op = BinaryExpr.Opcode.Eq;
+ x = t; op = BinaryExpr.Opcode.Eq;
break;
}
case 20: {
Get();
- x = t; op = BinaryExpr.Opcode.Lt;
+ x = t; op = BinaryExpr.Opcode.Lt;
break;
}
case 21: {
Get();
- x = t; op = BinaryExpr.Opcode.Gt;
+ x = t; op = BinaryExpr.Opcode.Gt;
break;
}
case 74: {
Get();
- x = t; op = BinaryExpr.Opcode.Le;
+ x = t; op = BinaryExpr.Opcode.Le;
break;
}
case 75: {
Get();
- x = t; op = BinaryExpr.Opcode.Ge;
+ x = t; op = BinaryExpr.Opcode.Ge;
break;
}
case 76: {
Get();
- x = t; op = BinaryExpr.Opcode.Neq;
+ x = t; op = BinaryExpr.Opcode.Neq;
break;
}
case 77: {
Get();
- x = t; op = BinaryExpr.Opcode.Disjoint;
+ x = t; op = BinaryExpr.Opcode.Disjoint;
break;
}
case 58: {
Get();
- x = t; op = BinaryExpr.Opcode.In;
+ x = t; op = BinaryExpr.Opcode.In;
break;
}
case 78: {
Get();
- x = t; op = BinaryExpr.Opcode.NotIn;
+ x = t; op = BinaryExpr.Opcode.NotIn;
break;
}
case 79: {
Get();
- x = t; op = BinaryExpr.Opcode.Neq;
+ x = t; op = BinaryExpr.Opcode.Neq;
break;
}
case 80: {
Get();
- x = t; op = BinaryExpr.Opcode.Le;
+ x = t; op = BinaryExpr.Opcode.Le;
break;
}
case 81: {
Get();
- x = t; op = BinaryExpr.Opcode.Ge;
+ x = t; op = BinaryExpr.Opcode.Ge;
break;
}
default: SynErr(130); break;
@@ -1619,38 +1618,38 @@ List<Expression/*!*/>/*!*/ decreases) { }
void Factor(out Expression/*!*/ e0) {
- Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
+ Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
while (la.kind == 39 || la.kind == 84 || la.kind == 85) {
MulOp(out x, out op);
UnaryExpression(out e1);
- e0 = new BinaryExpr(x, op, e0, e1);
+ e0 = new BinaryExpr(x, op, e0, e1);
}
}
void AddOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
- Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
+ Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
if (la.kind == 82) {
Get();
- x = t; op = BinaryExpr.Opcode.Add;
+ x = t; op = BinaryExpr.Opcode.Add;
} else if (la.kind == 83) {
Get();
- x = t; op = BinaryExpr.Opcode.Sub;
+ x = t; op = BinaryExpr.Opcode.Sub;
} else SynErr(131);
}
void UnaryExpression(out Expression/*!*/ e) {
- Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
if (la.kind == 83) {
Get();
- x = t;
+ x = t;
UnaryExpression(out e);
- e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
+ e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
} else if (la.kind == 86 || la.kind == 87) {
NegOp();
- x = t;
+ x = t;
UnaryExpression(out e);
- e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
+ e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
} else if (StartOf(12)) {
SelectExpression(out e);
} else if (StartOf(15)) {
@@ -1659,16 +1658,16 @@ List<Expression/*!*/>/*!*/ decreases) { }
void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
- Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
+ Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
if (la.kind == 39) {
Get();
- x = t; op = BinaryExpr.Opcode.Mul;
+ x = t; op = BinaryExpr.Opcode.Mul;
} else if (la.kind == 84) {
Get();
- x = t; op = BinaryExpr.Opcode.Div;
+ x = t; op = BinaryExpr.Opcode.Div;
} else if (la.kind == 85) {
Get();
- x = t; op = BinaryExpr.Opcode.Mod;
+ x = t; op = BinaryExpr.Opcode.Mod;
} else SynErr(133);
}
@@ -1687,31 +1686,31 @@ List<Expression/*!*/>/*!*/ decreases) { switch (la.kind) {
case 88: {
Get();
- e = new LiteralExpr(t, false);
+ e = new LiteralExpr(t, false);
break;
}
case 89: {
Get();
- e = new LiteralExpr(t, true);
+ e = new LiteralExpr(t, true);
break;
}
case 90: {
Get();
- e = new LiteralExpr(t);
+ e = new LiteralExpr(t);
break;
}
case 2: {
Nat(out n);
- e = new LiteralExpr(t, n);
+ e = new LiteralExpr(t, n);
break;
}
case 91: {
Get();
- x = t;
+ x = t;
Ident(out dtName);
Expect(92);
Ident(out id);
- elements = new List<Expression/*!*/>();
+ elements = new List<Expression/*!*/>();
if (la.kind == 29) {
Get();
if (StartOf(8)) {
@@ -1719,43 +1718,43 @@ List<Expression/*!*/>/*!*/ decreases) { }
Expect(30);
}
- e = new DatatypeValue(t, dtName.val, id.val, elements);
+ e = new DatatypeValue(t, dtName.val, id.val, elements);
break;
}
case 93: {
Get();
- x = t;
+ x = t;
Expect(29);
Expression(out e);
Expect(30);
- e = new FreshExpr(x, e);
+ e = new FreshExpr(x, e);
break;
}
case 59: {
Get();
- x = t;
+ x = t;
Expression(out e);
- e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e);
+ e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e);
Expect(59);
break;
}
case 6: {
Get();
- x = t; elements = new List<Expression/*!*/>();
+ x = t; elements = new List<Expression/*!*/>();
if (StartOf(8)) {
Expressions(elements);
}
- e = new SetDisplayExpr(x, elements);
+ e = new SetDisplayExpr(x, elements);
Expect(7);
break;
}
case 49: {
Get();
- x = t; elements = new List<Expression/*!*/>();
+ x = t; elements = new List<Expression/*!*/>();
if (StartOf(8)) {
Expressions(elements);
}
- e = new SeqDisplayExpr(x, elements);
+ e = new SeqDisplayExpr(x, elements);
Expect(50);
break;
}
@@ -1775,16 +1774,16 @@ List<Expression/*!*/>/*!*/ decreases) { }
void IdentOrFuncExpression(out Expression/*!*/ e) {
- Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ id; e = dummyExpr; List<Expression/*!*/>/*!*/ args;
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ id; e = dummyExpr; List<Expression/*!*/>/*!*/ args;
Ident(out id);
if (la.kind == 29) {
Get();
- args = new List<Expression/*!*/>();
+ args = new List<Expression/*!*/>();
if (StartOf(8)) {
Expressions(args);
}
Expect(30);
- e = new FunctionCallExpr(id, id.val, new ImplicitThisExpr(id), args);
+ e = new FunctionCallExpr(id, id.val, new ImplicitThisExpr(id), args);
}
if (e == dummyExpr) {
if (parseVarScope.Find(id.val) != null) {
@@ -1797,17 +1796,17 @@ List<Expression/*!*/>/*!*/ decreases) { }
void ObjectExpression(out Expression/*!*/ e) {
- Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
if (la.kind == 95) {
Get();
- e = new ThisExpr(t);
+ e = new ThisExpr(t);
} else if (la.kind == 96) {
Get();
- x = t;
+ x = t;
Expect(29);
Expression(out e);
Expect(30);
- e = new OldExpr(x, e);
+ e = new OldExpr(x, e);
} else if (la.kind == 29) {
Get();
if (StartOf(16)) {
@@ -1829,38 +1828,38 @@ List<Expression/*!*/>/*!*/ decreases) { Ident(out id);
if (la.kind == 29) {
Get();
- args = new List<Expression/*!*/>(); func = true;
+ args = new List<Expression/*!*/>(); func = true;
if (StartOf(8)) {
Expressions(args);
}
Expect(30);
- e = new FunctionCallExpr(id, id.val, e, args);
+ e = new FunctionCallExpr(id, id.val, e, args);
}
if (!func) { e = new FieldSelectExpr(id, e, id.val); }
} else if (la.kind == 49) {
Get();
- x = t;
+ x = t;
if (StartOf(8)) {
Expression(out ee);
- e0 = ee;
+ e0 = ee;
if (la.kind == 47 || la.kind == 94) {
if (la.kind == 94) {
Get();
- anyDots = true;
+ anyDots = true;
if (StartOf(8)) {
Expression(out ee);
- e1 = ee;
+ e1 = ee;
}
} else {
Get();
Expression(out ee);
- e1 = ee;
+ e1 = ee;
}
}
} else if (la.kind == 94) {
Get();
Expression(out ee);
- anyDots = true; e1 = ee;
+ anyDots = true; e1 = ee;
} else SynErr(138);
if (!anyDots && e0 == null) {
/* a parsing error occurred */
@@ -1887,25 +1886,24 @@ List<Expression/*!*/>/*!*/ decreases) { bool univ = false;
BoundVar/*!*/ bv;
List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
- IToken/*!*/ tok; Expr/*!*/ e; ExprSeq/*!*/ es;
Attributes attrs = null;
Triggers trigs = null;
Expression/*!*/ body;
if (la.kind == 97 || la.kind == 98) {
Forall();
- x = t; univ = true;
+ x = t; univ = true;
} else if (la.kind == 99 || la.kind == 100) {
Exists();
- x = t;
+ x = t;
} else SynErr(140);
- parseVarScope.PushMarker();
+ parseVarScope.PushMarker();
IdentTypeOptional(out bv);
- bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
+ bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
while (la.kind == 16) {
Get();
IdentTypeOptional(out bv);
- bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
+ bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
}
while (la.kind == 6) {
AttributeOrTrigger(ref attrs, ref trigs);
@@ -1944,9 +1942,9 @@ List<Expression/*!*/>/*!*/ decreases) { if (la.kind == 19) {
AttributeBody(ref attrs);
} else if (StartOf(8)) {
- es = new List<Expression/*!*/>();
+ es = new List<Expression/*!*/>();
Expressions(es);
- trigs = new Triggers(es, trigs);
+ trigs = new Triggers(es, trigs);
} else SynErr(143);
Expect(7);
}
@@ -1966,17 +1964,17 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(19);
Expect(1);
- aName = t.val;
+ aName = t.val;
if (StartOf(17)) {
AttributeArg(out aArg);
- aArgs.Add(aArg);
+ aArgs.Add(aArg);
while (la.kind == 16) {
Get();
AttributeArg(out aArg);
- aArgs.Add(aArg);
+ aArgs.Add(aArg);
}
}
- attrs = new Attributes(aName, aArgs, attrs);
+ attrs = new Attributes(aName, aArgs, attrs);
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index a0d0e583..31c43a44 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -578,9 +578,14 @@ void ObjectInvariant() TypeRhs t = (TypeRhs)rhs;
wr.Write("new ");
PrintType(t.EType);
- if (t.ArraySize != null) {
- wr.Write("[");
- PrintExpression(t.ArraySize);
+ if (t.ArrayDimensions != null) {
+ string s = "[";
+ foreach (Expression dim in t.ArrayDimensions) {
+ Contract.Requires(dim != null);
+ wr.Write(s);
+ PrintExpression(dim);
+ s = ", ";
+ }
wr.Write("]");
}
} else {
@@ -735,7 +740,26 @@ void ObjectInvariant() }
wr.Write("]");
if (parensNeeded) { wr.Write(")"); }
-
+
+ } else if (expr is MultiSelectExpr) {
+ MultiSelectExpr e = (MultiSelectExpr)expr;
+ // determine if parens are needed
+ int opBindingStrength = 0x70;
+ bool parensNeeded = opBindingStrength < contextBindingStrength ||
+ (fragileContext && opBindingStrength == contextBindingStrength);
+
+ if (parensNeeded) { wr.Write("("); }
+ PrintExpr(e.Array, 0x00, false, indent); // BOGUS: fix me
+ string prefix = "[";
+ foreach (Expression idx in e.Indices) {
+ Contract.Assert(idx != null);
+ wr.Write(prefix);
+ PrintExpression(idx);
+ prefix = ", ";
+ }
+ wr.Write("]");
+ if (parensNeeded) { wr.Write(")"); }
+
} else if (expr is SeqUpdateExpr) {
SeqUpdateExpr e = (SeqUpdateExpr)expr;
// determine if parens are needed
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index ff658378..c3dceb97 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -983,7 +983,7 @@ void ObjectInvariant() return true;
} else if (b is IndexableTypeProxy) {
// the intersection of ObjectTypeProxy and IndexableTypeProxy is an array type
- a.T = UserDefinedType.ArrayType(Token.NoToken, ((IndexableTypeProxy)b).Arg);
+ a.T = UserDefinedType.ArrayType(Token.NoToken, 1, ((IndexableTypeProxy)b).Arg);
b.T = a.T;
return true;
} else {
@@ -1167,7 +1167,7 @@ void ObjectInvariant() if (lhsResolvedSuccessfully) {
Contract.Assert( lhs.Seq.Type != null);
Type elementType = new InferredTypeProxy();
- if (!UnifyTypes(lhs.Seq.Type, UserDefinedType.ArrayType(Token.NoToken, elementType))) {
+ if (!UnifyTypes(lhs.Seq.Type, UserDefinedType.ArrayType(Token.NoToken, 1, elementType))) {
Error(lhs.Seq, "LHS of array assignment must denote an array element (found {0})", lhs.Seq.Type);
}
if (specContextOnly) {
@@ -1178,6 +1178,14 @@ void ObjectInvariant() Error(stmt, "Assignment to array element must have an expression RHS; try using a temporary local variable");
}
+ } else if (s.Lhs is MultiSelectExpr) {
+ if (specContextOnly) {
+ Error(stmt, "Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
+ }
+ if (!(s.Rhs is ExprRhs)) {
+ Error(stmt, "Assignment to array element must have an expression RHS; try using a temporary local variable");
+ }
+
} else {
Error(stmt, "LHS of assignment must denote a mutable variable or field");
}
@@ -1556,20 +1564,23 @@ void ObjectInvariant() Contract.Ensures(Contract.Result<Type>() != null);
ResolveType(rr.EType);
- if (rr.ArraySize == null) {
+ if (rr.ArrayDimensions == null) {
if (!rr.EType.IsRefType) {
Error(stmt, "new can be applied only to reference types (got {0})", rr.EType);
}
+ return rr.EType;
} else {
- ResolveExpression(rr.ArraySize, true, specContext);
- if (rr.ArraySize.Type is IntType) {
- // all is good
- return UserDefinedType.ArrayType(stmt.Tok, rr.EType);
- } else {
- Error(stmt, "new must use an integer expression for the array size (got {0})", rr.ArraySize.Type);
+ int i = 0;
+ foreach (Expression dim in rr.ArrayDimensions) {
+ Contract.Assert(dim != null);
+ ResolveExpression(dim, true, specContext);
+ if (!UnifyTypes(dim.Type, Type.Int)) {
+ Error(stmt, "new must use an integer expression for the array size (got {0} for index {1})", dim.Type, i);
+ }
+ i++;
}
+ return UserDefinedType.ArrayType(stmt.Tok, rr.ArrayDimensions.Count, rr.EType);
}
- return rr.EType;
}
MemberDecl ResolveMember(IToken tok, Type receiverType, string memberName, out UserDefinedType ctype)
@@ -1819,7 +1830,28 @@ void ObjectInvariant() } else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
ResolveSeqSelectExpr(e, twoState, specContext, false);
-
+
+ } else if (expr is MultiSelectExpr) {
+ MultiSelectExpr e = (MultiSelectExpr)expr;
+
+ ResolveExpression(e.Array, twoState, specContext);
+ Contract.Assert(e.Array.Type != null); // follows from postcondition of ResolveExpression
+ Type elementType = new InferredTypeProxy();
+ if (!UnifyTypes(e.Array.Type, UserDefinedType.ArrayType(Token.NoToken, 1, elementType))) {
+ Error(e.Array, "array selection requires an array (got {0})", e.Array.Type);
+ }
+ int i = 0;
+ foreach (Expression idx in e.Indices) {
+ Contract.Assert(idx != null);
+ ResolveExpression(idx, twoState, specContext);
+ Contract.Assert(idx.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(idx.Type, Type.Int)) {
+ Error(idx, "array selection requires integer indices (got {0} for index {1})", idx.Type, i);
+ }
+ i++;
+ }
+ e.Type = elementType;
+
} else if (expr is SeqUpdateExpr) {
SeqUpdateExpr e = (SeqUpdateExpr)expr;
bool seqErr = false;
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index b9f36a87..b7224070 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -253,40 +253,40 @@ void objectInvariant(){ for (int i = 97; i <= 122; ++i) start[i] = 1;
for (int i = 48; i <= 57; ++i) start[i] = 2;
for (int i = 34; i <= 34; ++i) start[i] = 3;
- start[123] = 5;
- start[125] = 6;
- start[59] = 7;
- start[44] = 8;
- start[58] = 46;
- start[60] = 47;
- start[62] = 48;
- start[40] = 9;
- start[41] = 10;
- start[42] = 11;
- start[96] = 12;
- start[61] = 49;
- start[91] = 15;
- start[93] = 16;
- start[124] = 50;
- start[8660] = 19;
- start[8658] = 21;
- start[38] = 22;
- start[8743] = 24;
- start[8744] = 26;
- start[33] = 51;
- start[8800] = 32;
- start[8804] = 33;
- start[8805] = 34;
- start[43] = 35;
- start[45] = 36;
- start[47] = 37;
- start[37] = 38;
- start[172] = 39;
- start[35] = 40;
- start[46] = 52;
- start[8704] = 42;
- start[8707] = 43;
- start[8226] = 45;
+ start[123] = 5;
+ start[125] = 6;
+ start[59] = 7;
+ start[44] = 8;
+ start[58] = 46;
+ start[60] = 47;
+ start[62] = 48;
+ start[40] = 9;
+ start[41] = 10;
+ start[42] = 11;
+ start[96] = 12;
+ start[61] = 49;
+ start[91] = 15;
+ start[93] = 16;
+ start[124] = 50;
+ start[8660] = 19;
+ start[8658] = 21;
+ start[38] = 22;
+ start[8743] = 24;
+ start[8744] = 26;
+ start[33] = 51;
+ start[8800] = 32;
+ start[8804] = 33;
+ start[8805] = 34;
+ start[43] = 35;
+ start[45] = 36;
+ start[47] = 37;
+ start[37] = 38;
+ start[172] = 39;
+ start[35] = 40;
+ start[46] = 52;
+ start[8704] = 42;
+ start[8707] = 43;
+ start[8226] = 45;
start[Buffer.EOF] = -1;
}
@@ -374,7 +374,7 @@ void objectInvariant(){ // eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
if (ch == EOL) {
- line++; col = 0;
+ line++; col = 0; } else if (ch == '#' && col == 1) {
int prLine = line;
int prColumn = 0;
@@ -552,7 +552,7 @@ void objectInvariant(){ int recKind = noSym;
int recEnd = pos;
t = new Token();
- t.pos = pos; t.col = col; t.line = line;
+ t.pos = pos; t.col = col; t.line = line; t.filename = this.Filename;
int state;
if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index b7a37d23..6d106855 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -36,20 +36,20 @@ namespace Microsoft.Dafny { readonly Dictionary<string/*!*/,Bpl.Constant/*!*/>/*!*/ cevVariables = new Dictionary<string/*!*/,Bpl.Constant/*!*/>();
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(cce.NonNullElements(classes));
+ void ObjectInvariant()
+ {
+ Contract.Invariant(cce.NonNullElements(classes));
Contract.Invariant(cce.NonNullElements(fields));
Contract.Invariant(cce.NonNullElements(cevFilenames));
Contract.Invariant(cce.NonNullElements(cevLocations));
Contract.Invariant(cce.NonNullElements(cevVariables));
-}
+ }
Bpl.Expr CevLocation(IToken tok)
- {
+ {
Contract.Requires(tok != null);
- Contract.Requires( predef != null && sink != null);
+ Contract.Requires( predef != null && sink != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
@@ -121,7 +121,6 @@ void ObjectInvariant() public readonly string HeapVarName;
public readonly Bpl.Constant CevHeapName;
public readonly Bpl.Type ClassNameType;
- public readonly Bpl.Type FieldCategoryType;
public readonly Bpl.Type DatatypeType;
public readonly Bpl.Type DtCtorId;
public readonly Bpl.Expr Null;
@@ -141,7 +140,6 @@ void ObjectInvariant() Contract.Invariant(HeapVarName != null);
Contract.Invariant(CevEventType != null);
Contract.Invariant(ClassNameType != null);
- Contract.Invariant(FieldCategoryType != null);
Contract.Invariant(DatatypeType != null);
Contract.Invariant(DtCtorId != null);
Contract.Invariant(Null != null);
@@ -182,7 +180,7 @@ void ObjectInvariant() public PredefinedDecls(Bpl.TypeCtorDecl refType, Bpl.TypeCtorDecl boxType, Bpl.TypeCtorDecl cevTokenType,
Bpl.TypeCtorDecl cevVariableKind, Bpl.TypeCtorDecl cevEventType,
Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType,
- Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType, Bpl.TypeCtorDecl fieldCategoryType,
+ Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType,
Bpl.TypeCtorDecl datatypeType, Bpl.TypeCtorDecl dtCtorId,
Bpl.Constant allocField, Bpl.Constant cevHeapNameConst) {
#region Non-null preconditions on parameters
@@ -196,7 +194,6 @@ void ObjectInvariant() Contract.Requires(fieldNameType != null);
Contract.Requires(heap != null);
Contract.Requires(classNameType != null);
- Contract.Requires(fieldCategoryType != null);
Contract.Requires(datatypeType != null);
Contract.Requires(dtCtorId != null);
Contract.Requires(allocField != null);
@@ -216,7 +213,6 @@ void ObjectInvariant() this.HeapVarName = heap.Name;
this.CevHeapName = cevHeapNameConst;
this.ClassNameType = new Bpl.CtorType(Token.NoToken, classNameType, new Bpl.TypeSeq());
- this.FieldCategoryType = new Bpl.CtorType(Token.NoToken, fieldCategoryType, new Bpl.TypeSeq());
this.DatatypeType = new Bpl.CtorType(Token.NoToken, datatypeType, new Bpl.TypeSeq());
this.DtCtorId = new Bpl.CtorType(Token.NoToken, dtCtorId, new Bpl.TypeSeq());
this.allocField = allocField;
@@ -239,7 +235,6 @@ void ObjectInvariant() Bpl.TypeCtorDecl seqTypeCtor = null;
Bpl.TypeCtorDecl fieldNameType = null;
Bpl.TypeCtorDecl classNameType = null;
- Bpl.TypeCtorDecl fieldCategoryType = null;
Bpl.TypeCtorDecl datatypeType = null;
Bpl.TypeCtorDecl dtCtorId = null;
Bpl.TypeCtorDecl boxType = null;
@@ -255,8 +250,6 @@ void ObjectInvariant() fieldNameType = dt;
} else if (dt.Name == "ClassName") {
classNameType = dt;
- } else if (dt.Name == "FieldCategory") {
- fieldCategoryType = dt;
} else if (dt.Name == "DatatypeType") {
datatypeType = dt;
} else if (dt.Name == "DtCtorId") {
@@ -299,8 +292,6 @@ void ObjectInvariant() Console.WriteLine("Error: Dafny prelude is missing declaration of type Field");
} else if (classNameType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type ClassName");
- } else if (fieldCategoryType == null) {
- Console.WriteLine("Error: Dafny prelude is missing declaration of type FieldCategory");
} else if (datatypeType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type DatatypeType");
} else if (dtCtorId == null) {
@@ -323,7 +314,7 @@ void ObjectInvariant() Console.WriteLine("Error: Dafny prelude is missing declaration of constant #loc.$Heap");
} else {
return new PredefinedDecls(refType, boxType, cevTokenType, cevVariableKind, cevEventType,
- setTypeCtor, seqTypeCtor, fieldNameType, heap, classNameType, fieldCategoryType, datatypeType, dtCtorId,
+ setTypeCtor, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId,
allocField, cevHeapNameConst);
}
return null;
@@ -364,13 +355,19 @@ void ObjectInvariant() public Bpl.Program Translate(Program program) {
Contract.Requires(program != null);
- Contract.Ensures(Contract.Result<Bpl.Program>() != null);
+ Contract.Ensures(Contract.Result<Bpl.Program>() != null);
if (sink == null || predef == null) {
// something went wrong during construction, which reads the prelude; an error has
// already been printed, so just return an empty program here (which is non-null)
return new Bpl.Program();
}
+
+ // add the array classes used in this program
+ foreach (ClassDecl arrayDecl in UserDefinedType.ArrayTypeDecls.Values) {
+ AddClassMembers(arrayDecl);
+ }
+
foreach (ModuleDecl m in program.Modules) {
foreach (TopLevelDecl d in m.TopLevelDecls) {
if (d is DatatypeDecl) {
@@ -478,13 +475,10 @@ void ObjectInvariant() void CreateBoundVariables(List<Formal/*!*/>/*!*/ formals, out Bpl.VariableSeq/*!*/ bvs, out List<Bpl.Expr/*!*/>/*!*/ args)
{
Contract.Requires(formals != null);
-
-
Contract.Ensures( Contract.ValueAtReturn(out bvs).Length == Contract.ValueAtReturn(out args).Count);
Contract.Ensures(Contract.ValueAtReturn(out bvs) != null);
Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out args)));
-
bvs = new Bpl.VariableSeq();
args = new List<Bpl.Expr>();
foreach (Formal arg in formals) {
@@ -498,7 +492,6 @@ void ObjectInvariant() void AddClassMembers(ClassDecl c)
{
Contract.Requires( sink != null && predef != null);
-
Contract.Requires(c != null);
sink.TopLevelDeclarations.Add(GetClass(c));
@@ -800,7 +793,9 @@ void ObjectInvariant() lowerBound = Bpl.Expr.Literal(0);
}
Bpl.Expr lower = Bpl.Expr.Le(lowerBound, index);
- Bpl.Expr length = FunctionCall(tok, isSequence ? BuiltinFunction.SeqLength : BuiltinFunction.ArrayLength, null, seq);
+ Bpl.Expr length = isSequence ?
+ FunctionCall(tok, BuiltinFunction.SeqLength, null, seq) :
+ FunctionCall(tok, BuiltinFunction.ArrayLength, null, seq, Bpl.Expr.Literal(0));
Bpl.Expr upper;
if (includeUpperBound) {
upper = Bpl.Expr.Le(index, length);
@@ -1296,6 +1291,22 @@ void ObjectInvariant() total = BplAnd(total, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true));
}
return total;
+ } else if (expr is MultiSelectExpr) {
+ MultiSelectExpr e = (MultiSelectExpr)expr;
+ Bpl.Expr total = IsTotal(e.Array, etran);
+ Bpl.Expr array = etran.TrExpr(e.Array);
+ int i = 0;
+ foreach (Expression idx in e.Indices) {
+ total = BplAnd(total, IsTotal(idx, etran));
+
+ Bpl.Expr index = etran.TrExpr(idx);
+ Bpl.Expr lower = Bpl.Expr.Le(Bpl.Expr.Literal(0), index);
+ Bpl.Expr length = FunctionCall(idx.tok, BuiltinFunction.ArrayLength, null, array, Bpl.Expr.Literal(i));
+ Bpl.Expr upper = Bpl.Expr.Lt(index, length);
+ total = BplAnd(total, Bpl.Expr.And(lower, upper));
+ i++;
+ }
+ return total;
} else if (expr is SeqUpdateExpr) {
SeqUpdateExpr e = (SeqUpdateExpr)expr;
Bpl.Expr total = IsTotal(e.Seq, etran);
@@ -1479,6 +1490,21 @@ void ObjectInvariant() Bpl.Expr fieldName = FunctionCall(expr.tok, BuiltinFunction.IndexField, null, etran.TrExpr(e.E0));
builder.Add(Assert(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), seq, fieldName), "insufficient reads clause to read array element"));
}
+ } else if (expr is MultiSelectExpr) {
+ MultiSelectExpr e = (MultiSelectExpr)expr;
+ CheckWellformed(e.Array, func, Position.Neither, locals, builder, etran);
+ Bpl.Expr array = etran.TrExpr(e.Array);
+ int i = 0;
+ foreach (Expression idx in e.Indices) {
+ CheckWellformed(idx, func, Position.Neither, locals, builder, etran);
+
+ Bpl.Expr index = etran.TrExpr(idx);
+ Bpl.Expr lower = Bpl.Expr.Le(Bpl.Expr.Literal(0), index);
+ Bpl.Expr length = FunctionCall(idx.tok, BuiltinFunction.ArrayLength, null, array, Bpl.Expr.Literal(i));
+ Bpl.Expr upper = Bpl.Expr.Lt(index, length);
+ builder.Add(Assert(idx.tok, Bpl.Expr.And(lower, upper), "index " + i + " out of range"));
+ i++;
+ }
} else if (expr is SeqUpdateExpr) {
SeqUpdateExpr e = (SeqUpdateExpr)expr;
CheckWellformed(e.Seq, func, Position.Neither, locals, builder, etran);
@@ -1767,10 +1793,10 @@ void ObjectInvariant() Bpl.Type ty = predef.FieldName(f.tok, TrType(f.Type));
fc = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, f.FullName, ty), true);
fields.Add(f, fc);
- // axiom FCat(f) == $NamedField && DeclType(f) == C;
- Bpl.Expr fcat = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.FCat, ty, Bpl.Expr.Ident(fc)), new Bpl.IdentifierExpr(f.tok, "$NamedField", predef.FieldCategoryType));
+ // axiom FDim(f) == 0 && DeclType(f) == C;
+ Bpl.Expr fdim = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.FDim, ty, Bpl.Expr.Ident(fc)), Bpl.Expr.Literal(0));
Bpl.Expr declType = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.DeclType, ty, Bpl.Expr.Ident(fc)), new Bpl.IdentifierExpr(f.tok, GetClass(cce.NonNull(f.EnclosingClass))));
- Bpl.Axiom ax = new Bpl.Axiom(f.tok, Bpl.Expr.And(fcat, declType));
+ Bpl.Axiom ax = new Bpl.Axiom(f.tok, Bpl.Expr.And(fdim, declType));
sink.TopLevelDeclarations.Add(ax);
}
return fc;
@@ -2880,7 +2906,7 @@ void ObjectInvariant() // Here comes: assume (forall o: ref :: o != null && o in S && Range(o) ==> $Heap[o,F] = RHS[$Heap := oldHeap]);
if (rhsExpr != null) {
- Bpl.Expr heapOField = ExpressionTranslator.ReadHeap(stmt.Tok, etran.HeapExpr, o, GetField((FieldSelectExpr)(s.BodyAssign).Lhs));
+ Bpl.Expr heapOField = ExpressionTranslator.ReadHeap(stmt.Tok, etran.HeapExpr, o, GetField((FieldSelectExpr)(s.BodyAssign).Lhs));
ExpressionTranslator oldEtran = new ExpressionTranslator(this, predef, prevHeap);
body = Bpl.Expr.Imp(oInS, Bpl.Expr.Eq(heapOField, oldEtran.TrExpr(rhsExpr.Expr)));
qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);
@@ -3311,7 +3337,7 @@ void ObjectInvariant() builder.Add(AssumeGoodHeap(tok, etran));
} else {
Bpl.Expr low = sel.E0 == null ? Bpl.Expr.Literal(0) : etran.TrExpr(sel.E0);
- Bpl.Expr high = sel.E1 == null ? FunctionCall(tok, BuiltinFunction.ArrayLength, null, etran.TrExpr(sel.Seq)) : etran.TrExpr(sel.E1);
+ Bpl.Expr high = sel.E1 == null ? FunctionCall(tok, BuiltinFunction.ArrayLength, null, etran.TrExpr(sel.Seq), Bpl.Expr.Literal(0)) : etran.TrExpr(sel.E1);
// check frame:
// assert (forall i: int :: low <= i && i < high ==> $_Frame[arr,i]);
Bpl.Variable iVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$i", Bpl.Type.Int));
@@ -3337,10 +3363,17 @@ void ObjectInvariant() Contract.Assert( rhs is TypeRhs); // otherwise, an unexpected AssignmentRhs
TypeRhs tRhs = (TypeRhs)rhs;
Contract.Assert( lhs is IdentifierExpr); // for this kind of RHS, the LHS is restricted to be a simple variable
-
- if (tRhs.ArraySize != null) {
- CheckWellformed(tRhs.ArraySize, null, Position.Positive, locals, builder, etran);
- builder.Add(Assert(tok, Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(tRhs.ArraySize)), "array size might be negative"));
+
+ if (tRhs.ArrayDimensions != null) {
+ int i = 0;
+ foreach (Expression dim in tRhs.ArrayDimensions) {
+ CheckWellformed(dim, null, Position.Positive, locals, builder, etran);
+ if (tRhs.ArrayDimensions.Count == 1) {
+ builder.Add(Assert(tok, Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(dim)),
+ tRhs.ArrayDimensions.Count == 1 ? "array size might be negative" : string.Format("array size (dimension {0}) might be negative", i)));
+ }
+ i++;
+ }
}
Bpl.IdentifierExpr nw = GetNewVar_IdExpr(tok, locals);
@@ -3348,21 +3381,25 @@ void ObjectInvariant() // assume $nw != null && !$Heap[$nw, alloc] && dtype($nw) == RHS;
Bpl.Expr nwNotNull = Bpl.Expr.Neq(nw, predef.Null);
Bpl.Expr rightType;
- if (tRhs.ArraySize != null) {
+ if (tRhs.ArrayDimensions != null) {
// array allocation
List<Type> typeArgs = new List<Type>();
typeArgs.Add(tRhs.EType);
- rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(tok, "class.array", predef.ClassNameType), typeArgs, true);
+ rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(tok, "class.array" + tRhs.ArrayDimensions.Count, predef.ClassNameType), typeArgs, true);
} else if (tRhs.EType is ObjectType) {
rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(tok, "class.object", predef.ClassNameType), new List<Type>(), true);
} else {
rightType = etran.GoodRef_Class(tok, nw, (UserDefinedType)tRhs.EType, true);
}
builder.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.And(nwNotNull, rightType)));
- if (tRhs.ArraySize != null) {
- // assume Array#Length($nw) == arraySize;
- Bpl.Expr arrayLength = FunctionCall(tok, BuiltinFunction.ArrayLength, null, nw);
- builder.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.Eq(arrayLength, etran.TrExpr(tRhs.ArraySize))));
+ if (tRhs.ArrayDimensions != null) {
+ int i = 0;
+ foreach (Expression dim in tRhs.ArrayDimensions) {
+ // assume Array#Length($nw, i) == arraySize;
+ Bpl.Expr arrayLength = FunctionCall(tok, BuiltinFunction.ArrayLength, null, nw, Bpl.Expr.Literal(i));
+ builder.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.Eq(arrayLength, etran.TrExpr(dim))));
+ i++;
+ }
}
// $Heap[$nw, alloc] := true;
Bpl.Expr alloc = predef.Alloc(tok);
@@ -3587,7 +3624,29 @@ void ObjectInvariant() Bpl.Expr index = TrExpr(e.Index);
Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value), elmtType);
return translator.FunctionCall(expr.tok, BuiltinFunction.SeqUpdate, predef.BoxType, seq, index, val);
-
+
+ } else if (expr is MultiSelectExpr) {
+ MultiSelectExpr e = (MultiSelectExpr)expr;
+ Type elmtType = UserDefinedType.ArrayElementType(e.Array.Type);;
+ Bpl.Type elType = translator.TrType(elmtType);
+
+ Bpl.Expr fieldName = null;
+ foreach (Expression idx in e.Indices) {
+ Bpl.Expr index = TrExpr(idx);
+ if (fieldName == null) {
+ // the index in dimension 0: IndexField(index0)
+ fieldName = translator.FunctionCall(expr.tok, BuiltinFunction.IndexField, null, index);
+ } else {
+ // the index in dimension n: MultiIndexField(...field name for first n indices..., index_n)
+ fieldName = translator.FunctionCall(expr.tok, BuiltinFunction.MultiIndexField, null, fieldName, index);
+ }
+ }
+ Bpl.Expr x = ReadHeap(expr.tok, HeapExpr, TrExpr(e.Array), fieldName);
+ if (!ModeledAsBoxType(elmtType)) {
+ x = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, elType, x);
+ }
+ return x;
+
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
string nm = cce.NonNull(e.Function).FullName;
@@ -3670,7 +3729,7 @@ void ObjectInvariant() if (e.E.Type is SeqType) {
return translator.FunctionCall(expr.tok, BuiltinFunction.SeqLength, null, arg);
} else {
- return translator.FunctionCall(expr.tok, BuiltinFunction.ArrayLength, null, arg);
+ return translator.FunctionCall(expr.tok, BuiltinFunction.ArrayLength, null, arg, Bpl.Expr.Literal(0));
}
default:
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary expression
@@ -3938,41 +3997,39 @@ Contract.Requires(tok != null); return new Bpl.IdentifierExpr(tok, var.UniqueName, translator.TrType(var.Type));
}
- public static Bpl.NAryExpr ReadHeap(IToken tok, Expr heap, Expr r, Expr f)
- {
- Contract.Requires(tok != null);
- Contract.Requires(heap != null);
- Contract.Requires(r != null);
- Contract.Requires(f != null);
- Contract.Ensures(Contract.Result<Bpl.NAryExpr>() != null);
+ public static Bpl.NAryExpr ReadHeap(IToken tok, Expr heap, Expr r, Expr f) {
+ Contract.Requires(tok != null);
+ Contract.Requires(heap != null);
+ Contract.Requires(r != null);
+ Contract.Requires(f != null);
+ Contract.Ensures(Contract.Result<Bpl.NAryExpr>() != null);
- Bpl.ExprSeq args = new Bpl.ExprSeq();
- args.Add(heap);
- args.Add(r);
- args.Add(f);
- Bpl.Type t = (f.Type != null) ? f.Type : f.ShallowType;
- return new Bpl.NAryExpr(tok,
- new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, "read", t.AsCtor.Arguments[0])),
- args);
+ Bpl.ExprSeq args = new Bpl.ExprSeq();
+ args.Add(heap);
+ args.Add(r);
+ args.Add(f);
+ Bpl.Type t = (f.Type != null) ? f.Type : f.ShallowType;
+ return new Bpl.NAryExpr(tok,
+ new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, "read", t.AsCtor.Arguments[0])),
+ args);
}
- public static Bpl.NAryExpr UpdateHeap(IToken tok, Expr heap, Expr r, Expr f, Expr v)
- {
- Contract.Requires(tok != null);
- Contract.Requires(heap != null);
- Contract.Requires(r != null);
- Contract.Requires(f != null);
- Contract.Requires(v != null);
- Contract.Ensures(Contract.Result<Bpl.NAryExpr>() != null);
+ public static Bpl.NAryExpr UpdateHeap(IToken tok, Expr heap, Expr r, Expr f, Expr v) {
+ Contract.Requires(tok != null);
+ Contract.Requires(heap != null);
+ Contract.Requires(r != null);
+ Contract.Requires(f != null);
+ Contract.Requires(v != null);
+ Contract.Ensures(Contract.Result<Bpl.NAryExpr>() != null);
- Bpl.ExprSeq args = new Bpl.ExprSeq();
- args.Add(heap);
- args.Add(r);
- args.Add(f);
- args.Add(v);
- return new Bpl.NAryExpr(tok,
- new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, "update", heap.Type)),
- args);
+ Bpl.ExprSeq args = new Bpl.ExprSeq();
+ args.Add(heap);
+ args.Add(r);
+ args.Add(f);
+ args.Add(v);
+ return new Bpl.NAryExpr(tok,
+ new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, "update", heap.Type)),
+ args);
}
/// <summary>
@@ -4183,6 +4240,7 @@ Contract.Requires(tok != null); ArrayLength,
IndexField,
+ MultiIndexField,
IfThenElse,
@@ -4196,7 +4254,7 @@ Contract.Requires(tok != null); TypeParams, // type parameters to allocated type
TypeTuple,
DeclType,
- FCat, // field category (indexed or named)
+ FDim, // field dimension (0 - named, 1 or more - indexed)
DatatypeCtorId,
DtRank,
@@ -4211,155 +4269,159 @@ Contract.Requires(tok != null); // The "typeInstantiation" argument is passed in to help construct the result type of the function.
Bpl.NAryExpr FunctionCall(IToken tok, BuiltinFunction f, Bpl.Type typeInstantiation, params Bpl.Expr[] args)
- {
+ {
Contract.Requires(tok != null);
Contract.Requires(args != null);
- Contract.Requires( predef != null);
- Contract.Ensures(Contract.Result<Bpl.NAryExpr>() != null);
+ Contract.Requires(predef != null);
+ Contract.Ensures(Contract.Result<Bpl.NAryExpr>() != null);
switch (f) {
case BuiltinFunction.SetEmpty: {
- Contract.Assert( args.Length == 0);
- Contract.Assert( typeInstantiation != null);
+ Contract.Assert(args.Length == 0);
+ Contract.Assert(typeInstantiation != null);
Bpl.Type resultType = predef.SetType(tok, typeInstantiation);
return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "Set#Empty", resultType, args), resultType);
}
case BuiltinFunction.SetUnionOne:
- Contract.Assert( args.Length == 2);
- Contract.Assert( typeInstantiation != null);
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Set#UnionOne", predef.SetType(tok, typeInstantiation), args);
case BuiltinFunction.SetUnion:
- Contract.Assert( args.Length == 2);
- Contract.Assert( typeInstantiation != null);
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Set#Union", predef.SetType(tok, typeInstantiation), args);
case BuiltinFunction.SetIntersection:
- Contract.Assert( args.Length == 2);
- Contract.Assert( typeInstantiation != null);
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Set#Intersection", predef.SetType(tok, typeInstantiation), args);
case BuiltinFunction.SetDifference:
- Contract.Assert( args.Length == 2);
- Contract.Assert( typeInstantiation != null);
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Set#Difference", predef.SetType(tok, typeInstantiation), args);
case BuiltinFunction.SetEqual:
- Contract.Assert( args.Length == 2);
- Contract.Assert( typeInstantiation == null);
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "Set#Equal", Bpl.Type.Bool, args);
case BuiltinFunction.SetSubset:
- Contract.Assert( args.Length == 2);
- Contract.Assert( typeInstantiation == null);
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "Set#Subset", Bpl.Type.Bool, args);
case BuiltinFunction.SetDisjoint:
- Contract.Assert( args.Length == 2);
- Contract.Assert( typeInstantiation == null);
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "Set#Disjoint", Bpl.Type.Bool, args);
case BuiltinFunction.SeqLength:
- Contract.Assert( args.Length == 1);
- Contract.Assert( typeInstantiation == null);
+ Contract.Assert(args.Length == 1);
+ Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "Seq#Length", Bpl.Type.Int, args);
case BuiltinFunction.SeqEmpty: {
- Contract.Assert( args.Length == 0);
- Contract.Assert( typeInstantiation != null);
+ Contract.Assert(args.Length == 0);
+ Contract.Assert(typeInstantiation != null);
Bpl.Type resultType = predef.SeqType(tok, typeInstantiation);
return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "Seq#Empty", resultType, args), resultType);
}
case BuiltinFunction.SeqBuild:
- Contract.Assert( args.Length == 4);
- Contract.Assert( typeInstantiation != null);
+ Contract.Assert(args.Length == 4);
+ Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Seq#Build", predef.SeqType(tok, typeInstantiation), args);
case BuiltinFunction.SeqAppend:
- Contract.Assert( args.Length == 2);
- Contract.Assert( typeInstantiation != null);
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Seq#Append", predef.SeqType(tok, typeInstantiation), args);
case BuiltinFunction.SeqIndex:
- Contract.Assert( args.Length == 2);
- Contract.Assert( typeInstantiation != null);
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Seq#Index", typeInstantiation, args);
case BuiltinFunction.SeqUpdate:
- Contract.Assert( args.Length == 3);
- Contract.Assert( typeInstantiation != null);
+ Contract.Assert(args.Length == 3);
+ Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Seq#Update", predef.SeqType(tok, typeInstantiation), args);
case BuiltinFunction.SeqContains:
- Contract.Assert( args.Length == 2);
- Contract.Assert( typeInstantiation == null);
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "Seq#Contains", Bpl.Type.Bool, args);
case BuiltinFunction.SeqDrop:
- Contract.Assert( args.Length == 2);
- Contract.Assert( typeInstantiation != null);
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Seq#Drop", predef.SeqType(tok, typeInstantiation), args);
case BuiltinFunction.SeqTake:
- Contract.Assert( args.Length == 2);
- Contract.Assert( typeInstantiation != null);
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Seq#Take", predef.SeqType(tok, typeInstantiation), args);
case BuiltinFunction.SeqEqual:
- Contract.Assert( args.Length == 2);
- Contract.Assert( typeInstantiation == null);
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "Seq#Equal", Bpl.Type.Bool, args);
case BuiltinFunction.SeqSameUntil:
- Contract.Assert( args.Length == 3);
- Contract.Assert( typeInstantiation == null);
+ Contract.Assert(args.Length == 3);
+ Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "Seq#SameUntil", Bpl.Type.Bool, args);
case BuiltinFunction.ArrayLength:
- Contract.Assert( args.Length == 1);
- Contract.Assert( typeInstantiation == null);
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "Array#Length", Bpl.Type.Int, args);
case BuiltinFunction.IndexField:
- Contract.Assert( args.Length == 1);
- Contract.Assert( typeInstantiation == null);
+ Contract.Assert(args.Length == 1);
+ Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "IndexField", predef.FieldName(tok, predef.BoxType), args);
+ case BuiltinFunction.MultiIndexField:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation == null);
+ return FunctionCall(tok, "MultiIndexField", predef.FieldName(tok, predef.BoxType), args);
case BuiltinFunction.IfThenElse:
- Contract.Assert( args.Length == 3);
- Contract.Assert( typeInstantiation != null);
+ Contract.Assert(args.Length == 3);
+ Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "$ite", typeInstantiation, args);
case BuiltinFunction.Box:
- Contract.Assert( args.Length == 1);
- Contract.Assert( typeInstantiation == null);
+ Contract.Assert(args.Length == 1);
+ Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "$Box", predef.BoxType, args);
case BuiltinFunction.Unbox:
- Contract.Assert( args.Length == 1);
- Contract.Assert( typeInstantiation != null);
+ Contract.Assert(args.Length == 1);
+ Contract.Assert(typeInstantiation != null);
return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "$Unbox", typeInstantiation, args), typeInstantiation);
case BuiltinFunction.IsGoodHeap:
- Contract.Assert( args.Length == 1);
- Contract.Assert( typeInstantiation == null);
+ Contract.Assert(args.Length == 1);
+ Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "$IsGoodHeap", Bpl.Type.Bool, args);
case BuiltinFunction.HeapSucc:
- Contract.Assert( args.Length == 2);
- Contract.Assert( typeInstantiation == null);
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "$HeapSucc", Bpl.Type.Bool, args);
case BuiltinFunction.DynamicType:
- Contract.Assert( args.Length == 1);
- Contract.Assert( typeInstantiation == null);
+ Contract.Assert(args.Length == 1);
+ Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "dtype", predef.ClassNameType, args);
case BuiltinFunction.TypeParams:
- Contract.Assert( args.Length == 2);
- Contract.Assert( typeInstantiation == null);
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "TypeParams", predef.ClassNameType, args);
case BuiltinFunction.TypeTuple:
- Contract.Assert( args.Length == 2);
- Contract.Assert( typeInstantiation == null);
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "TypeTuple", predef.ClassNameType, args);
case BuiltinFunction.DeclType:
- Contract.Assert( args.Length == 1);
- Contract.Assert( typeInstantiation != null);
+ Contract.Assert(args.Length == 1);
+ Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "DeclType", predef.ClassNameType, args);
- case BuiltinFunction.FCat:
- Contract.Assert( args.Length == 1);
- Contract.Assert( typeInstantiation != null);
- return FunctionCall(tok, "FCat", predef.FieldCategoryType, args);
+ case BuiltinFunction.FDim:
+ Contract.Assert(args.Length == 1);
+ Contract.Assert(typeInstantiation != null);
+ return FunctionCall(tok, "FDim", Bpl.Type.Int, args);
case BuiltinFunction.DatatypeCtorId:
- Contract.Assert( args.Length == 1);
- Contract.Assert( typeInstantiation == null);
+ Contract.Assert(args.Length == 1);
+ Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "DatatypeCtorId", predef.DtCtorId, args);
case BuiltinFunction.DtRank:
- Contract.Assert( args.Length == 1);
- Contract.Assert( typeInstantiation == null);
+ Contract.Assert(args.Length == 1);
+ Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "DtRank", Bpl.Type.Int, args);
case BuiltinFunction.CevInit:
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 18f8b1c5..48c85d27 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -664,7 +664,7 @@ void ObjectInvariant() else if (error is ReturnCounterexample)
{
ReturnCounterexample err = (ReturnCounterexample) error;
- ReportBplError(err.FailingReturn, "Error BP5003: A postcondition might not hold at this return statement.", true);
+ ReportBplError(err.FailingReturn, "Error BP5003: A postcondition might not hold on this return path.", true);
ReportBplError(err.FailingEnsures, "Related location: This is the postcondition that might not hold.", false);
if (CommandLineOptions.Clo.XmlSink != null) {
CommandLineOptions.Clo.XmlSink.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, error.Trace);
diff --git a/Test/codeexpr/Answer b/Test/codeexpr/Answer index 55709034..9c22ca61 100644 --- a/Test/codeexpr/Answer +++ b/Test/codeexpr/Answer @@ -13,7 +13,7 @@ Execution trace: Boogie program verifier finished with 3 verified, 3 errors
------------------------------ CodeExpr1.bpl ---------------------
-CodeExpr1.bpl(44,5): Error BP5003: A postcondition might not hold at this return statement.
+CodeExpr1.bpl(44,5): Error BP5003: A postcondition might not hold on this return path.
CodeExpr1.bpl(40,3): Related location: This is the postcondition that might not hold.
Execution trace:
CodeExpr1.bpl(42,3): start
diff --git a/Test/inline/Answer b/Test/inline/Answer index 12cb5960..0820093a 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -1,8 +1,8 @@ -------------------- test0.bpl --------------------
test0.bpl(30,5): Error BP5001: This assertion might not hold.
Execution trace:
- test0.bpl(26,3): anon0
- test0.bpl(30,5): anon3_Then
+ test0.bpl(26,3): anon0
+ test0.bpl(30,5): anon3_Then
Boogie program verifier finished with 1 verified, 1 error
-------------------- test1.bpl --------------------
@@ -819,44 +819,44 @@ implementation find(A: [int]int, size: int, x: int) returns (ret: int, found: bo }
-<console>(68,4): Error BP5003: A postcondition might not hold at this return statement.
+<console>(68,4): Error BP5003: A postcondition might not hold on this return path.
<console>(78,2): Related location: This is the postcondition that might not hold.
Execution trace:
- <console>(19,0): anon0
- <console>(28,0): inline$find$0$anon0
- <console>(38,0): inline$find$0$anon4_LoopBody
- <console>(42,0): inline$check$0$Entry
- <console>(57,0): inline$check$0$anon4_Else
- <console>(62,0): inline$check$0$anon3
- <console>(65,0): inline$check$0$Return
+ <console>(19,0): anon0
+ <console>(28,0): inline$find$0$anon0
+ <console>(38,0): inline$find$0$anon4_LoopBody
+ <console>(42,0): inline$check$0$Entry
+ <console>(57,0): inline$check$0$anon4_Else
+ <console>(62,0): inline$check$0$anon3
+ <console>(65,0): inline$check$0$Return
<console>(100,4): Error BP5001: This assertion might not hold.
Execution trace:
- <console>(19,0): anon0
- <console>(28,0): inline$find$0$anon0
- <console>(38,0): inline$find$0$anon4_LoopBody
- <console>(42,0): inline$check$0$Entry
- <console>(52,0): inline$check$0$anon4_Then
- <console>(65,0): inline$check$0$Return
- <console>(73,0): inline$find$0$anon5_Then
- <console>(87,0): inline$find$0$anon3
- <console>(90,0): inline$find$0$Return
- <console>(95,0): anon0$1
- <console>(98,0): anon3_Then
-<console>(50,4): Error BP5003: A postcondition might not hold at this return statement.
+ <console>(19,0): anon0
+ <console>(28,0): inline$find$0$anon0
+ <console>(38,0): inline$find$0$anon4_LoopBody
+ <console>(42,0): inline$check$0$Entry
+ <console>(52,0): inline$check$0$anon4_Then
+ <console>(65,0): inline$check$0$Return
+ <console>(73,0): inline$find$0$anon5_Then
+ <console>(87,0): inline$find$0$anon3
+ <console>(90,0): inline$find$0$Return
+ <console>(95,0): anon0$1
+ <console>(98,0): anon3_Then
+<console>(50,4): Error BP5003: A postcondition might not hold on this return path.
<console>(78,2): Related location: This is the postcondition that might not hold.
Execution trace:
- <console>(10,0): anon0
- <console>(20,0): anon4_LoopBody
- <console>(24,0): inline$check$0$Entry
- <console>(39,0): inline$check$0$anon4_Else
- <console>(44,0): inline$check$0$anon3
- <console>(47,0): inline$check$0$Return
-<console>(99,0): Error BP5003: A postcondition might not hold at this return statement.
+ <console>(10,0): anon0
+ <console>(20,0): anon4_LoopBody
+ <console>(24,0): inline$check$0$Entry
+ <console>(39,0): inline$check$0$anon4_Else
+ <console>(44,0): inline$check$0$anon3
+ <console>(47,0): inline$check$0$Return
+<console>(99,0): Error BP5003: A postcondition might not hold on this return path.
<console>(78,2): Related location: This is the postcondition that might not hold.
Execution trace:
- <console>(85,0): anon0
- <console>(93,0): anon4_Else
- <console>(98,0): anon3
+ <console>(85,0): anon0
+ <console>(93,0): anon4_Else
+ <console>(98,0): anon3
Boogie program verifier finished with 0 verified, 4 errors
-------------------- test6.bpl --------------------
@@ -1442,10 +1442,10 @@ Boogie program verifier finished with 5 verified, 0 errors -------------------- test5.bpl --------------------
test5.bpl(37,3): Error BP5001: This assertion might not hold.
Execution trace:
- test5.bpl(34,10): anon0
- test5.bpl(28,10): inline$P$0$anon0
- test5.bpl(28,10): inline$P$1$anon0
- test5.bpl(34,10): anon0$2
+ test5.bpl(34,10): anon0
+ test5.bpl(28,10): inline$P$0$anon0
+ test5.bpl(28,10): inline$P$1$anon0
+ test5.bpl(34,10): anon0$2
Boogie program verifier finished with 4 verified, 1 error
-------------------- expansion.bpl --------------------
@@ -1465,37 +1465,37 @@ expansion.bpl(33,22): Error: expansion: an identifier was used more than once *** more than one possible expansion for x1
expansion3.bpl(18,3): Error BP5001: This assertion might not hold.
Execution trace:
- expansion3.bpl(18,3): anon0
+ expansion3.bpl(18,3): anon0
Boogie program verifier finished with 1 verified, 1 error
-------------------- Elevator.bpl --------------------
Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
- Elevator.bpl(15,3): anon0
- Elevator.bpl(15,3): anon0$1
- Elevator.bpl(16,3): anon10_LoopHead
- Elevator.bpl(19,5): anon10_LoopBody
- Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0
- Elevator.bpl(24,7): anon13_Then$1
+ Elevator.bpl(15,3): anon0
+ Elevator.bpl(15,3): anon0$1
+ Elevator.bpl(16,3): anon10_LoopHead
+ Elevator.bpl(19,5): anon10_LoopBody
+ Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0
+ Elevator.bpl(24,7): anon13_Then$1
Boogie program verifier finished with 1 verified, 1 error
-------------------- Elevator.bpl with empty blocks --------------------
Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
- Elevator.bpl(15,3): anon0
- Elevator.bpl(68,23): inline$Initialize$0$Entry
- Elevator.bpl(71,13): inline$Initialize$0$anon0
- Elevator.bpl(68,23): inline$Initialize$0$Return
- Elevator.bpl(15,3): anon0$1
- Elevator.bpl(16,3): anon10_LoopHead
- Elevator.bpl(19,5): anon10_LoopBody
- Elevator.bpl(19,5): anon11_Else
- Elevator.bpl(19,5): anon12_Else
- Elevator.bpl(24,7): anon13_Then
- Elevator.bpl(94,23): inline$MoveDown_Error$0$Entry
- Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0
- Elevator.bpl(94,23): inline$MoveDown_Error$0$Return
- Elevator.bpl(24,7): anon13_Then$1
+ Elevator.bpl(15,3): anon0
+ Elevator.bpl(68,23): inline$Initialize$0$Entry
+ Elevator.bpl(71,13): inline$Initialize$0$anon0
+ Elevator.bpl(68,23): inline$Initialize$0$Return
+ Elevator.bpl(15,3): anon0$1
+ Elevator.bpl(16,3): anon10_LoopHead
+ Elevator.bpl(19,5): anon10_LoopBody
+ Elevator.bpl(19,5): anon11_Else
+ Elevator.bpl(19,5): anon12_Else
+ Elevator.bpl(24,7): anon13_Then
+ Elevator.bpl(94,23): inline$MoveDown_Error$0$Entry
+ Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0
+ Elevator.bpl(94,23): inline$MoveDown_Error$0$Return
+ Elevator.bpl(24,7): anon13_Then$1
Boogie program verifier finished with 1 verified, 1 error
-------------------- expansion2.bpl --------------------
@@ -1528,7 +1528,7 @@ axiom (forall x: int :: { foo3(x): bool } foo3(x): bool == (x > 0)); Boogie program verifier finished with 0 verified, 0 errors
fundef2.bpl(6,3): Error BP5001: This assertion might not hold.
Execution trace:
- fundef2.bpl(5,3): anon0
+ fundef2.bpl(5,3): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- polyInline.bpl --------------------
@@ -1537,10 +1537,10 @@ polyInline.bpl(31,9): Warning: type parameter alpha is ambiguous, instantiating polyInline.bpl(35,9): Warning: type parameter alpha is ambiguous, instantiating to int
polyInline.bpl(23,3): Error BP5001: This assertion might not hold.
Execution trace:
- polyInline.bpl(20,3): anon0
+ polyInline.bpl(20,3): anon0
polyInline.bpl(39,3): Error BP5001: This assertion might not hold.
Execution trace:
- polyInline.bpl(27,3): anon0
+ polyInline.bpl(27,3): anon0
Boogie program verifier finished with 0 verified, 2 errors
polyInline.bpl(27,9): Warning: type parameter alpha is ambiguous, instantiating to int
@@ -1548,9 +1548,9 @@ polyInline.bpl(31,9): Warning: type parameter alpha is ambiguous, instantiating polyInline.bpl(35,9): Warning: type parameter alpha is ambiguous, instantiating to int
polyInline.bpl(23,3): Error BP5001: This assertion might not hold.
Execution trace:
- polyInline.bpl(20,3): anon0
+ polyInline.bpl(20,3): anon0
polyInline.bpl(39,3): Error BP5001: This assertion might not hold.
Execution trace:
- polyInline.bpl(27,3): anon0
+ polyInline.bpl(27,3): anon0
Boogie program verifier finished with 0 verified, 2 errors
diff --git a/Test/lazyinline/Answer b/Test/lazyinline/Answer index ecb258a2..1feac694 100644 --- a/Test/lazyinline/Answer +++ b/Test/lazyinline/Answer @@ -1,5 +1,5 @@ ----- Running regression test bar1.bpl
-bar1.bpl(25,1): Error BP5003: A postcondition might not hold at this return statement.
+bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path.
bar1.bpl(21,1): Related location: This is the postcondition that might not hold.
Execution trace:
bar1.bpl(24,3): anon0
@@ -31,7 +31,7 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar3.bpl
-bar3.bpl(41,1): Error BP5003: A postcondition might not hold at this return statement.
+bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path.
bar3.bpl(34,1): Related location: This is the postcondition that might not hold.
Execution trace:
bar3.bpl(38,3): anon0
diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer index aa83b37c..290059d6 100644 --- a/Test/stratifiedinline/Answer +++ b/Test/stratifiedinline/Answer @@ -1,5 +1,5 @@ ----- Running regression test bar1.bpl
-bar1.bpl(25,1): Error BP5003: A postcondition might not hold at this return statement.
+bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path.
bar1.bpl(21,1): Related location: This is the postcondition that might not hold.
Execution trace:
bar1.bpl(24,3): anon0
@@ -31,7 +31,7 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar3.bpl
-bar3.bpl(41,1): Error BP5003: A postcondition might not hold at this return statement.
+bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path.
bar3.bpl(34,1): Related location: This is the postcondition that might not hold.
Execution trace:
bar3.bpl(38,3): anon0
diff --git a/Test/test2/Answer b/Test/test2/Answer index 5cea9721..ae27fa94 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -1,6 +1,6 @@ -------------------- FormulaTerm.bpl --------------------
-FormulaTerm.bpl(10,3): Error BP5003: A postcondition might not hold at this return statement.
+FormulaTerm.bpl(10,3): Error BP5003: A postcondition might not hold on this return path.
FormulaTerm.bpl(4,3): Related location: This is the postcondition that might not hold.
Execution trace:
FormulaTerm.bpl(8,1): start
@@ -18,7 +18,7 @@ Execution trace: Boogie program verifier finished with 2 verified, 2 errors
-------------------- Passification.bpl --------------------
-Passification.bpl(44,3): Error BP5003: A postcondition might not hold at this return statement.
+Passification.bpl(44,3): Error BP5003: A postcondition might not hold on this return path.
Passification.bpl(36,3): Related location: This is the postcondition that might not hold.
Execution trace:
Passification.bpl(39,1): A
@@ -44,23 +44,23 @@ Boogie program verifier finished with 7 verified, 4 errors Boogie program verifier finished with 4 verified, 0 errors
-------------------- Ensures.bpl --------------------
-Ensures.bpl(30,5): Error BP5003: A postcondition might not hold at this return statement.
+Ensures.bpl(30,5): Error BP5003: A postcondition might not hold on this return path.
Ensures.bpl(19,3): Related location: This is the postcondition that might not hold.
Execution trace:
Ensures.bpl(28,3): start
-Ensures.bpl(35,5): Error BP5003: A postcondition might not hold at this return statement.
+Ensures.bpl(35,5): Error BP5003: A postcondition might not hold on this return path.
Ensures.bpl(19,3): Related location: This is the postcondition that might not hold.
Execution trace:
Ensures.bpl(34,3): start
-Ensures.bpl(41,5): Error BP5003: A postcondition might not hold at this return statement.
+Ensures.bpl(41,5): Error BP5003: A postcondition might not hold on this return path.
Ensures.bpl(19,3): Related location: This is the postcondition that might not hold.
Execution trace:
Ensures.bpl(39,3): start
-Ensures.bpl(47,5): Error BP5003: A postcondition might not hold at this return statement.
+Ensures.bpl(47,5): Error BP5003: A postcondition might not hold on this return path.
Ensures.bpl(19,3): Related location: This is the postcondition that might not hold.
Execution trace:
Ensures.bpl(45,3): start
-Ensures.bpl(72,5): Error BP5003: A postcondition might not hold at this return statement.
+Ensures.bpl(72,5): Error BP5003: A postcondition might not hold on this return path.
Ensures.bpl(19,3): Related location: This is the postcondition that might not hold.
Execution trace:
Ensures.bpl(70,3): start
@@ -68,7 +68,7 @@ Execution trace: Boogie program verifier finished with 5 verified, 5 errors
-------------------- Old.bpl --------------------
-Old.bpl(29,5): Error BP5003: A postcondition might not hold at this return statement.
+Old.bpl(29,5): Error BP5003: A postcondition might not hold on this return path.
Old.bpl(26,3): Related location: This is the postcondition that might not hold.
Execution trace:
Old.bpl(28,3): start
@@ -81,11 +81,11 @@ OldIllegal.bpl(14,23): Error: old expressions allowed only in two-state contexts 2 name resolution errors detected in OldIllegal.bpl
-------------------- Arrays.bpl --------------------
-Arrays.bpl(46,5): Error BP5003: A postcondition might not hold at this return statement.
+Arrays.bpl(46,5): Error BP5003: A postcondition might not hold on this return path.
Arrays.bpl(38,3): Related location: This is the postcondition that might not hold.
Execution trace:
Arrays.bpl(42,3): start
-Arrays.bpl(127,5): Error BP5003: A postcondition might not hold at this return statement.
+Arrays.bpl(127,5): Error BP5003: A postcondition might not hold on this return path.
Arrays.bpl(119,3): Related location: This is the postcondition that might not hold.
Execution trace:
Arrays.bpl(123,3): start
@@ -128,7 +128,7 @@ Execution trace: Call.bpl(46,5): Error BP5001: This assertion might not hold.
Execution trace:
Call.bpl(45,3): start
-Call.bpl(55,5): Error BP5003: A postcondition might not hold at this return statement.
+Call.bpl(55,5): Error BP5003: A postcondition might not hold on this return path.
Call.bpl(20,3): Related location: This is the postcondition that might not hold.
Execution trace:
Call.bpl(53,3): start
@@ -211,7 +211,7 @@ strings-where.bpl(990,36): Error: invalid argument types (any and name) to binar 18 type checking errors detected in strings-where.bpl
-------------------- Structured.bpl --------------------
-Structured.bpl(252,14): Error BP5003: A postcondition might not hold at this return statement.
+Structured.bpl(252,14): Error BP5003: A postcondition might not hold on this return path.
Structured.bpl(243,3): Related location: This is the postcondition that might not hold.
Execution trace:
Structured.bpl(244,5): anon0
@@ -382,11 +382,11 @@ Execution trace: Boogie program verifier finished with 1 verified, 3 errors
-------------------- Arrays.bpl /typeEncoding:m --------------------
-Arrays.bpl(46,5): Error BP5003: A postcondition might not hold at this return statement.
+Arrays.bpl(46,5): Error BP5003: A postcondition might not hold on this return path.
Arrays.bpl(38,3): Related location: This is the postcondition that might not hold.
Execution trace:
Arrays.bpl(42,3): start
-Arrays.bpl(127,5): Error BP5003: A postcondition might not hold at this return statement.
+Arrays.bpl(127,5): Error BP5003: A postcondition might not hold on this return path.
Arrays.bpl(119,3): Related location: This is the postcondition that might not hold.
Execution trace:
Arrays.bpl(123,3): start
@@ -442,7 +442,7 @@ Execution trace: Boogie program verifier finished with 10 verified, 8 errors
-------------------- ContractEvaluationOrder.bpl --------------------
-ContractEvaluationOrder.bpl(8,1): Error BP5003: A postcondition might not hold at this return statement.
+ContractEvaluationOrder.bpl(8,1): Error BP5003: A postcondition might not hold on this return path.
ContractEvaluationOrder.bpl(3,3): Related location: This is the postcondition that might not hold.
Execution trace:
ContractEvaluationOrder.bpl(7,5): anon0
|