diff options
| -rw-r--r-- | Source/Core/Parser.cs | 48 | ||||
| -rw-r--r-- | Source/Core/Scanner.cs | 4 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 19 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 65 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.cs | 4 | ||||
| -rw-r--r-- | Test/dafny1/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny1/Cubes.dfy | 23 | ||||
| -rw-r--r-- | Test/dafny1/runtest.bat | 2 | ||||
| -rw-r--r-- | Test/test0/Answer | 74 | ||||
| -rw-r--r-- | Test/test2/Answer | 222 |
10 files changed, 247 insertions, 218 deletions
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index a2887dcf..9b344a4f 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -2035,13 +2035,16 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { 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 = "-- line {0} col {1}: {2}"; // 0=line, 1=column, 2=text
- public string/*!*/ errMsgFormat4 = "{0}({1},{2}): Error: {3}"; // 0=line, 1=column, 2=text
- public string/*!*/ errMsgFormat = "-- line {0} col {1}: {2}"; // 0=line, 1=column, 2=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) {
+ public virtual void SynErr (string filename, int line, int col, int n) {
+ string s = GetErrorString(n);
+ errorStream.WriteLine(errMsgFormat, filename, line, col, s);
+ count++;
+ }
+ public string GetErrorString(int n) {
string s;
- Console.Write("{0}({1},{2}): syntax error: ", filename, line, col);
switch (n) {
case 0: s = "EOF expected"; break;
case 1: s = "ident expected"; break;
@@ -2175,40 +2178,23 @@ public class Errors { default: s = "error " + n; break;
}
- //errorStream.WriteLine(errMsgFormat, line, col, s);
- errorStream.WriteLine(s);
- count++;
- }
-
- public void SemErr (int line, int col, string/*!*/ s) {
- Contract.Requires(s != null);
- errorStream.WriteLine(errMsgFormat, line, col, s);
- count++;
+ return s;
}
- public void SemErr (string filename, int line, int col, string/*!*/ s) {
+ public virtual void SemErr (string filename, int line, int col, string/*!*/ s) {
Contract.Requires(s != null);
- errorStream.WriteLine(errMsgFormat4, filename, line, col, s);
+ errorStream.WriteLine(errMsgFormat, filename, line, col, s);
count++;
}
- public void SemErr (string s) {
- errorStream.WriteLine(s);
- count++;
+ public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors
+ Contract.Requires(tok != null);
+ Contract.Requires(msg != null);
+ SemErr(tok.filename, tok.line, tok.col, msg);
}
- public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors
- Contract.Requires(tok != null);
- Contract.Requires(msg != null);
- SemErr(tok.filename, tok.line, tok.col, msg);
- }
-
- public void Warning (int line, int col, string s) {
- errorStream.WriteLine(errMsgFormat, line, col, s);
- }
-
- public void Warning(string s) {
- errorStream.WriteLine(s);
+ public virtual void Warning (int line, int col, string s) {
+ errorStream.WriteLine(warningMsgFormat, line, col, s);
}
} // Errors
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs index deb8b809..faab5837 100644 --- a/Source/Core/Scanner.cs +++ b/Source/Core/Scanner.cs @@ -375,7 +375,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;
@@ -536,7 +536,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/Dafny.atg b/Source/Dafny/Dafny.atg index 560c0aea..cfb9be3e 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -96,13 +96,28 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Contract.Requires(s != null);
Contract.Requires(filename != null);
Contract.Requires(cce.NonNullElements(modules));
+ Errors errors = new Errors();
+ return Parse(s, filename, modules, builtIns, errors);
+}
+
+///<summary>
+/// Parses top-level things (modules, classes, datatypes, class members)
+/// and appends them in appropriate form to "modules".
+/// Returns the number of parsing errors encountered.
+/// Note: first initialize the Scanner with the given Errors sink.
+///</summary>
+public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ modules, BuiltIns builtIns,
+ Errors/*!*/ errors) {
+ Contract.Requires(s != null);
+ Contract.Requires(filename != null);
+ Contract.Requires(cce.NonNullElements(modules));
+ Contract.Requires(errors != null);
List<ModuleDecl/*!*/> oldModules = theModules;
theModules = modules;
BuiltIns oldBuiltIns = builtIns;
theBuiltIns = builtIns;
byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));
MemoryStream ms = new MemoryStream(buffer,false);
- Errors errors = new Errors();
Scanner scanner = new Scanner(ms, errors, filename);
Parser parser = new Parser(scanner, errors);
parser.Parse();
@@ -743,7 +758,7 @@ AssignRhs<.out List<Expression> ee, out Type ty.> { "," Expression<out e> (. ee.Add(e); .)
}
"]" (. // make sure an array class with this dimensionality exists
- UserDefinedType tmp = theBuiltIns.ArrayType(ee.Count, Type.Int, true);
+ UserDefinedType tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);
.)
]
| Expression<out e> (. ee = new List<Expression>(); ee.Add(e); .)
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 6577e993..1877fafe 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -109,13 +109,28 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Contract.Requires(s != null);
Contract.Requires(filename != null);
Contract.Requires(cce.NonNullElements(modules));
+ Errors errors = new Errors();
+ return Parse(s, filename, modules, builtIns, errors);
+}
+
+///<summary>
+/// Parses top-level things (modules, classes, datatypes, class members)
+/// and appends them in appropriate form to "modules".
+/// Returns the number of parsing errors encountered.
+/// Note: first initialize the Scanner with the given Errors sink.
+///</summary>
+public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ modules, BuiltIns builtIns,
+ Errors/*!*/ errors) {
+ Contract.Requires(s != null);
+ Contract.Requires(filename != null);
+ Contract.Requires(cce.NonNullElements(modules));
+ Contract.Requires(errors != null);
List<ModuleDecl/*!*/> oldModules = theModules;
theModules = modules;
BuiltIns oldBuiltIns = builtIns;
theBuiltIns = builtIns;
byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));
MemoryStream ms = new MemoryStream(buffer,false);
- Errors errors = new Errors();
Scanner scanner = new Scanner(ms, errors, filename);
Parser parser = new Parser(scanner, errors);
parser.Parse();
@@ -2045,13 +2060,16 @@ 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 = "-- line {0} col {1}: {2}"; // 0=line, 1=column, 2=text
- public string/*!*/ errMsgFormat4 = "{0}({1},{2}): Error: {3}"; // 0=line, 1=column, 2=text
- public string/*!*/ errMsgFormat = "-- line {0} col {1}: {2}"; // 0=line, 1=column, 2=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) {
+ public virtual void SynErr (string filename, int line, int col, int n) {
+ string s = GetErrorString(n);
+ errorStream.WriteLine(errMsgFormat, filename, line, col, s);
+ count++;
+ }
+ public string GetErrorString(int n) {
string s;
- Console.Write("{0}({1},{2}): syntax error: ", filename, line, col);
switch (n) {
case 0: s = "EOF expected"; break;
case 1: s = "ident expected"; break;
@@ -2202,40 +2220,23 @@ public class Errors { default: s = "error " + n; break;
}
- //errorStream.WriteLine(errMsgFormat, line, col, s);
- errorStream.WriteLine(s);
- count++;
+ return s;
}
- public void SemErr (int line, int col, string/*!*/ s) {
+ public virtual void SemErr (string filename, int line, int col, string/*!*/ s) {
Contract.Requires(s != null);
- errorStream.WriteLine(errMsgFormat, line, col, s);
- count++;
- }
-
- public void SemErr (string filename, int line, int col, string/*!*/ s) {
- Contract.Requires(s != null);
- errorStream.WriteLine(errMsgFormat4, filename, line, col, s);
+ errorStream.WriteLine(errMsgFormat, filename, line, col, s);
count++;
}
- public void SemErr (string s) {
- errorStream.WriteLine(s);
- count++;
+ public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors
+ Contract.Requires(tok != null);
+ Contract.Requires(msg != null);
+ SemErr(tok.filename, tok.line, tok.col, msg);
}
- public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors
- Contract.Requires(tok != null);
- Contract.Requires(msg != null);
- SemErr(tok.filename, tok.line, tok.col, msg);
- }
-
- public void Warning (int line, int col, string s) {
- errorStream.WriteLine(errMsgFormat, line, col, s);
- }
-
- public void Warning(string s) {
- errorStream.WriteLine(s);
+ public virtual void Warning (int line, int col, string s) {
+ errorStream.WriteLine(warningMsgFormat, line, col, s);
}
} // Errors
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index 75d301a4..de87c6ad 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -375,7 +375,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/Test/dafny1/Answer b/Test/dafny1/Answer index 306de96c..45081e03 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -39,6 +39,10 @@ Dafny program verifier finished with 8 verified, 0 errors Dafny program verifier finished with 10 verified, 0 errors
+-------------------- Cubes.dfy --------------------
+
+Dafny program verifier finished with 2 verified, 0 errors
+
-------------------- SumOfCubes.dfy --------------------
Dafny program verifier finished with 17 verified, 0 errors
diff --git a/Test/dafny1/Cubes.dfy b/Test/dafny1/Cubes.dfy new file mode 100644 index 00000000..1ada79fa --- /dev/null +++ b/Test/dafny1/Cubes.dfy @@ -0,0 +1,23 @@ +method Cubes(a: array<int>)
+ requires a != null;
+ modifies a;
+ ensures (forall i :: 0 <= i && i < a.Length ==> a[i] == i*i*i);
+{
+ var n := 0;
+ var c := 0;
+ var k := 1;
+ var m := 6;
+ while (n < a.Length)
+ invariant n <= a.Length;
+ invariant (forall i :: 0 <= i && i < n ==> a[i] == i*i*i);
+ invariant c == n*n*n;
+ invariant k == 3*n*n + 3*n + 1;
+ invariant m == 6*n + 6;
+ {
+ a[n] := c;
+ c := c + k;
+ k := k + m;
+ m := m + 6;
+ n := n + 1;
+ }
+}
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat index ea5b0ec7..8a21b3d8 100644 --- a/Test/dafny1/runtest.bat +++ b/Test/dafny1/runtest.bat @@ -18,7 +18,7 @@ for %%f in (Queue.dfy ListCopy.dfy ListReverse.dfy ListContents.dfy
MatrixFun.dfy
SchorrWaite.dfy
- SumOfCubes.dfy
+ Cubes.dfy SumOfCubes.dfy
TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy
Celebrity.dfy
UltraFilter.dfy) do (
diff --git a/Test/test0/Answer b/Test/test0/Answer index 8d9ba2c3..9e60f623 100644 --- a/Test/test0/Answer +++ b/Test/test0/Answer @@ -2,7 +2,7 @@ Boogie program verifier finished with 0 verified, 0 errors
Boogie program verifier finished with 0 verified, 0 errors
-Triggers0.bpl(14,31): Error: the 'nopats' quantifier attribute expects a string-literal parameter
+Triggers0.bpl(14,31): error: the 'nopats' quantifier attribute expects a string-literal parameter
1 parse errors detected in Triggers0.bpl
Triggers1.bpl(7,17): Error: boolean operators are not allowed in triggers
Triggers1.bpl(11,21): Error: boolean operators are not allowed in triggers
@@ -86,22 +86,22 @@ Boogie program verifier finished with 0 verified, 0 errors Arrays1.bpl(11,11): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: Q
Arrays1.bpl(14,15): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: Q
2 type checking errors detected in Arrays1.bpl
-Types0.bpl(6,18): Error: expected identifier before ':'
-Types0.bpl(6,12): Error: expecting an identifier as parameter name
+Types0.bpl(6,18): error: expected identifier before ':'
+Types0.bpl(6,12): error: expecting an identifier as parameter name
2 parse errors detected in Types0.bpl
Types1.bpl(6,11): Error: undeclared type: x
Types1.bpl(7,11): Error: undeclared type: x
Types1.bpl(7,14): Error: undeclared type: x
3 name resolution errors detected in Types1.bpl
-WhereParsing.bpl(14,37): Error: where clause not allowed here
-WhereParsing.bpl(15,33): Error: where clause not allowed here
+WhereParsing.bpl(14,37): error: where clause not allowed here
+WhereParsing.bpl(15,33): error: where clause not allowed here
2 parse errors detected in WhereParsing.bpl
-WhereParsing0.bpl(17,38): Error: where clause not allowed here
-WhereParsing0.bpl(18,38): Error: where clause not allowed here
+WhereParsing0.bpl(17,38): error: where clause not allowed here
+WhereParsing0.bpl(18,38): error: where clause not allowed here
2 parse errors detected in WhereParsing0.bpl
-WhereParsing1.bpl(14,27): syntax error: ")" expected
+WhereParsing1.bpl(14,27): error: ")" expected
1 parse errors detected in WhereParsing1.bpl
-WhereParsing2.bpl(1,14): syntax error: ";" expected
+WhereParsing2.bpl(1,14): error: ";" expected
1 parse errors detected in WhereParsing2.bpl
WhereResolution.bpl(28,38): Error: undeclared identifier: alpha
WhereResolution.bpl(32,30): Error: old expressions allowed only in two-state contexts
@@ -109,25 +109,25 @@ WhereResolution.bpl(32,30): Error: old expressions allowed only in two-state con BadLabels0.bpl(4,2): Error: more than one declaration of block name: X
BadLabels0.bpl(11,4): Error: more than one declaration of block name: Y
2 name resolution errors detected in BadLabels0.bpl
-BadLabels1.bpl(4,3): Error: Error: goto label 'X' is undefined or out of reach
-BadLabels1.bpl(5,3): Error: Error: goto label 'Y' is undefined or out of reach
-BadLabels1.bpl(10,3): Error: Error: goto label 'X' is undefined or out of reach
-BadLabels1.bpl(24,5): Error: Error: goto label 'K' is undefined or out of reach
-BadLabels1.bpl(30,5): Error: Error: goto label 'A' is undefined or out of reach
-BadLabels1.bpl(38,7): Error: Error: goto label 'M' is undefined or out of reach
-BadLabels1.bpl(41,3): Error: Error: goto label 'B' is undefined or out of reach
-BadLabels1.bpl(47,3): Error: Error: break statement is not inside a loop
-BadLabels1.bpl(49,5): Error: Error: break statement is not inside a loop
-BadLabels1.bpl(60,5): Error: Error: break label 'B' must designate an enclosing statement
-BadLabels1.bpl(63,5): Error: Error: break label 'A' must designate an enclosing statement
-BadLabels1.bpl(64,5): Error: Error: break label 'C' must designate an enclosing statement
-BadLabels1.bpl(65,8): Error: Error: break label 'F' must designate an enclosing statement
+BadLabels1.bpl(4,3): error: Error: goto label 'X' is undefined or out of reach
+BadLabels1.bpl(5,3): error: Error: goto label 'Y' is undefined or out of reach
+BadLabels1.bpl(10,3): error: Error: goto label 'X' is undefined or out of reach
+BadLabels1.bpl(24,5): error: Error: goto label 'K' is undefined or out of reach
+BadLabels1.bpl(30,5): error: Error: goto label 'A' is undefined or out of reach
+BadLabels1.bpl(38,7): error: Error: goto label 'M' is undefined or out of reach
+BadLabels1.bpl(41,3): error: Error: goto label 'B' is undefined or out of reach
+BadLabels1.bpl(47,3): error: Error: break statement is not inside a loop
+BadLabels1.bpl(49,5): error: Error: break statement is not inside a loop
+BadLabels1.bpl(60,5): error: Error: break label 'B' must designate an enclosing statement
+BadLabels1.bpl(63,5): error: Error: break label 'A' must designate an enclosing statement
+BadLabels1.bpl(64,5): error: Error: break label 'C' must designate an enclosing statement
+BadLabels1.bpl(65,8): error: Error: break label 'F' must designate an enclosing statement
13 parse errors detected in BadLabels1.bpl
-LineParse.bpl(1,0): Error: Malformed (#line num [filename]) pragma: #line
-LineParse.bpl(2,0): Error: Malformed (#line num [filename]) pragma: #line
-LineParse.bpl(1,0): Error: Unrecognized pragma: #dontknow what this is No, I don't well, it's an error is what it is
-LineParse.bpl(3,0): Error: Unrecognized pragma: #define ASSERT(x) {if (!(x)) { crash(); }} // error: A B C . txt(12,0)
-LineParse.bpl(6,2): syntax error: EOF expected
+LineParse.bpl(1,0): error: Malformed (#line num [filename]) pragma: #line
+LineParse.bpl(2,0): error: Malformed (#line num [filename]) pragma: #line
+LineParse.bpl(1,0): error: Unrecognized pragma: #dontknow what this is No, I don't well, it's an error is what it is
+LineParse.bpl(3,0): error: Unrecognized pragma: #define ASSERT(x) {if (!(x)) { crash(); }} // error: A B C . txt(12,0)
+LineParse.bpl(6,2): error: EOF expected
5 parse errors detected in LineParse.bpl
LineResolve.bpl(5,1): Error: undeclared identifier: a
LineResolve.bpl(7,2): Error: undeclared identifier: b
@@ -142,15 +142,15 @@ Abc.txt(99,0): Error: undeclared identifier: j c:\Users\leino\Documents\Programs\MyClass.ssc(104,0): Error: undeclared identifier: k
A B C . txt(12,0): Error: undeclared identifier: l
12 name resolution errors detected in LineResolve.bpl
-AttributeParsingErr.bpl(1,33): Error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(3,33): Error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(5,52): Error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(7,37): Error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(9,31): Error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(11,29): Error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(13,13): Error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(15,18): Error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(20,26): Error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(1,33): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(3,33): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(5,52): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(7,37): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(9,31): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(11,29): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(13,13): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(15,18): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(20,26): error: only attributes, not triggers, allowed here
9 parse errors detected in AttributeParsingErr.bpl
type {:sourcefile "test.ssc"} T;
@@ -247,7 +247,7 @@ Orderings.bpl(15,23): Error: c0 occurs more than once as parent Orderings.bpl(16,19): Error: constant cannot be its own parent
Orderings.bpl(18,20): Error: the parent of a constant has to be a constant
4 name resolution errors detected in Orderings.bpl
-BadQuantifier.bpl(3,15): syntax error: invalid QuantifierBody
+BadQuantifier.bpl(3,15): error: invalid QuantifierBody
1 parse errors detected in BadQuantifier.bpl
EmptyCallArgs.bpl(31,2): Error: type variable must occur in types of given arguments: a
EmptyCallArgs.bpl(32,2): Error: type variable must occur in types of given arguments: a
diff --git a/Test/test2/Answer b/Test/test2/Answer index ae27fa94..4c0cbfc1 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -3,17 +3,17 @@ 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
+ FormulaTerm.bpl(8,1): start
Boogie program verifier finished with 11 verified, 1 error
-------------------- FormulaTerm2.bpl --------------------
FormulaTerm2.bpl(39,5): Error BP5001: This assertion might not hold.
Execution trace:
- FormulaTerm2.bpl(36,3): start
+ FormulaTerm2.bpl(36,3): start
FormulaTerm2.bpl(47,5): Error BP5001: This assertion might not hold.
Execution trace:
- FormulaTerm2.bpl(45,3): start
+ FormulaTerm2.bpl(45,3): start
Boogie program verifier finished with 2 verified, 2 errors
@@ -21,21 +21,21 @@ Boogie program verifier finished with 2 verified, 2 errors 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
+ Passification.bpl(39,1): A
Passification.bpl(116,3): Error BP5001: This assertion might not hold.
Execution trace:
- Passification.bpl(106,1): L0
- Passification.bpl(111,1): L1
- Passification.bpl(115,1): L2
+ Passification.bpl(106,1): L0
+ Passification.bpl(111,1): L1
+ Passification.bpl(115,1): L2
Passification.bpl(151,3): Error BP5001: This assertion might not hold.
Execution trace:
- Passification.bpl(144,1): L0
- Passification.bpl(150,1): L2
+ Passification.bpl(144,1): L0
+ Passification.bpl(150,1): L2
Passification.bpl(165,3): Error BP5001: This assertion might not hold.
Execution trace:
- Passification.bpl(158,1): L0
- Passification.bpl(161,1): L1
- Passification.bpl(164,1): L2
+ Passification.bpl(158,1): L0
+ Passification.bpl(161,1): L1
+ Passification.bpl(164,1): L2
Boogie program verifier finished with 7 verified, 4 errors
@@ -47,23 +47,23 @@ Boogie program verifier finished with 4 verified, 0 errors 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(28,3): start
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(34,3): start
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(39,3): start
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(45,3): start
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
+ Ensures.bpl(70,3): start
Boogie program verifier finished with 5 verified, 5 errors
@@ -71,7 +71,7 @@ Boogie program verifier finished with 5 verified, 5 errors 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
+ Old.bpl(28,3): start
Boogie program verifier finished with 7 verified, 1 error
@@ -84,75 +84,75 @@ OldIllegal.bpl(14,23): Error: old expressions allowed only in two-state contexts 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(42,3): start
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
+ Arrays.bpl(123,3): start
Boogie program verifier finished with 8 verified, 2 errors
-------------------- Axioms.bpl --------------------
Axioms.bpl(19,5): Error BP5001: This assertion might not hold.
Execution trace:
- Axioms.bpl(18,3): start
+ Axioms.bpl(18,3): start
Boogie program verifier finished with 2 verified, 1 error
-------------------- Quantifiers.bpl --------------------
Quantifiers.bpl(20,5): Error BP5001: This assertion might not hold.
Execution trace:
- Quantifiers.bpl(19,3): start
+ Quantifiers.bpl(19,3): start
Quantifiers.bpl(43,5): Error BP5001: This assertion might not hold.
Execution trace:
- Quantifiers.bpl(42,3): start
+ Quantifiers.bpl(42,3): start
Quantifiers.bpl(65,5): Error BP5001: This assertion might not hold.
Execution trace:
- Quantifiers.bpl(64,3): start
+ Quantifiers.bpl(64,3): start
Quantifiers.bpl(73,5): Error BP5001: This assertion might not hold.
Execution trace:
- Quantifiers.bpl(71,3): start
+ Quantifiers.bpl(71,3): start
Quantifiers.bpl(125,5): Error BP5001: This assertion might not hold.
Execution trace:
- Quantifiers.bpl(124,3): start
+ Quantifiers.bpl(124,3): start
Quantifiers.bpl(150,5): Error BP5001: This assertion might not hold.
Execution trace:
- Quantifiers.bpl(149,3): start
+ Quantifiers.bpl(149,3): start
Boogie program verifier finished with 8 verified, 6 errors
-------------------- Call.bpl --------------------
Call.bpl(13,5): Error BP5001: This assertion might not hold.
Execution trace:
- Call.bpl(9,3): entry
+ Call.bpl(9,3): entry
Call.bpl(46,5): Error BP5001: This assertion might not hold.
Execution trace:
- Call.bpl(45,3): start
+ Call.bpl(45,3): start
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
+ Call.bpl(53,3): start
Boogie program verifier finished with 2 verified, 3 errors
-------------------- AssumeEnsures.bpl --------------------
AssumeEnsures.bpl(28,9): Error BP5001: This assertion might not hold.
Execution trace:
- AssumeEnsures.bpl(26,5): entry
+ AssumeEnsures.bpl(26,5): entry
AssumeEnsures.bpl(47,9): Error BP5001: This assertion might not hold.
Execution trace:
- AssumeEnsures.bpl(46,5): entry
+ AssumeEnsures.bpl(46,5): entry
AssumeEnsures.bpl(62,9): Error BP5001: This assertion might not hold.
Execution trace:
- AssumeEnsures.bpl(60,5): entry
+ AssumeEnsures.bpl(60,5): entry
Boogie program verifier finished with 4 verified, 3 errors
-------------------- CutBackEdge.bpl --------------------
CutBackEdge.bpl(10,5): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
- CutBackEdge.bpl(5,3): entry
- CutBackEdge.bpl(9,3): block850
+ CutBackEdge.bpl(5,3): entry
+ CutBackEdge.bpl(9,3): block850
Boogie program verifier finished with 0 verified, 1 error
@@ -163,8 +163,8 @@ Boogie program verifier finished with 2 verified, 0 errors -------------------- LoopInvAssume.bpl --------------------
LoopInvAssume.bpl(18,7): Error BP5001: This assertion might not hold.
Execution trace:
- LoopInvAssume.bpl(8,4): entry
- LoopInvAssume.bpl(16,4): exit
+ LoopInvAssume.bpl(8,4): entry
+ LoopInvAssume.bpl(16,4): exit
Boogie program verifier finished with 0 verified, 1 error
@@ -214,170 +214,170 @@ strings-where.bpl(990,36): Error: invalid argument types (any and name) to binar 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
- Structured.bpl(246,5): anon6_LoopBody
- Structured.bpl(247,7): anon7_LoopBody
- Structured.bpl(248,11): anon8_Then
- Structured.bpl(252,5): anon4
- Structured.bpl(252,14): anon9_Then
+ Structured.bpl(244,5): anon0
+ Structured.bpl(246,5): anon6_LoopBody
+ Structured.bpl(247,7): anon7_LoopBody
+ Structured.bpl(248,11): anon8_Then
+ Structured.bpl(252,5): anon4
+ Structured.bpl(252,14): anon9_Then
Structured.bpl(303,3): Error BP5001: This assertion might not hold.
Execution trace:
- Structured.bpl(299,5): anon0
- Structured.bpl(300,3): anon3_Else
- Structured.bpl(303,3): anon2
+ Structured.bpl(299,5): anon0
+ Structured.bpl(300,3): anon3_Else
+ Structured.bpl(303,3): anon2
Structured.bpl(311,7): Error BP5001: This assertion might not hold.
Execution trace:
- Structured.bpl(308,3): anon0
- Structured.bpl(308,3): anon1_Then
- Structured.bpl(309,5): A
+ Structured.bpl(308,3): anon0
+ Structured.bpl(308,3): anon1_Then
+ Structured.bpl(309,5): A
Boogie program verifier finished with 15 verified, 3 errors
-------------------- Where.bpl --------------------
Where.bpl(8,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(6,3): anon0
+ Where.bpl(6,3): anon0
Where.bpl(22,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(16,5): anon0
+ Where.bpl(16,5): anon0
Where.bpl(32,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(30,3): anon0
+ Where.bpl(30,3): anon0
Where.bpl(44,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(40,5): anon0
+ Where.bpl(40,5): anon0
Where.bpl(57,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(52,3): anon0
+ Where.bpl(52,3): anon0
Where.bpl(111,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(102,5): anon0
- Where.bpl(104,3): anon3_LoopHead
- Where.bpl(104,3): anon3_LoopDone
+ Where.bpl(102,5): anon0
+ Where.bpl(104,3): anon3_LoopHead
+ Where.bpl(104,3): anon3_LoopDone
Where.bpl(128,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(121,5): anon0
- Where.bpl(122,3): anon3_LoopHead
- Where.bpl(122,3): anon3_LoopDone
+ Where.bpl(121,5): anon0
+ Where.bpl(122,3): anon3_LoopHead
+ Where.bpl(122,3): anon3_LoopDone
Where.bpl(145,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(138,5): anon0
- Where.bpl(139,3): anon3_LoopHead
- Where.bpl(139,3): anon3_LoopDone
+ Where.bpl(138,5): anon0
+ Where.bpl(139,3): anon3_LoopHead
+ Where.bpl(139,3): anon3_LoopDone
Where.bpl(162,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(155,5): anon0
- Where.bpl(156,3): anon3_LoopHead
- Where.bpl(156,3): anon3_LoopDone
+ Where.bpl(155,5): anon0
+ Where.bpl(156,3): anon3_LoopHead
+ Where.bpl(156,3): anon3_LoopDone
Boogie program verifier finished with 2 verified, 9 errors
-------------------- UpdateExpr.bpl --------------------
UpdateExpr.bpl(14,3): Error BP5001: This assertion might not hold.
Execution trace:
- UpdateExpr.bpl(14,3): anon0
+ UpdateExpr.bpl(14,3): anon0
UpdateExpr.bpl(19,3): Error BP5001: This assertion might not hold.
Execution trace:
- UpdateExpr.bpl(19,3): anon0
+ UpdateExpr.bpl(19,3): anon0
UpdateExpr.bpl(32,3): Error BP5001: This assertion might not hold.
Execution trace:
- UpdateExpr.bpl(32,3): anon0
+ UpdateExpr.bpl(32,3): anon0
UpdateExpr.bpl(38,3): Error BP5001: This assertion might not hold.
Execution trace:
- UpdateExpr.bpl(38,3): anon0
+ UpdateExpr.bpl(38,3): anon0
UpdateExpr.bpl(52,3): Error BP5001: This assertion might not hold.
Execution trace:
- UpdateExpr.bpl(51,5): anon0
+ UpdateExpr.bpl(51,5): anon0
Boogie program verifier finished with 5 verified, 5 errors
-------------------- NeverPattern.bpl --------------------
NeverPattern.bpl(16,3): Error BP5001: This assertion might not hold.
Execution trace:
- NeverPattern.bpl(15,3): anon0
+ NeverPattern.bpl(15,3): anon0
NeverPattern.bpl(22,3): Error BP5001: This assertion might not hold.
Execution trace:
- NeverPattern.bpl(21,3): anon0
+ NeverPattern.bpl(21,3): anon0
NeverPattern.bpl(28,3): Error BP5001: This assertion might not hold.
Execution trace:
- NeverPattern.bpl(27,3): anon0
+ NeverPattern.bpl(27,3): anon0
Boogie program verifier finished with 1 verified, 3 errors
-------------------- NullaryMaps.bpl --------------------
NullaryMaps.bpl(28,3): Error BP5001: This assertion might not hold.
Execution trace:
- NullaryMaps.bpl(28,3): anon0
+ NullaryMaps.bpl(28,3): anon0
NullaryMaps.bpl(30,3): Error BP5001: This assertion might not hold.
Execution trace:
- NullaryMaps.bpl(28,3): anon0
+ NullaryMaps.bpl(28,3): anon0
NullaryMaps.bpl(36,3): Error BP5001: This assertion might not hold.
Execution trace:
- NullaryMaps.bpl(36,3): anon0
+ NullaryMaps.bpl(36,3): anon0
Boogie program verifier finished with 2 verified, 3 errors
-------------------- Implies.bpl --------------------
Implies.bpl(12,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(11,3): anon0
+ Implies.bpl(11,3): anon0
Implies.bpl(15,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(11,3): anon0
+ Implies.bpl(11,3): anon0
Implies.bpl(19,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(19,3): anon0
+ Implies.bpl(19,3): anon0
Implies.bpl(24,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(24,3): anon0
+ Implies.bpl(24,3): anon0
Implies.bpl(25,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(24,3): anon0
+ Implies.bpl(24,3): anon0
Implies.bpl(29,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(29,3): anon0
+ Implies.bpl(29,3): anon0
Implies.bpl(34,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(34,3): anon0
+ Implies.bpl(34,3): anon0
Implies.bpl(35,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(34,3): anon0
+ Implies.bpl(34,3): anon0
Boogie program verifier finished with 0 verified, 8 errors
-------------------- IfThenElse1.bpl --------------------
IfThenElse1.bpl(26,3): Error BP5001: This assertion might not hold.
Execution trace:
- IfThenElse1.bpl(26,3): anon0
+ IfThenElse1.bpl(26,3): anon0
IfThenElse1.bpl(33,3): Error BP5001: This assertion might not hold.
Execution trace:
- IfThenElse1.bpl(33,3): anon0
+ IfThenElse1.bpl(33,3): anon0
Boogie program verifier finished with 2 verified, 2 errors
-------------------- Lambda.bpl --------------------
Lambda.bpl(37,3): Error BP5001: This assertion might not hold.
Execution trace:
- Lambda.bpl(36,5): anon0
+ Lambda.bpl(36,5): anon0
Lambda.bpl(38,3): Error BP5001: This assertion might not hold.
Execution trace:
- Lambda.bpl(36,5): anon0
+ Lambda.bpl(36,5): anon0
Boogie program verifier finished with 4 verified, 2 errors
-------------------- LambdaPoly.bpl --------------------
LambdaPoly.bpl(28,5): Error BP5001: This assertion might not hold.
Execution trace:
- LambdaPoly.bpl(24,5): anon0
- LambdaPoly.bpl(27,5): anon4_Then
+ LambdaPoly.bpl(24,5): anon0
+ LambdaPoly.bpl(27,5): anon4_Then
LambdaPoly.bpl(31,5): Error BP5001: This assertion might not hold.
Execution trace:
- LambdaPoly.bpl(24,5): anon0
- LambdaPoly.bpl(30,5): anon5_Then
+ LambdaPoly.bpl(24,5): anon0
+ LambdaPoly.bpl(30,5): anon5_Then
LambdaPoly.bpl(36,5): Error BP5001: This assertion might not hold.
Execution trace:
- LambdaPoly.bpl(24,5): anon0
- LambdaPoly.bpl(34,5): anon5_Else
+ LambdaPoly.bpl(24,5): anon0
+ LambdaPoly.bpl(34,5): anon5_Else
Boogie program verifier finished with 1 verified, 3 errors
@@ -385,28 +385,28 @@ Boogie program verifier finished with 1 verified, 3 errors 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(42,3): start
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
+ Arrays.bpl(123,3): start
Boogie program verifier finished with 8 verified, 2 errors
-------------------- Lambda.bpl /typeEncoding:m --------------------
Lambda.bpl(37,3): Error BP5001: This assertion might not hold.
Execution trace:
- Lambda.bpl(36,5): anon0
+ Lambda.bpl(36,5): anon0
Lambda.bpl(38,3): Error BP5001: This assertion might not hold.
Execution trace:
- Lambda.bpl(36,5): anon0
+ Lambda.bpl(36,5): anon0
Boogie program verifier finished with 4 verified, 2 errors
-------------------- TypeEncodingM.bpl /typeEncoding:m --------------------
TypeEncodingM.bpl(24,3): Error BP5001: This assertion might not hold.
Execution trace:
- TypeEncodingM.bpl(11,9): anon0
+ TypeEncodingM.bpl(11,9): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- sk_hack.bpl --------------------
@@ -416,28 +416,28 @@ Boogie program verifier finished with 1 verified, 0 errors -------------------- CallForall.bpl --------------------
CallForall.bpl(17,3): Error BP5001: This assertion might not hold.
Execution trace:
- CallForall.bpl(17,3): anon0
+ CallForall.bpl(17,3): anon0
CallForall.bpl(29,3): Error BP5001: This assertion might not hold.
Execution trace:
- CallForall.bpl(28,3): anon0
+ CallForall.bpl(28,3): anon0
CallForall.bpl(41,3): Error BP5001: This assertion might not hold.
Execution trace:
- CallForall.bpl(40,3): anon0
+ CallForall.bpl(40,3): anon0
CallForall.bpl(47,3): Error BP5001: This assertion might not hold.
Execution trace:
- CallForall.bpl(46,3): anon0
+ CallForall.bpl(46,3): anon0
CallForall.bpl(75,3): Error BP5001: This assertion might not hold.
Execution trace:
- CallForall.bpl(75,3): anon0
+ CallForall.bpl(75,3): anon0
CallForall.bpl(111,3): Error BP5001: This assertion might not hold.
Execution trace:
- CallForall.bpl(109,3): anon0
+ CallForall.bpl(109,3): anon0
CallForall.bpl(118,3): Error BP5001: This assertion might not hold.
Execution trace:
- CallForall.bpl(117,3): anon0
+ CallForall.bpl(117,3): anon0
CallForall.bpl(125,3): Error BP5001: This assertion might not hold.
Execution trace:
- CallForall.bpl(124,3): anon0
+ CallForall.bpl(124,3): anon0
Boogie program verifier finished with 10 verified, 8 errors
@@ -445,13 +445,13 @@ Boogie program verifier finished with 10 verified, 8 errors 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
+ ContractEvaluationOrder.bpl(7,5): anon0
ContractEvaluationOrder.bpl(15,3): Error BP5001: This assertion might not hold.
Execution trace:
- ContractEvaluationOrder.bpl(12,5): anon0
+ ContractEvaluationOrder.bpl(12,5): anon0
ContractEvaluationOrder.bpl(24,3): Error BP5002: A precondition for this call might not hold.
ContractEvaluationOrder.bpl(30,3): Related location: This is the precondition that might not hold.
Execution trace:
- ContractEvaluationOrder.bpl(23,5): anon0
+ ContractEvaluationOrder.bpl(23,5): anon0
Boogie program verifier finished with 1 verified, 3 errors
|