diff options
| -rw-r--r-- | Source/Core/BoogiePL.atg | 58 | ||||
| -rw-r--r-- | Source/Core/Core.csproj | 3 | ||||
| -rw-r--r-- | Source/Core/Parser.cs | 58 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 38 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 38 | ||||
| -rw-r--r-- | Test/test15/Answer | 28 | ||||
| -rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs | 21 |
7 files changed, 146 insertions, 98 deletions
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index aed741d8..9c721703 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -19,16 +19,15 @@ COMPILER BoogiePL /*--------------------------------------------------------------------------*/
-static Program/*!*/ Pgm = new Program();
+readonly Program/*!*/ Pgm;
-static Expr/*!*/ dummyExpr = new LiteralExpr(Token.NoToken, false);
-static Cmd/*!*/ dummyCmd = new AssumeCmd(Token.NoToken, dummyExpr);
-static Block/*!*/ dummyBlock = new Block(Token.NoToken, "dummyBlock", new CmdSeq(),
- new ReturnCmd(Token.NoToken));
-static Bpl.Type/*!*/ dummyType = new BasicType(Token.NoToken, SimpleType.Bool);
-static Bpl.ExprSeq/*!*/ dummyExprSeq = new ExprSeq ();
-static TransferCmd/*!*/ dummyTransferCmd = new ReturnCmd(Token.NoToken);
-static StructuredCmd/*!*/ dummyStructuredCmd = new BreakCmd(Token.NoToken, null);
+readonly Expr/*!*/ dummyExpr;
+readonly Cmd/*!*/ dummyCmd;
+readonly Block/*!*/ dummyBlock;
+readonly Bpl.Type/*!*/ dummyType;
+readonly Bpl.ExprSeq/*!*/ dummyExprSeq;
+readonly TransferCmd/*!*/ dummyTransferCmd;
+readonly StructuredCmd/*!*/ dummyStructuredCmd;
///<summary>
///Returns the number of parsing errors encountered. If 0, "program" returns as
@@ -64,20 +63,33 @@ public static int Parse (string s, string/*!*/ filename, out /*maybe null*/ Prog Errors errors = new Errors();
Scanner scanner = new Scanner(ms, errors, filename);
- Parser parser = new Parser(scanner, errors);
- Pgm = new Program(); // reset the global variable
- parser.Parse();
- if (parser.errors.count == 0)
- {
- program = Pgm;
- program.ProcessDatatypeConstructors();
- return 0;
- }
- else
- {
- program = null;
- return parser.errors.count;
- }
+ Parser parser = new Parser(scanner, errors, false);
+ parser.Parse();
+ if (parser.errors.count == 0)
+ {
+ program = parser.Pgm;
+ program.ProcessDatatypeConstructors();
+ return 0;
+ }
+ else
+ {
+ program = null;
+ return parser.errors.count;
+ }
+}
+
+public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, bool disambiguation)
+ : this(scanner, errors)
+{
+ // initialize readonly fields
+ Pgm = new Program();
+ dummyExpr = new LiteralExpr(Token.NoToken, false);
+ dummyCmd = new AssumeCmd(Token.NoToken, dummyExpr);
+ dummyBlock = new Block(Token.NoToken, "dummyBlock", new CmdSeq(), new ReturnCmd(Token.NoToken));
+ dummyType = new BasicType(Token.NoToken, SimpleType.Bool);
+ dummyExprSeq = new ExprSeq ();
+ dummyTransferCmd = new ReturnCmd(Token.NoToken);
+ dummyStructuredCmd = new BreakCmd(Token.NoToken, null);
}
// Class to represent the bounds of a bitvector expression t[a:b].
diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj index cff4f7f2..9a24b6b2 100644 --- a/Source/Core/Core.csproj +++ b/Source/Core/Core.csproj @@ -213,6 +213,9 @@ <Install>true</Install>
</BootstrapperPackage>
</ItemGroup>
+ <ItemGroup>
+ <None Include="BoogiePL.atg" />
+ </ItemGroup>
<Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
<!-- To modify your build process, add your task inside one of the targets below and uncomment it.
Other similar extension points exist, see Microsoft.Common.targets.
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 5a6f8098..69f505bc 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -38,16 +38,15 @@ public class Parser { public Token/*!*/ la; // lookahead token
int errDist = minErrDist;
-static Program/*!*/ Pgm = new Program();
+readonly Program/*!*/ Pgm;
-static Expr/*!*/ dummyExpr = new LiteralExpr(Token.NoToken, false);
-static Cmd/*!*/ dummyCmd = new AssumeCmd(Token.NoToken, dummyExpr);
-static Block/*!*/ dummyBlock = new Block(Token.NoToken, "dummyBlock", new CmdSeq(),
- new ReturnCmd(Token.NoToken));
-static Bpl.Type/*!*/ dummyType = new BasicType(Token.NoToken, SimpleType.Bool);
-static Bpl.ExprSeq/*!*/ dummyExprSeq = new ExprSeq ();
-static TransferCmd/*!*/ dummyTransferCmd = new ReturnCmd(Token.NoToken);
-static StructuredCmd/*!*/ dummyStructuredCmd = new BreakCmd(Token.NoToken, null);
+readonly Expr/*!*/ dummyExpr;
+readonly Cmd/*!*/ dummyCmd;
+readonly Block/*!*/ dummyBlock;
+readonly Bpl.Type/*!*/ dummyType;
+readonly Bpl.ExprSeq/*!*/ dummyExprSeq;
+readonly TransferCmd/*!*/ dummyTransferCmd;
+readonly StructuredCmd/*!*/ dummyStructuredCmd;
///<summary>
///Returns the number of parsing errors encountered. If 0, "program" returns as
@@ -83,20 +82,33 @@ public static int Parse (string s, string/*!*/ filename, out /*maybe null*/ Prog Errors errors = new Errors();
Scanner scanner = new Scanner(ms, errors, filename);
- Parser parser = new Parser(scanner, errors);
- Pgm = new Program(); // reset the global variable
- parser.Parse();
- if (parser.errors.count == 0)
- {
- program = Pgm;
- program.ProcessDatatypeConstructors();
- return 0;
- }
- else
- {
- program = null;
- return parser.errors.count;
- }
+ Parser parser = new Parser(scanner, errors, false);
+ parser.Parse();
+ if (parser.errors.count == 0)
+ {
+ program = parser.Pgm;
+ program.ProcessDatatypeConstructors();
+ return 0;
+ }
+ else
+ {
+ program = null;
+ return parser.errors.count;
+ }
+}
+
+public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, bool disambiguation)
+ : this(scanner, errors)
+{
+ // initialize readonly fields
+ Pgm = new Program();
+ dummyExpr = new LiteralExpr(Token.NoToken, false);
+ dummyCmd = new AssumeCmd(Token.NoToken, dummyExpr);
+ dummyBlock = new Block(Token.NoToken, "dummyBlock", new CmdSeq(), new ReturnCmd(Token.NoToken));
+ dummyType = new BasicType(Token.NoToken, SimpleType.Bool);
+ dummyExprSeq = new ExprSeq ();
+ dummyTransferCmd = new ReturnCmd(Token.NoToken);
+ dummyStructuredCmd = new BreakCmd(Token.NoToken, null);
}
// Class to represent the bounds of a bitvector expression t[a:b].
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 1629fe51..5280521f 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/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/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 2f49f689..306dd369 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/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/Test/test15/Answer b/Test/test15/Answer index ae010dc9..24ed0446 100644 --- a/Test/test15/Answer +++ b/Test/test15/Answer @@ -1,9 +1,9 @@ -------------------- NullInModel --------------------
*** MODEL
-%lbl%@47 -> false
-%lbl%+24 -> true
-%lbl%+37 -> true
+%lbl%@46 -> false
+%lbl%+23 -> true
+%lbl%+36 -> true
boolType -> T@T!val!1
intType -> T@T!val!0
null -> T@U!val!0
@@ -33,9 +33,9 @@ Boogie program verifier finished with 0 verified, 1 error -------------------- IntInModel --------------------
*** MODEL
-%lbl%@39 -> false
-%lbl%+23 -> true
-%lbl%+29 -> true
+%lbl%@38 -> false
+%lbl%+22 -> true
+%lbl%+28 -> true
boolType -> T@T!val!1
i -> 0
intType -> T@T!val!0
@@ -58,9 +58,9 @@ Boogie program verifier finished with 0 verified, 1 error -------------------- ModelTest --------------------
*** MODEL
-%lbl%@182 -> false
-%lbl%+119 -> true
-%lbl%+64 -> true
+%lbl%@181 -> false
+%lbl%+118 -> true
+%lbl%+63 -> true
boolType -> T@T!val!1
i@0 -> 1
intType -> T@T!val!0
@@ -114,11 +114,11 @@ Execution trace: CaptureState.bpl(16,5): anon4_Then
CaptureState.bpl(24,5): anon3
*** MODEL
-%lbl%@336 -> false
-%lbl%+112 -> true
-%lbl%+114 -> true
-%lbl%+118 -> true
-%lbl%+191 -> true
+%lbl%@335 -> false
+%lbl%+111 -> true
+%lbl%+113 -> true
+%lbl%+117 -> true
+%lbl%+190 -> true
@MV_state_const -> 6
boolType -> T@T!val!1
F -> T@U!val!2
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();
|