summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Dafny.atg2
-rw-r--r--Source/Dafny/Parser.cs51
-rw-r--r--Source/Dafny/Resolver.cs4
-rw-r--r--Source/Dafny/Scanner.cs102
-rw-r--r--Test/dafny0/Answer5
-rw-r--r--Test/dafny0/ResolutionErrors.dfy8
6 files changed, 90 insertions, 82 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 23582495..8e999553 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1312,6 +1312,8 @@ SelectOrCallSuffix<ref Expression/*!*/ e>
)
(. if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
+ // make sure an array class with this dimensionality exists
+ UserDefinedType tmp = theBuiltIns.ArrayType(multipleIndices.Count, new IntType(), true);
} else {
if (!anyDots && e0 == null) {
/* a parsing error occurred */
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 180f15ab..db33283b 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -25,7 +25,7 @@ public class Parser {
const bool T = true;
const bool x = false;
const int minErrDist = 2;
-
+
public Scanner/*!*/ scanner;
public Errors/*!*/ errors;
@@ -161,10 +161,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
if (errDist >= minErrDist) errors.SemErr(t, msg);
errDist = 0;
}
-
- public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
- Contract.Requires(tok != null);
- Contract.Requires(msg != null);
+
+ public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
+ Contract.Requires(tok != null);
+ Contract.Requires(msg != null);
errors.SemErr(tok, msg);
}
@@ -177,15 +177,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
la = t;
}
}
-
+
void Expect (int n) {
if (la.kind==n) Get(); else { SynErr(n); }
}
-
+
bool StartOf (int s) {
return set[s, la.kind];
}
-
+
void ExpectWeak (int n, int follow) {
if (la.kind == n) Get();
else {
@@ -209,7 +209,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
}
}
-
+
void Dafny() {
ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
Attributes attrs; IToken/*!*/ id; List<string/*!*/> theImports;
@@ -2047,6 +2047,8 @@ List<Expression/*!*/>/*!*/ decreases) {
} else SynErr(144);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
+ // make sure an array class with this dimensionality exists
+ UserDefinedType tmp = theBuiltIns.ArrayType(multipleIndices.Count, new IntType(), true);
} else {
if (!anyDots && e0 == null) {
/* a parsing error occurred */
@@ -2131,13 +2133,13 @@ List<Expression/*!*/>/*!*/ decreases) {
public void Parse() {
la = new Token();
- la.val = "";
+ la.val = "";
Get();
Dafny();
- Expect(0);
+ Expect(0);
}
-
+
static readonly bool[,]/*!*/ set = {
{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
{x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
@@ -2164,20 +2166,18 @@ List<Expression/*!*/>/*!*/ decreases) {
public class Errors {
public int count = 0; // number of errors detected
public System.IO.TextWriter/*!*/ errorStream = Console.Out; // error messages go to this stream
- public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
- public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
-
+ public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
+ public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
+
public void SynErr(string filename, int line, int col, int n) {
- SynErr(filename, line, col, GetSyntaxErrorString(n));
- }
-
- public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {
- Contract.Requires(msg != null);
+ SynErr(filename, line, col, GetSyntaxErrorString(n));
+ }
+ public virtual void SynErr(string filename, int line, int col, string msg) {
+ Contract.Requires(msg != null);
errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
count++;
- }
-
- string GetSyntaxErrorString(int n) {
+ }
+ string GetSyntaxErrorString(int n) {
string s;
switch (n) {
case 0: s = "EOF expected"; break;
@@ -2333,7 +2333,7 @@ public class Errors {
default: s = "error " + n; break;
}
- return s;
+ return s;
}
public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors
@@ -2341,9 +2341,8 @@ public class Errors {
Contract.Requires(msg != null);
SemErr(tok.filename, tok.line, tok.col, msg);
}
-
public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {
- Contract.Requires(msg != null);
+ Contract.Requires(msg != null);
errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
count++;
}
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 972c82ab..00cabd1d 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -960,7 +960,7 @@ namespace Microsoft.Dafny {
if (!UnifyTypes(iProxy.Arg, ((SeqType)t).Arg)) {
return false;
}
- } else if (t.IsArrayType) {
+ } else if (t.IsArrayType && (t.AsArrayType).Dims == 1) {
Type elType = UserDefinedType.ArrayElementType(t);
if (!UnifyTypes(iProxy.Arg, elType)) {
return false;
@@ -1909,7 +1909,7 @@ namespace Microsoft.Dafny {
Contract.Assert(e.Array.Type != null); // follows from postcondition of ResolveExpression
Type elementType = new InferredTypeProxy();
if (!UnifyTypes(e.Array.Type, builtIns.ArrayType(e.Indices.Count, elementType))) {
- Error(e.Array, "array selection requires an array (got {0})", e.Array.Type);
+ Error(e.Array, "array selection requires an array{0} (got {1})", e.Indices.Count, e.Array.Type);
}
int i = 0;
foreach (Expression idx in e.Indices) {
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 817df6cd..0af254f3 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -19,7 +19,7 @@ public class Buffer {
// a) whole stream in buffer
// b) part of stream in buffer
// 2) non seekable stream (network, console)
-
+
public const int EOF = 65535 + 1; // char.MaxValue + 1;
const int MIN_BUFFER_LENGTH = 1024; // 1KB
const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB
@@ -31,17 +31,15 @@ public class Buffer {
Stream/*!*/ stream; // input stream (seekable)
bool isUserStream; // was the stream opened by the user?
- [ContractInvariantMethod]
- void ObjectInvariant(){
- Contract.Invariant(buf != null);
- Contract.Invariant(stream != null);
- }
-
-// [NotDelayed]
- public Buffer (Stream/*!*/ s, bool isUserStream) : base() {
+[ContractInvariantMethod]
+void ObjectInvariant(){
+ Contract.Invariant(buf != null);
+ Contract.Invariant(stream != null);}
+ [NotDelayed]
+ public Buffer (Stream/*!*/ s, bool isUserStream) :base() {
Contract.Requires(s != null);
stream = s; this.isUserStream = isUserStream;
-
+
int fl, bl;
if (s.CanSeek) {
fl = (int) s.Length;
@@ -53,12 +51,12 @@ public class Buffer {
buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];
fileLen = fl; bufLen = bl;
-
+
if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)
else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid
if (bufLen == fileLen && s.CanSeek) Close();
}
-
+
protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor
Contract.Requires(b != null);
buf = b.buf;
@@ -75,14 +73,14 @@ public class Buffer {
}
~Buffer() { Close(); }
-
+
protected void Close() {
if (!isUserStream && stream != null) {
stream.Close();
//stream = null;
}
}
-
+
public virtual int Read () {
if (bufPos < bufLen) {
return buf[bufPos++];
@@ -102,7 +100,7 @@ public class Buffer {
Pos = curPos;
return ch;
}
-
+
public string/*!*/ GetString (int beg, int end) {
Contract.Ensures(Contract.Result<string>() != null);
int len = 0;
@@ -141,7 +139,7 @@ public class Buffer {
}
}
}
-
+
// Read the next chunk of bytes from the stream, increases the buffer
// if needed and updates the fields fileLen and bufLen.
// Returns the number of bytes read.
@@ -215,20 +213,19 @@ public class Scanner {
const int noSym = 107;
- [ContractInvariantMethod]
- void objectInvariant(){
- Contract.Invariant(buffer!=null);
- Contract.Invariant(t != null);
- Contract.Invariant(start != null);
- Contract.Invariant(tokens != null);
- Contract.Invariant(pt != null);
- Contract.Invariant(tval != null);
- Contract.Invariant(Filename != null);
- Contract.Invariant(errorHandler != null);
- }
-
+[ContractInvariantMethod]
+void objectInvariant(){
+ Contract.Invariant(buffer!=null);
+ Contract.Invariant(t != null);
+ Contract.Invariant(start != null);
+ Contract.Invariant(tokens != null);
+ Contract.Invariant(pt != null);
+ Contract.Invariant(tval != null);
+ Contract.Invariant(Filename != null);
+ Contract.Invariant(errorHandler != null);
+}
public Buffer/*!*/ buffer; // scanner buffer
-
+
Token/*!*/ t; // current token
int ch; // current input character
int pos; // byte position of current character
@@ -239,13 +236,13 @@ public class Scanner {
Token/*!*/ tokens; // list of tokens already peeked (first token is a dummy)
Token/*!*/ pt; // current peek token
-
+
char[]/*!*/ tval = new char[128]; // text of current token
int tlen; // length of current token
-
+
private string/*!*/ Filename;
private Errors/*!*/ errorHandler;
-
+
static Scanner() {
start = new Hashtable(128);
for (int i = 39; i <= 39; ++i) start[i] = 1;
@@ -294,9 +291,9 @@ public class Scanner {
start[Buffer.EOF] = -1;
}
-
-// [NotDelayed]
- public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {
+
+ [NotDelayed]
+ public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){
Contract.Requires(fileName != null);
Contract.Requires(errorHandler != null);
this.errorHandler = errorHandler;
@@ -306,14 +303,15 @@ public class Scanner {
Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);
buffer = new Buffer(stream, false);
Filename = fileName;
+
Init();
} catch (IOException) {
throw new FatalError("Cannot open file " + fileName);
}
}
-
-// [NotDelayed]
- public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {
+
+ [NotDelayed]
+ public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){
Contract.Requires(s != null);
Contract.Requires(errorHandler != null);
Contract.Requires(fileName != null);
@@ -322,9 +320,10 @@ public class Scanner {
buffer = new Buffer(s, true);
this.errorHandler = errorHandler;
this.Filename = fileName;
+
Init();
}
-
+
void Init() {
pos = -1; line = 1; col = 0;
oldEols = 0;
@@ -345,11 +344,11 @@ public class Scanner {
Contract.Ensures(Contract.Result<string>() != null);
int p = buffer.Pos;
int ch = buffer.Read();
- // replace isolated '\r' by '\n' in order to make
+ // replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
while (ch != EOL && ch != Buffer.EOF){
- ch = buffer.Read();
+ ch = buffer.Read();
// replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
@@ -360,7 +359,7 @@ public class Scanner {
}
void NextCh() {
- if (oldEols > 0) { ch = EOL; oldEols--; }
+ if (oldEols > 0) { ch = EOL; oldEols--; }
else {
// pos = buffer.Pos;
// ch = buffer.Read(); col++;
@@ -368,9 +367,9 @@ public class Scanner {
// // eol handling uniform across Windows, Unix and Mac
// if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
// if (ch == EOL) { line++; col = 0; }
-
+
while (true) {
- pos = buffer.Pos;
+ pos = buffer.Pos;
ch = buffer.Read(); col++;
// replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
@@ -420,7 +419,7 @@ public class Scanner {
return;
}
-
+
}
}
@@ -559,13 +558,10 @@ public class Scanner {
t.pos = pos; t.col = col; t.line = line;
t.filename = this.Filename;
int state;
- if (start.ContainsKey(ch)) {
- Contract.Assert(start[ch] != null);
- state = (int) start[ch];
- }
+ if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }
else { state = 0; }
tlen = 0; AddCh();
-
+
switch (state) {
case -1: { t.kind = eofSym; break; } // NextCh already done
case 0: {
@@ -773,14 +769,14 @@ public class Scanner {
t.val = new String(tval, 0, tlen);
return t;
}
-
+
private void SetScannerBehindT() {
buffer.Pos = t.pos;
NextCh();
line = t.line; col = t.col;
for (int i = 0; i < tlen; i++) NextCh();
}
-
+
// get the next token (possibly a token already seen during peeking)
public Token/*!*/ Scan () {
Contract.Ensures(Contract.Result<Token>() != null);
@@ -801,7 +797,7 @@ public class Scanner {
}
pt = pt.next;
} while (pt.kind > maxT); // skip pragmas
-
+
return pt;
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index cd531472..8382a525 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -393,7 +393,10 @@ Dafny program verifier finished with 3 verified, 3 errors
-------------------- ResolutionErrors.dfy --------------------
ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops
-1 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(23,11): Error: array selection requires an array2 (got array3<T>)
+ResolutionErrors.dfy(24,12): Error: sequence/array selection requires a sequence or array (got array3<T>)
+ResolutionErrors.dfy(25,11): Error: array selection requires an array4 (got array<T>)
+4 resolution/type errors detected in ResolutionErrors.dfy
-------------------- Array.dfy --------------------
Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index b105a5c0..77a30102 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -16,3 +16,11 @@ method UmmThisIsntGoingToWork()
assert a[1] == -1; // ...for then this would incorrectly verify
b[a[1]] := 0;
}
+
+method M<T>(a: array3<T>, b: array<T>, m: int, n: int)
+{
+ // the following invalid expressions were once incorrectly resolved:
+ var x := a[m, n]; // error
+ var y := a[m]; // error
+ var z := b[m, n, m, n]; // error
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-31 05:50:11 +0000