diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/DafnyOptions.cs | 21 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 22 |
2 files changed, 39 insertions, 4 deletions
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 125ab11e..b2593705 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -56,6 +56,8 @@ namespace Microsoft.Dafny public bool AllowGlobals = false;
public bool CountVerificationErrors = true;
public bool Optimize = false;
+ public bool AutoTriggers = true;
+ public bool PrintTooltips = false;
protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {
var args = ps.args; // convenient synonym
@@ -181,6 +183,18 @@ namespace Microsoft.Dafny return true;
}
+ case "printTooltips":
+ PrintTooltips = true;
+ return true;
+
+ case "autoTriggers": {
+ int autoTriggers = 1; // defaults to reporting verification errors
+ if (ps.GetNumericArgument(ref autoTriggers, 2)) {
+ AutoTriggers = autoTriggers == 1;
+ }
+ return true;
+ }
+
case "optimize": {
Optimize = true;
return true;
@@ -276,12 +290,19 @@ namespace Microsoft.Dafny of verification errors.
1 (default) - If preprocessing succeeds, set exit code to the number of
verification errors.
+ /autoTriggers:<n>
+ 0 - Do not generate {:trigger} annotations for user-level quantifiers.
+ 1 (default) - Add a {:trigger} to each user-level quantifier. Existing
+ annotations are preserved.
/optimize Produce optimized C# code, meaning:
- selects optimized C# prelude by passing
/define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE to csc.exe (requires
System.Collections.Immutable.dll in the source directory to successfully
compile).
- passes /optimize flag to csc.exe.
+ /printTooltips
+ Dump additional positional information (displayed as mouse-over tooltips by
+ the VS plugin) to stdout as 'Info' messages.
");
base.Usage(); // also print the Boogie options
}
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index c5535808..300d4985 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -25,7 +25,7 @@ namespace Microsoft.Dafny ConsoleColor col = Console.ForegroundColor;
Console.ForegroundColor = ConsoleColor.Red;
Console.WriteLine("{0}({1},{2}): Error: {3}",
- DafnyOptions.Clo.UseBaseNameForFileName ? System.IO.Path.GetFileName(tok.filename) : tok.filename, tok.line, tok.col - 1,
+ DafnyOptions.Clo.UseBaseNameForFileName ? System.IO.Path.GetFileName(tok.filename) : tok.filename, tok.line, tok.col,
string.Format(msg, args));
Console.ForegroundColor = col;
ErrorCount++;
@@ -254,6 +254,10 @@ namespace Microsoft.Dafny // Populate the members of the basic types
var trunc = new SpecialField(Token.NoToken, "Trunc", "ToBigInteger()", "", "", false, false, false, Type.Int, null);
basicTypeMembers[(int)BasicTypeVariety.Real].Add(trunc.Name, trunc);
+
+ if (DafnyOptions.O.PrintTooltips) {
+ AdditionalInformationReporter = DefaultInformationReporter;
+ }
}
[ContractInvariantMethod]
@@ -264,6 +268,12 @@ namespace Microsoft.Dafny Contract.Invariant(cce.NonNullDictionaryAndValues(datatypeCtors) && Contract.ForAll(datatypeCtors.Values, v => cce.NonNullDictionaryAndValues(v)));
}
+ public void DefaultInformationReporter(AdditionalInformation info) {
+ Console.WriteLine("{0}({1},{2}): Info: {3}",
+ DafnyOptions.Clo.UseBaseNameForFileName ? System.IO.Path.GetFileName(info.Token.filename) : info.Token.filename,
+ info.Token.line, info.Token.col, info.Text);
+ }
+
public void ResolveProgram(Program prog) {
Contract.Requires(prog != null);
var origErrorCount = ErrorCount;
@@ -303,6 +313,10 @@ namespace Microsoft.Dafny rewriters.Add(opaqueRewriter);
rewriters.Add(new TimeLimitRewriter());
+ if (DafnyOptions.O.AutoTriggers) {
+ rewriters.Add(new TriggersRewriter(this));
+ }
+
systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule, false);
prog.CompileModules.Add(prog.BuiltIns.SystemModule);
foreach (var decl in sortedDecls) {
@@ -2048,7 +2062,7 @@ namespace Microsoft.Dafny foreach (var p in e.TypeArgumentSubstitutions) {
if (!IsDetermined(p.Value.Normalize())) {
Error(e.tok, "type variable '{0}' in the function call to '{1}' could not be determined{2}", p.Key.Name, e.Name,
- (e.Name.Contains("reveal_") || e.Name.Contains("_FULL"))
+ (e.Name.Contains("reveal_") || e.Name.Contains("_FULL")) //CLEMENT should this be StartsWith and EndsWith?
? ". If you are making an opaque function, make sure that the function can be called."
: ""
);
@@ -8135,7 +8149,7 @@ namespace Microsoft.Dafny Contract.Requires(!expr.WasResolved());
Contract.Requires(opts != null);
Contract.Ensures(Contract.Result<Expression>() == null || args != null);
-
+
if (expr.OptTypeArguments != null) {
foreach (var ty in expr.OptTypeArguments) {
ResolveType(expr.tok, ty, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
@@ -8175,7 +8189,7 @@ namespace Microsoft.Dafny receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass, true);
} else {
if (!scope.AllowInstance) {
- Error(expr.tok, "'this' is not allowed in a 'static' context");
+ Error(expr.tok, "'this' is not allowed in a 'static' context"); //FIXME: Rephrase this
// nevertheless, set "receiver" to a value so we can continue resolution
}
receiver = new ImplicitThisExpr(expr.tok);
|