diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Translator.cs | 15 | ||||
| -rw-r--r-- | Source/DafnyExtension/DafnyDriver.cs | 3 | ||||
| -rw-r--r-- | Source/DafnyExtension/ProgressMargin.cs | 34 |
3 files changed, 30 insertions, 22 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 7f326ffa..7afb3d9c 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -43,6 +43,7 @@ namespace Microsoft.Dafny { readonly PredefinedDecls predef;
public bool InsertChecksums { get; set; }
+ public string UniqueIdPrefix { get; set; }
internal class PredefinedDecls {
public readonly Bpl.Type RefType;
@@ -2148,7 +2149,7 @@ namespace Microsoft.Dafny { _tmpIEs.Clear();
}
- private static void InsertChecksum(Method m, Bpl.Declaration decl, bool specificationOnly = false)
+ private void InsertChecksum(Method m, Bpl.Declaration decl, bool specificationOnly = false)
{
byte[] data;
using (var writer = new System.IO.StringWriter())
@@ -2169,7 +2170,7 @@ namespace Microsoft.Dafny { InsertChecksum(decl, data);
}
- private static void InsertChecksum(Function f, Bpl.Declaration decl, bool specificationOnly = false)
+ private void InsertChecksum(Function f, Bpl.Declaration decl, bool specificationOnly = false)
{
byte[] data;
using (var writer = new System.IO.StringWriter())
@@ -2190,7 +2191,7 @@ namespace Microsoft.Dafny { InsertChecksum(decl, data);
}
- private static void InsertChecksum(Bpl.Declaration decl, byte[] data)
+ private void InsertChecksum(Bpl.Declaration decl, byte[] data)
{
var md5 = System.Security.Cryptography.MD5.Create();
var hashedData = md5.ComputeHash(data);
@@ -2201,12 +2202,13 @@ namespace Microsoft.Dafny { InsertUniqueIdForImplementation(decl);
}
- public static void InsertUniqueIdForImplementation(Bpl.Declaration decl)
+ public void InsertUniqueIdForImplementation(Bpl.Declaration decl)
{
var impl = decl as Bpl.Implementation;
- if (impl != null && !string.IsNullOrEmpty(impl.tok.filename))
+ var prefix = UniqueIdPrefix ?? impl.tok.filename;
+ if (impl != null && !string.IsNullOrEmpty(prefix))
{
- decl.AddAttribute("id", impl.tok.filename + ":" + impl.Id);
+ decl.AddAttribute("id", prefix + ":" + impl.Id);
}
}
@@ -10204,6 +10206,5 @@ namespace Microsoft.Dafny { return attrs;
}
}
-
}
}
diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs index 2dfc0025..79f49dfb 100644 --- a/Source/DafnyExtension/DafnyDriver.cs +++ b/Source/DafnyExtension/DafnyDriver.cs @@ -191,9 +191,10 @@ namespace DafnyLanguage return Dafny.DafnyOptions.Clo.VerifySnapshots;
}
- public static bool Verify(Dafny.Program dafnyProgram, string requestId, ErrorReporterDelegate er) {
+ public static bool Verify(Dafny.Program dafnyProgram, string uniqueIdPrefix, string requestId, ErrorReporterDelegate er) {
Dafny.Translator translator = new Dafny.Translator();
translator.InsertChecksums = true;
+ translator.UniqueIdPrefix = uniqueIdPrefix;
Bpl.Program boogieProgram = translator.Translate(dafnyProgram);
PipelineOutcome oc = BoogiePipeline(boogieProgram, requestId, er);
diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs index f2ea452e..da1f2084 100644 --- a/Source/DafnyExtension/ProgressMargin.cs +++ b/Source/DafnyExtension/ProgressMargin.cs @@ -230,7 +230,10 @@ namespace DafnyLanguage string requestId = null;
lock (RequestIdToSnapshot)
{
- requestId = (RequestIdToSnapshot.Count + 1).ToString();
+ do
+ {
+ requestId = DateTime.UtcNow.Ticks.ToString();
+ } while (RequestIdToSnapshot.ContainsKey(requestId));
RequestIdToSnapshot[requestId] = snap;
}
@@ -277,7 +280,7 @@ namespace DafnyLanguage verificationDisabled = false;
if (_document != null)
{
- Microsoft.Boogie.ExecutionEngine.Cache.RemoveMatchingKeys(new Regex(string.Format(@"^{0}", Regex.Escape(_document.FilePath))));
+ Microsoft.Boogie.ExecutionEngine.Cache.RemoveMatchingKeys(new Regex(string.Format(@"^{0}", Regex.Escape(GetHashCode().ToString()))));
}
NotifyAboutChangedTags(_buffer.CurrentSnapshot);
}
@@ -295,24 +298,27 @@ namespace DafnyLanguage // Run the verifier
var newErrors = new List<DafnyError>();
- try {
- bool success = DafnyDriver.Verify(program, requestId, errorInfo =>
+ try
+ {
+ bool success = DafnyDriver.Verify(program, GetHashCode().ToString(), requestId, errorInfo =>
{
- ITextSnapshot s = snapshot;
- if (errorInfo.RequestId != null)
+ if (errorInfo.RequestId != null && RequestIdToSnapshot.ContainsKey(errorInfo.RequestId))
{
- Contract.Assert(RequestIdToSnapshot.ContainsKey(errorInfo.RequestId));
- s = RequestIdToSnapshot[errorInfo.RequestId];
- }
- newErrors.Add(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.Msg, s));
- foreach (var aux in errorInfo.Aux) {
- newErrors.Add(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.Msg, s));
+ var s = RequestIdToSnapshot[errorInfo.RequestId];
+ newErrors.Add(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.Msg, s));
+ foreach (var aux in errorInfo.Aux)
+ {
+ newErrors.Add(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.Msg, s));
+ }
}
});
- if (!success) {
+ if (!success)
+ {
newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "verification process error", snapshot));
}
- } catch (Exception e) {
+ }
+ catch (Exception e)
+ {
newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "verification process error: " + e.Message, snapshot));
}
|