diff options
| -rw-r--r-- | Dafny/Dafny.atg | 38 | ||||
| -rw-r--r-- | Dafny/Parser.cs | 38 | ||||
| -rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs | 21 |
3 files changed, 59 insertions, 38 deletions
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index 1629fe51..5280521f 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -14,14 +14,15 @@ using System.IO; using System.Text;
COMPILER Dafny
/*--------------------------------------------------------------------------*/
-static ModuleDecl theModule;
-static BuiltIns theBuiltIns;
-static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
-static AssignmentRhs/*!*/ dummyRhs = new ExprRhs(dummyExpr, null);
-static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null);
-static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);
-static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");
-static int anonymousIds = 0;
+readonly Expression/*!*/ dummyExpr;
+readonly AssignmentRhs/*!*/ dummyRhs;
+readonly FrameExpression/*!*/ dummyFrameExpr;
+readonly Statement/*!*/ dummyStmt;
+readonly Attributes.Argument/*!*/ dummyAttrArg;
+readonly ModuleDecl theModule;
+readonly BuiltIns theBuiltIns;
+int anonymousIds = 0;
+
struct MemberModifiers {
public bool IsGhost;
public bool IsStatic;
@@ -72,19 +73,26 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, Contract.Requires(filename != null);
Contract.Requires(module != null);
Contract.Requires(errors != null);
- var oldModule = theModule;
- theModule = module;
- BuiltIns oldBuiltIns = builtIns;
- theBuiltIns = builtIns;
byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));
MemoryStream ms = new MemoryStream(buffer,false);
Scanner scanner = new Scanner(ms, errors, filename);
- Parser parser = new Parser(scanner, errors);
+ Parser parser = new Parser(scanner, errors, module, builtIns);
parser.Parse();
- theModule = oldModule;
- theBuiltIns = oldBuiltIns;
return parser.errors.count;
}
+public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, BuiltIns builtIns)
+ : this(scanner, errors) // the real work
+{
+ // initialize readonly fields
+ dummyExpr = new LiteralExpr(Token.NoToken);
+ dummyRhs = new ExprRhs(dummyExpr, null);
+ dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null);
+ dummyStmt = new ReturnStmt(Token.NoToken, null);
+ dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");
+ theModule = module;
+ theBuiltIns = builtIns;
+}
+
bool IsAttribute() {
Token x = scanner.Peek();
return la.kind == _lbrace && x.kind == _colon;
diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs index 2f49f689..306dd369 100644 --- a/Dafny/Parser.cs +++ b/Dafny/Parser.cs @@ -34,14 +34,15 @@ public class Parser { public Token/*!*/ la; // lookahead token
int errDist = minErrDist;
-static ModuleDecl theModule;
-static BuiltIns theBuiltIns;
-static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
-static AssignmentRhs/*!*/ dummyRhs = new ExprRhs(dummyExpr, null);
-static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null);
-static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);
-static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");
-static int anonymousIds = 0;
+readonly Expression/*!*/ dummyExpr;
+readonly AssignmentRhs/*!*/ dummyRhs;
+readonly FrameExpression/*!*/ dummyFrameExpr;
+readonly Statement/*!*/ dummyStmt;
+readonly Attributes.Argument/*!*/ dummyAttrArg;
+readonly ModuleDecl theModule;
+readonly BuiltIns theBuiltIns;
+int anonymousIds = 0;
+
struct MemberModifiers {
public bool IsGhost;
public bool IsStatic;
@@ -92,19 +93,26 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, Contract.Requires(filename != null);
Contract.Requires(module != null);
Contract.Requires(errors != null);
- var oldModule = theModule;
- theModule = module;
- BuiltIns oldBuiltIns = builtIns;
- theBuiltIns = builtIns;
byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));
MemoryStream ms = new MemoryStream(buffer,false);
Scanner scanner = new Scanner(ms, errors, filename);
- Parser parser = new Parser(scanner, errors);
+ Parser parser = new Parser(scanner, errors, module, builtIns);
parser.Parse();
- theModule = oldModule;
- theBuiltIns = oldBuiltIns;
return parser.errors.count;
}
+public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, BuiltIns builtIns)
+ : this(scanner, errors) // the real work
+{
+ // initialize readonly fields
+ dummyExpr = new LiteralExpr(Token.NoToken);
+ dummyRhs = new ExprRhs(dummyExpr, null);
+ dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null);
+ dummyStmt = new ReturnStmt(Token.NoToken, null);
+ dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");
+ theModule = module;
+ theBuiltIns = builtIns;
+}
+
bool IsAttribute() {
Token x = scanner.Peek();
return la.kind == _lbrace && x.kind == _colon;
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs index 16ed18f4..5fa7d91c 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs @@ -191,17 +191,22 @@ namespace DafnyLanguage // Run the verifier
var newErrors = new List<DafnyError>();
- bool success = DafnyDriver.Verify(program, errorInfo => {
- newErrors.Add(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.Msg));
- foreach (var aux in errorInfo.Aux) {
- newErrors.Add(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.Msg));
+ try {
+ bool success = DafnyDriver.Verify(program, errorInfo => {
+ newErrors.Add(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.Msg));
+ foreach (var aux in errorInfo.Aux) {
+ newErrors.Add(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.Msg));
+ }
+ });
+ if (!success) {
+ newErrors.Clear();
+ newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "verification process error"));
}
- });
- errorListHolder.PopulateErrorList(newErrors, true, snapshot);
- if (!success) {
+ } catch (Exception e) {
newErrors.Clear();
- newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "verification process error"));
+ newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "verification process error: " + e.Message));
}
+ errorListHolder.PopulateErrorList(newErrors, true, snapshot);
lock (this) {
bufferChangesPreVerificationStart.Clear();
|