From 040fd81c5cc6f06296e167b6595baa58c6e6450b Mon Sep 17 00:00:00 2001 From: Sasha Fedchin Date: Wed, 8 Jun 2022 14:38:19 -0700 Subject: [PATCH 1/6] Type Polymorphism --- .../CounterExampleGeneration/DafnyModel.cs | 24 ++++++++--- .../DafnyModelType.cs | 34 ++++++++------- Source/DafnyTestGeneration.Test/Various.cs | 31 +++++++++++++- Source/DafnyTestGeneration/DafnyInfo.cs | 22 ++++++++++ Source/DafnyTestGeneration/TestMethod.cs | 42 +++++++++++++++---- Source/DafnyTestGeneration/Utils.cs | 23 +++++----- 6 files changed, 134 insertions(+), 42 deletions(-) diff --git a/Source/DafnyServer/CounterExampleGeneration/DafnyModel.cs b/Source/DafnyServer/CounterExampleGeneration/DafnyModel.cs index d9a51acbd34..914d05856b3 100644 --- a/Source/DafnyServer/CounterExampleGeneration/DafnyModel.cs +++ b/Source/DafnyServer/CounterExampleGeneration/DafnyModel.cs @@ -3,7 +3,6 @@ using System; using System.Collections.Generic; -using System.Collections.Specialized; using System.Diagnostics.Contracts; using System.IO; using System.Linq; @@ -29,7 +28,7 @@ public class DafnyModel { fChar, fNull, fSetUnion, fSetIntersection, fSetDifference, fSetUnionOne, fSetEmpty, fSeqEmpty, fSeqBuild, fSeqAppend, fSeqDrop, fSeqTake, fSeqUpdate, fSeqCreate, fReal, fU2Real, fBool, fU2Bool, fInt, fU2Int, - fMapDomain, fMapElements, fMapBuild; + fMapDomain, fMapElements, fMapBuild, fIs, fIsBox; private readonly Dictionary arrayLengths = new(); private readonly Dictionary datatypeValues = new(); private readonly Dictionary localValue = new(); @@ -70,6 +69,8 @@ public DafnyModel(Model model) { fMapDomain = model.MkFunc("Map#Domain", 1); fMapElements = model.MkFunc("Map#Elements", 1); fMapBuild = model.MkFunc("Map#Build", 3); + fIs = model.MkFunc("$Is", 2); + fIsBox = model.MkFunc("$IsBox", 2); fBox = model.MkFunc("$Box", 1); fDim = model.MkFunc("FDim", 1); fIndexField = model.MkFunc("IndexField", 1); @@ -292,7 +293,7 @@ private static string GetTrueName(Model.Element element) { /// with the element /// private string GetBoogieType(Model.Element element) { - var typeElement = Model.GetFunc("type").OptEval(element); + var typeElement = fType.OptEval(element); if (typeElement == null) { return null; } @@ -338,7 +339,7 @@ internal DafnyModelType GetDafnyType(Model.Element element) { /// private List GetIsResults(Model.Element element) { List result = new(); - foreach (var tuple in Model.GetFunc("$Is").AppsWithArg(0, element)) { + foreach (var tuple in fIs.AppsWithArg(0, element)) { if (((Model.Boolean)tuple.Result).Value) { result.Add(tuple.Args[1]); } @@ -443,6 +444,14 @@ private DafnyModelType GetDafnyType(Model.Uninterpreted element) { return new DafnyModelType("?"); case var bv when bvTypeRegex.IsMatch(bv): return new DafnyModelType(bv.Substring(0, bv.Length - 4)); + case "BoxType": + var unboxedTypes = fIsBox.AppsWithArg(0, element) + .Where(tuple => ((Model.Boolean)tuple.Result).Value) + .Select(tuple => tuple.Args[1]).ToList(); + if (unboxedTypes.Count == 1) { + return ReconstructType(unboxedTypes[0]); + } + return new DafnyModelType("?"); default: return new DafnyModelType("?"); } @@ -456,7 +465,7 @@ private DafnyModelType ReconstructType(Model.Element typeElement) { return new DafnyModelType("?"); } var fullName = GetTrueName(typeElement); - if (fullName != null && fullName.Length > 7) { + if (fullName != null && fullName.Length > 7 && fullName.Substring(0, 7).Equals("Tclass.")) { return new DafnyModelType(fullName.Substring(7)); } if (fullName is "TInt" or "TReal" or "TChar" or "TBool") { @@ -465,6 +474,9 @@ private DafnyModelType ReconstructType(Model.Element typeElement) { if (fBv.AppWithResult(typeElement) != null) { return new DafnyModelType("bv" + ((Model.Integer)fBv.AppWithResult(typeElement).Args[0]).AsInt()); } + if (fullName != null) { // this means this is a type variable + return new DafnyModelType(fullName); + } var tagElement = fTag.OptEval(typeElement); if (tagElement == null) { return new DafnyModelType("?"); @@ -606,7 +618,7 @@ private string GetUnreservedBoolValue(Model.Element element) { /// any other value of that type in the entire model. /// Reserve that value for given element /// - private string GetUnreservedNumericValue(Model.Element element, Type numericType) { + public string GetUnreservedNumericValue(Model.Element element, Type numericType) { if (reservedValuesMap.TryGetValue(element, out var reservedValue)) { return reservedValue; } diff --git a/Source/DafnyServer/CounterExampleGeneration/DafnyModelType.cs b/Source/DafnyServer/CounterExampleGeneration/DafnyModelType.cs index e657c87f00c..a2f7eba21df 100644 --- a/Source/DafnyServer/CounterExampleGeneration/DafnyModelType.cs +++ b/Source/DafnyServer/CounterExampleGeneration/DafnyModelType.cs @@ -11,7 +11,8 @@ public class DafnyModelType { public readonly string Name; public readonly List TypeArgs; - private static readonly Regex boogieToDafnyTypeRegex = new("(?<=[^_](__)*)_m"); + private static readonly Regex ModuleSeparatorRegex = new("(?<=[^_](__)*)_m"); + private static readonly Regex UnderscoreRemovalRegex = new("__"); public DafnyModelType(string name, IEnumerable typeArgs) { Name = name; @@ -37,20 +38,11 @@ public override string ToString() { /// public DafnyModelType InDafnyFormat() { // The line below converts "_m" used in boogie to separate modules to ".": - var tmp = boogieToDafnyTypeRegex.Replace(Name, "."); + var newName = ModuleSeparatorRegex.Replace(Name, "."); + // strip everything after @, this is done for type variables: + newName = newName.Split("@")[0]; // The code below converts every "__" to "_": - bool removeNextUnderscore = false; - var newName = ""; - foreach (char c in tmp) { - if (c == '_') { - if (!removeNextUnderscore) { - newName += c; - } - removeNextUnderscore = !removeNextUnderscore; - } else { - newName += c; - } - } + newName = UnderscoreRemovalRegex.Replace(newName, "_"); return new(newName, TypeArgs.ConvertAll(type => type.InDafnyFormat())); } @@ -59,6 +51,20 @@ public DafnyModelType GetNonNullable() { return new DafnyModelType(newName, TypeArgs); } + public DafnyModelType ReplaceTypeVariables(string with) { + // Assigns the given value to all type variables + var newName = Name.Contains("$") ? with : Name; + return new(newName, TypeArgs.ConvertAll(type => + type.ReplaceTypeVariables(with))); + } + + public override bool Equals(object other) { + if (other is not DafnyModelType typ) { + return false; + } + return typ.ToString() == ToString(); + } + /// /// Parse a string into a type. /// diff --git a/Source/DafnyTestGeneration.Test/Various.cs b/Source/DafnyTestGeneration.Test/Various.cs index 175babb69d9..e992c3b9c79 100644 --- a/Source/DafnyTestGeneration.Test/Various.cs +++ b/Source/DafnyTestGeneration.Test/Various.cs @@ -248,7 +248,7 @@ method ignoreNonNullableObject(v:Value, b:bool) { Assert.IsTrue(m.DafnyInfo.IsStatic("Module.ignoreNonNullableObject")); Assert.AreEqual(2, m.ArgValues.Count); Assert.AreEqual(1, m.ObjectsToMock.Count); - Assert.AreEqual("Module.Value", m.ObjectsToMock[0].type.Name); + Assert.AreEqual("Module.Value", m.ObjectsToMock[0].type.ToString()); } [TestMethod] @@ -287,6 +287,35 @@ method m(a:int) returns (b:int) Assert.AreEqual(1, stats.Count); // the only line with stats } + [TestMethod] + public async Task TypePolymorphism() { + var source = @" +module Test { + method IsEvenLength(s: seq) returns (isEven: bool) + { + if (|s| % 2 == 0) { + return true; + } else { + return false; + } + } +} +".TrimStart(); + var program = Utils.Parse(source); + DafnyOptions.O.TestGenOptions.TargetMethod = "Test.IsEvenLength"; + DafnyOptions.O.TestGenOptions.SeqLengthLimit = 1; + var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); + Assert.AreEqual(2, methods.Count); + Assert.IsTrue(methods.All(m => m.MethodName == "Test.IsEvenLength")); + Assert.IsTrue(methods.All(m => m.DafnyInfo.IsStatic("Test.IsEvenLength"))); + Assert.IsTrue(methods.All(m => m.ArgValues.Count == 1)); + Assert.IsTrue(methods.All(m => m.ObjectsToMock.Count == 0)); + Assert.IsTrue(methods.All(m => m.NOfTypeParams == 1)); + Assert.IsTrue(methods.Exists(m => m.ArgValues[0] == "[]")); + Assert.IsTrue(methods.Exists(m => + Regex.IsMatch(m.ArgValues[0], "\\[[0-9]+\\]"))); + } + /// /// If this fails, consider amending ProgramModifier.MergeBoogiePrograms /// diff --git a/Source/DafnyTestGeneration/DafnyInfo.cs b/Source/DafnyTestGeneration/DafnyInfo.cs index 828ee350e92..b111f62412c 100644 --- a/Source/DafnyTestGeneration/DafnyInfo.cs +++ b/Source/DafnyTestGeneration/DafnyInfo.cs @@ -55,6 +55,8 @@ private void Visit(TopLevelDecl d) { Visit(moduleDecl); } else if (d is ClassDecl classDecl) { Visit(classDecl); + } else if (d is IndDatatypeDecl datatypeDecl) { + Visit(datatypeDecl); } } @@ -69,6 +71,12 @@ private void Visit(LiteralModuleDecl d) { path.RemoveAt(path.Count - 1); } + private void Visit(IndDatatypeDecl d) { + path.Add(d.Name); + d.Members.ForEach(Visit); + path.RemoveAt(path.Count - 1); + } + private void Visit(ClassDecl d) { if (d.Name == "_default") { insideAClass = false; // methods in _default are considered static @@ -85,6 +93,8 @@ private void Visit(ClassDecl d) { private void Visit(MemberDecl d) { if (d is Method method) { Visit(method); + } else if (d is Function function) { + Visit(function); } } @@ -99,6 +109,18 @@ private void Visit(MemberDecl d) { var returnTypes = m.Outs.Select(arg => arg.Type.ToString()).ToList(); info.returnTypes[methodName] = returnTypes; } + + private new void Visit(Function f) { + var methodName = f.Name; + if (path.Count != 0) { + methodName = $"{string.Join(".", path)}.{methodName}"; + } + if (f.HasStaticKeyword || !insideAClass) { + info.isStatic.Add(methodName); + } + var returnTypes = new List { f.ResultType.ToString() }; + info.returnTypes[methodName] = returnTypes; + } } } } \ No newline at end of file diff --git a/Source/DafnyTestGeneration/TestMethod.cs b/Source/DafnyTestGeneration/TestMethod.cs index 763ab0e6bf4..75899fb401c 100644 --- a/Source/DafnyTestGeneration/TestMethod.cs +++ b/Source/DafnyTestGeneration/TestMethod.cs @@ -1,10 +1,9 @@ -using System; using System.Collections.Generic; -using System.IO; using System.Linq; using System.Text.RegularExpressions; using DafnyServer.CounterexampleGeneration; using Microsoft.Boogie; +using Type = Microsoft.Dafny.Type; namespace DafnyTestGeneration { @@ -24,14 +23,21 @@ public class TestMethod { public readonly string MethodName; // values of the arguments to be passed to the method call public readonly List ArgValues; + // number of type parameters for the method (all will be set to defaultType) + public readonly int NOfTypeParams = 0; + // default type to replace any type variable with + private readonly string defaultType = "int"; + // the DafnyModel that describes the inputs to this test method + private DafnyModel dafnyModel; public TestMethod(DafnyInfo dafnyInfo, string log) { DafnyInfo = dafnyInfo; var typeNames = ExtractPrintedInfo(log, "Types | "); var argumentNames = ExtractPrintedInfo(log, "Impl | "); - var dafnyModel = DafnyModel.ExtractModel(log); + dafnyModel = DafnyModel.ExtractModel(log); MethodName = Utils.GetDafnyMethodName(argumentNames.First()); argumentNames.RemoveAt(0); + NOfTypeParams = typeNames.Count(typeName => typeName == "Ty"); ArgValues = ExtractInputs(dafnyModel.States.First(), argumentNames, typeNames); } @@ -51,6 +57,9 @@ private List ExtractInputs(DafnyModelState state, IReadOnlyList var result = new List(); var vars = state.ExpandedVariableSet(null); for (var i = 0; i < printOutput.Count; i++) { + if (types[i] == "Ty") { + continue; // this means that this parameter is a type variable + } if (printOutput[i] == "") { result.Add(GetDefaultValue(DafnyModelType.FromString(types[i]))); continue; @@ -75,6 +84,11 @@ private List ExtractInputs(DafnyModelState state, IReadOnlyList return result; } + // Returns a new value of the defaultType type (set to int by default) + private string GetADefaultTypeValue(DafnyModelVariable variable) { + return dafnyModel.GetUnreservedNumericValue(variable.Element, Type.Int); + } + /// /// Extract the value of a variable. This can have side-effects on /// assignments, reservedValues, reservedValuesMap, and objectsToMock. @@ -89,7 +103,11 @@ private string ExtractVariable(DafnyModelVariable variable) { } List elements = new(); - switch (variable.Type.Name) { + var variableType = variable.Type.ReplaceTypeVariables(defaultType); + if (variableType.ToString() == defaultType && variableType != variable.Type) { + return GetADefaultTypeValue(variable); + } + switch (variableType.Name) { case "?": return "null"; case "char": @@ -106,7 +124,7 @@ private string ExtractVariable(DafnyModelVariable variable) { for (var i = 0; i < seqVar.GetLength(); i++) { var element = seqVar[i]; if (element == null) { - elements.Add(GetDefaultValue(variable.Type.TypeArgs.First())); + elements.Add(GetDefaultValue(variableType.TypeArgs.First())); continue; } elements.Add(ExtractVariable(element)); @@ -129,10 +147,11 @@ private string ExtractVariable(DafnyModelVariable variable) { return $"map[{string.Join(", ", mappingStrings)}]"; case var arrType when new Regex("^_System.array[0-9]*\\?$").IsMatch(arrType): break; + case var _ when (!variable.Value.StartsWith("(") && variable.Value != "null"): + return "DATATYPES_NOT_SUPPORTED"; default: var varId = $"v{ObjectsToMock.Count}"; - var dafnyType = - new DafnyModelType(variable.Type.GetNonNullable().InDafnyFormat().ToString()); + var dafnyType = variableType.GetNonNullable().InDafnyFormat(); ObjectsToMock.Add(new(varId, dafnyType)); mockedVarId[variable] = varId; foreach (var filedName in variable.children.Keys) { @@ -153,6 +172,7 @@ private string ExtractVariable(DafnyModelVariable variable) { /// an element (e.g. T@U!val!25). /// private string GetDefaultValue(DafnyModelType type) { + type = type.ReplaceTypeVariables(defaultType); var result = type.Name switch { "char" => "\'a\'", "bool" => "false", @@ -229,14 +249,18 @@ private List TestMethodLines() { } // the method call itself: + var typeArguments = ""; + if (NOfTypeParams > 0) { + typeArguments = "<" + string.Join(",", Enumerable.Repeat(defaultType, NOfTypeParams)) + ">"; + } string methodCall; if (DafnyInfo.IsStatic(MethodName)) { - methodCall = $"{MethodName}({string.Join(", ", ArgValues)});"; + methodCall = $"{MethodName}{typeArguments}({string.Join(", ", ArgValues)});"; } else { var receiver = ArgValues[0]; ArgValues.RemoveAt(0); methodCall = $"{receiver}.{MethodName.Split(".").Last()}" + - $"({string.Join(", ", ArgValues)});"; + $"{typeArguments}({string.Join(", ", ArgValues)});"; ArgValues.Insert(0, receiver); } diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs index 7b8a7b3bece..fffe72ea319 100644 --- a/Source/DafnyTestGeneration/Utils.cs +++ b/Source/DafnyTestGeneration/Utils.cs @@ -1,12 +1,7 @@ -using System; using System.Collections.Generic; -using System.IO; using System.Linq; -using System.Text; using DafnyServer.CounterexampleGeneration; -using Microsoft.Boogie; using Microsoft.Dafny; -using Action = System.Action; using Errors = Microsoft.Dafny.Errors; using Parser = Microsoft.Dafny.Parser; using Program = Microsoft.Dafny.Program; @@ -37,15 +32,19 @@ public static class Utils { /// Restore the original name of a Dafny method from its Boogie translation /// public static string GetDafnyMethodName(string boogieName) { + // strip the Impl$$, Call$ or CheckWellFormed$$ prefixes: boogieName = boogieName.Split("$").Last(); + // convert Boogie name to Dafny name: + boogieName = new DafnyModelType(boogieName).InDafnyFormat().Name; + // Get the name of the method: var methodName = boogieName.Split(".").Last(); - var classPath = new DafnyModelType(boogieName - .Substring(0, boogieName.Length - methodName.Length - 1)) - .InDafnyFormat().Name - .Split(".") - .Where(m => m[0] != '_'); - var className = string.Join(".", classPath); - return className.Equals("") ? methodName : $"{className}.{methodName}"; + // Get the fully qualified name of the class\module the method is defined in: + var classPath = boogieName + .Substring(0, boogieName.Length - methodName.Length - 1); + // Merge everything using the dot as a separator: + var fullPath = classPath.Split(".") + .Where(m => m != "" && m[0] != '_').Append(methodName); + return string.Join(".", fullPath); } } } \ No newline at end of file From fc20ef02c514955dea71754b81c5daf893b4ee8f Mon Sep 17 00:00:00 2001 From: Sasha Fedchin Date: Wed, 8 Jun 2022 14:46:34 -0700 Subject: [PATCH 2/6] Updated Release Notes --- RELEASE_NOTES.md | 1 + 1 file changed, 1 insertion(+) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 3667d8faae1..14d6ee05787 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -5,6 +5,7 @@ - feat: Live verification diagnostics for the language server (https://github.com/dafny-lang/dafny/pull/1942) - fix: Prevent the language server from crashing and not responding on resolution or ghost diagnostics errors (https://github.com/dafny-lang/dafny/pull/2080) - fix: Correctly specify the type of the receiver parameter when translating tail-recursive member functions to C# (https://github.com/dafny-lang/dafny/pull/2205) +- fix: Added support for type parameters in automatically generated tests # 3.6.0 From ebdc8e844921a7665e29dc9c5538bcba7a6a8fc8 Mon Sep 17 00:00:00 2001 From: Sasha Fedchin Date: Wed, 8 Jun 2022 14:56:34 -0700 Subject: [PATCH 3/6] Add GetHashCode to DafnyModelType --- .../CounterExampleGeneration/DafnyModelType.cs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Source/DafnyServer/CounterExampleGeneration/DafnyModelType.cs b/Source/DafnyServer/CounterExampleGeneration/DafnyModelType.cs index a2f7eba21df..5c7cd7dc2a9 100644 --- a/Source/DafnyServer/CounterExampleGeneration/DafnyModelType.cs +++ b/Source/DafnyServer/CounterExampleGeneration/DafnyModelType.cs @@ -58,6 +58,14 @@ public DafnyModelType ReplaceTypeVariables(string with) { type.ReplaceTypeVariables(with))); } + public override int GetHashCode() { + int hash = Name.GetHashCode(); + foreach (var typ in TypeArgs) { + hash = 31 * typ.GetHashCode(); + } + return hash; + } + public override bool Equals(object other) { if (other is not DafnyModelType typ) { return false; From 20968798dda2b33141da2917d4213bb2d8e19e01 Mon Sep 17 00:00:00 2001 From: Sasha Fedchin Date: Wed, 8 Jun 2022 15:51:59 -0700 Subject: [PATCH 4/6] Fix DafnyModelType Equality comparison --- .../CounterExampleGeneration/DafnyModelType.cs | 8 +++++--- Source/DafnyTestGeneration/TestMethod.cs | 6 +++--- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/Source/DafnyServer/CounterExampleGeneration/DafnyModelType.cs b/Source/DafnyServer/CounterExampleGeneration/DafnyModelType.cs index 5c7cd7dc2a9..7c7ff374908 100644 --- a/Source/DafnyServer/CounterExampleGeneration/DafnyModelType.cs +++ b/Source/DafnyServer/CounterExampleGeneration/DafnyModelType.cs @@ -51,10 +51,12 @@ public DafnyModelType GetNonNullable() { return new DafnyModelType(newName, TypeArgs); } - public DafnyModelType ReplaceTypeVariables(string with) { + public DafnyModelType ReplaceTypeVariables(DafnyModelType with) { // Assigns the given value to all type variables - var newName = Name.Contains("$") ? with : Name; - return new(newName, TypeArgs.ConvertAll(type => + if (Name.Contains("$")) { + return with; + } + return new(Name, TypeArgs.ConvertAll(type => type.ReplaceTypeVariables(with))); } diff --git a/Source/DafnyTestGeneration/TestMethod.cs b/Source/DafnyTestGeneration/TestMethod.cs index 75899fb401c..cc5cf6e88f7 100644 --- a/Source/DafnyTestGeneration/TestMethod.cs +++ b/Source/DafnyTestGeneration/TestMethod.cs @@ -26,7 +26,7 @@ public class TestMethod { // number of type parameters for the method (all will be set to defaultType) public readonly int NOfTypeParams = 0; // default type to replace any type variable with - private readonly string defaultType = "int"; + private readonly DafnyModelType defaultType = new("int"); // the DafnyModel that describes the inputs to this test method private DafnyModel dafnyModel; @@ -104,7 +104,7 @@ private string ExtractVariable(DafnyModelVariable variable) { List elements = new(); var variableType = variable.Type.ReplaceTypeVariables(defaultType); - if (variableType.ToString() == defaultType && variableType != variable.Type) { + if (variableType.Equals(defaultType) && !variableType.Equals(variable.Type)) { return GetADefaultTypeValue(variable); } switch (variableType.Name) { @@ -251,7 +251,7 @@ private List TestMethodLines() { // the method call itself: var typeArguments = ""; if (NOfTypeParams > 0) { - typeArguments = "<" + string.Join(",", Enumerable.Repeat(defaultType, NOfTypeParams)) + ">"; + typeArguments = "<" + string.Join(",", Enumerable.Repeat(defaultType.ToString(), NOfTypeParams)) + ">"; } string methodCall; if (DafnyInfo.IsStatic(MethodName)) { From 42c274a4d08682350ebc0637c5d756556ae97400 Mon Sep 17 00:00:00 2001 From: Aleksandr Fedchin Date: Fri, 10 Jun 2022 09:24:09 -0700 Subject: [PATCH 5/6] Update RELEASE_NOTES.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Mikaël Mayer --- RELEASE_NOTES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 14d6ee05787..67855ccb7a0 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -5,7 +5,7 @@ - feat: Live verification diagnostics for the language server (https://github.com/dafny-lang/dafny/pull/1942) - fix: Prevent the language server from crashing and not responding on resolution or ghost diagnostics errors (https://github.com/dafny-lang/dafny/pull/2080) - fix: Correctly specify the type of the receiver parameter when translating tail-recursive member functions to C# (https://github.com/dafny-lang/dafny/pull/2205) -- fix: Added support for type parameters in automatically generated tests +- fix: Added support for type parameters in automatically generated tests (https://github.com/dafny-lang/dafny/pull/2227) # 3.6.0 From cc391497a06da1a567fb3471d873b4e66268a2ff Mon Sep 17 00:00:00 2001 From: Sasha Fedchin Date: Fri, 10 Jun 2022 09:31:55 -0700 Subject: [PATCH 6/6] safer method name conversion --- Source/DafnyTestGeneration/Utils.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs index fffe72ea319..a151e2e3f97 100644 --- a/Source/DafnyTestGeneration/Utils.cs +++ b/Source/DafnyTestGeneration/Utils.cs @@ -40,7 +40,7 @@ public static string GetDafnyMethodName(string boogieName) { var methodName = boogieName.Split(".").Last(); // Get the fully qualified name of the class\module the method is defined in: var classPath = boogieName - .Substring(0, boogieName.Length - methodName.Length - 1); + .Substring(0, boogieName.Length - methodName.Length).TrimEnd('.'); // Merge everything using the dot as a separator: var fullPath = classPath.Split(".") .Where(m => m != "" && m[0] != '_').Append(methodName);