Support for Mocking in C# Compiler #1809

Dargones · 2022-02-10T09:46:18Z

UPDATE (Mar 28 2022):

As per the ensuing discussion, the functionality of the {:mock} and {:fresh} attributes has been merged into a single {:synthesize} attribute. Methods annotated with {:synthesize} no longer need to be annotated with {:extern}. The compilation behavior described below no longer requires a special CLI option to be triggered. Finally, the compiler will now throw an error if a stubbed method includes any post-conditions, which should guard against a use of the {:synthesize} attribute that might introduce unsoundness.

ORIGINAL PR DESCRIPTION:

This PR adds mocking support to the C# compiler. The idea is to have a special annotation for external methods that makes the compiler translate a postcondition to a series of API calls in C#'s Moq library (provided the /compileMocks command-line argument is also supplied). As an example, consider the following Dafny code, which tests the static method getOrDefault of class StringMap by mocking a StringMap object and stubbing its two instance methods. Using this approach, one is able to test the implementation of getOrDefault without specifying how one would add elements to the map.

class StringMap {

	var m:map<string, string>;

	function method Contains(key:string):bool reads this {
		key in m
	}

	function method Get(key:string):string reads this
		requires Contains(key)
	{
		m[key]
	}

	static function method GetOrDefault(m:StringMap, key:string, default:string):string reads m
	{
		if m.Contains(key) then m.Get(key) else default
	}
}

method {:extern} {:mock} MockStringMap(k:string, v:string) 
	returns (m:StringMap)
	ensures m.Contains(k) == true && m.Get(k) == v
	ensures fresh(m)

method {:test} PassingTestGetOrDefault() {
	var stringMap := MockStringMap("a", "b");
	assert StringMap.GetOrDefault(stringMap, "a", "c") == "b";
	expect StringMap.GetOrDefault(stringMap, "a", "c") == "b";
}

The mockStringMap method is automatically translated to the following in C#, allowing a runtime test that would otherwise be impossible without fully implementing the StringMap class:

public static StringMap mockStringMap(Dafny.ISequence<char> k, Dafny.ISequence<char> v) {
    var mTmp = new Mock<StringMap>();
    mTmp.Setup(x => x.contains(k)).Returns(true);
    mTmp.Setup(x => x.get(k)).Returns(v);
    return mTmp.Object;
}

Only functions can be mocked - methods can have side effects and are, therefore, not allowed in postconditions. Not all Dafny postconditions can be translated to calls in Moq either - compiling an arbitrary postcondition would be a full-blown synthesis problem and, while intersting from a research perspective, it would probably not be fast enough for a compiler. Here is the grammar for postconditions that are supported (S is the start symbol, EXP stands for an arbitrary Dafny expression, and ID stands for variable/method/type identifiers):

S       = FORALL 
        | EQUALS 
        | S && S
EQUALS  = ID.ID (ARGLIST) == EXP // stubs a method call
        | ID.ID            == EXP // stubs field access
        | EQUALS && EQUALS
FORALL  = forall SKOLEMS :: EXP ==> EQUALS
ARGLIST = ID // this can be one of the skolem variables
        | EXP // this exp may not reference any of the skolems 
        | ARGLIST, ARGLIST
SKOLEMS = ID : ID 
        | SKOLEMS, SKOLEMS

The compiler throws a NotImplementedException if postconditions on the mocked method do not follow this grammar. Support for mocking could be easily extended to Java and other target languages (and I am happy to work on this). Here is a design document that outlines the overall idea of a testing framework and of how one would do this in Java.

An additional feature that this PR introduces is the {:fresh} annotation that prompts the compiler to translate an external method to one that returns a fresh instance of an object. This could be useful in situations where inferring the right parameters to a constructor is difficult. So, for instance, an automatic test generation framework could use this to get a fresh instance of an object to then assign its fields as needed. This is the feature that was previously the topic of this PR.

Finally, this PR also fixes a small issue with the {:test} annotation - currently, the C# compiler only calls IsFailure on the first returned value of a testing method if there are more than one (should be more than zero) returned value (this is the line with the bug)

…TODO

… into testFrameworkCSharp

Dargones · 2022-02-10T19:43:50Z

Added a small fix that allows mocked objects to cross-reference each other (the problem was that C#'s out parameters cannot appear in lambda expressions)

robin-aws · 2022-02-11T21:32:18Z

Very exciting! As per our chat I think the general approach seems good and at least viable for other target languages, although I'm sure I'll have suggestions when I have time to review it properly.

FYI here's a good issue to track the mostly orthogonal concern we discussed, about catching when a mock's specification is actually unsatisfiable: #1767

keyboardDrummer · 2022-02-14T09:43:51Z

Source/Dafny/Compilers/Compiler-Csharp.cs

+          this.predicate = predicate;
+          this.nArgs = nArgs;
+          currArgs = new object[nArgs];
+          for (int i = 0; i < currArgs.Length; i++) {


null is the default value of the elements in new object[nArgs], so I think you can skip the for.

Thank you! Have fixed this in the following commit.

keyboardDrummer · 2022-02-14T09:45:57Z

Source/Dafny/Compilers/Compiler-Csharp.cs

+        private readonly object[] currArgs;
+        private int nextArgId;
+
+        public MultiMatcher(int nArgs, Func<object[], bool> predicate) {


I would rename nArgs to argumentCount.

keyboardDrummer · 2022-02-14T09:46:39Z

Source/Dafny/Compilers/Compiler-Csharp.cs

+    ///                    It.Is<int>(b => matcher.Match(b)))).Returns(4);
+    /// 
+    /// </summary>
+    private static void AddMultiMatcher(ConcreteSyntaxTree wr) {


Please rename wr to dafnyNamespace.

keyboardDrummer · 2022-02-14T09:49:30Z

Source/Dafny/Compilers/Compiler-Csharp.cs

+
+        private readonly Func<object[], bool> predicate;
+        private readonly int nArgs;
+        private readonly object[] currArgs;


I recommend you use a List<object> since it has the nextArgId field built into it through the Count field.

I would rename currArgs to collectedArguments

keyboardDrummer · 2022-02-14T09:58:05Z

Source/Dafny/Compilers/Compiler-Csharp.cs

@@ -1636,13 +1701,21 @@ protected class ClassWriter : IClassWriter {
        }
        cw.StaticMemberWriter.WriteLine(";");
      } else if (cw.CtorBodyWriter == null) {
-        cw.InstanceMemberWriter.Write($"{publik}{konst} {typeName} {name}");
+        if (isPublic && !isConst) {
+          cw.InstanceMemberWriter.Write($"{publik}{konst} virtual {typeName} {name} {{get; set;}}");


I'm guessing the addition of virtual causes a performance degradation of the C# code, please only do this if mocking is turned on.

I now only add virtual if DafnyOptions.O.CompileMocks is set to true.

keyboardDrummer · 2022-02-14T10:45:28Z

Source/Dafny/Compilers/Compiler-Csharp.cs

+          return predicate(currArgs);
+        }
+      }";
+      wr.WriteLine(multiMatcher);


I think only the first line of MultiMatcher will be indented while the rest won't be intended at all. Look at the definition of ConcreteSyntaxTree.Write and LineSegment.Render.

However, I think you don't have to fix this. I think it would be better if we generate a C# AST which then later gets printed with formatting, so we can accept incorrect formatting until we do that.

One option would be to generate a Roslyn C# AST using the Roslyn API, by in this case doing something like SyntaxFactory.ParseMemberDeclaration(multiMatcher) which returns the AST node that later gets formatted automatically.

It seems that the indentation is still preserved but I wrapped the code around SyntaxFactory.ParseMemberDeclaration to be certain. Let me know if there is anything else I should do in this respect!

Sorry, I misspoke. What I meant was that the indentation of the dafnyNamespace node is lost except for on the first line class MultiMatcher {. So you could get something like:

class MultiMatcher { private readonly Func<object[], bool> predicate; private readonly int argumentCount; private readonly List<object> collectedArguments; public MultiMatcher(int argumentCount, Func<object[], bool> predicate) { this.predicate = predicate; this.argumentCount = argumentCount; collectedArguments = new(); } public bool Match(object argument) { collectedArguments.Add(argument); if (collectedArguments.Count != argumentCount) { return true; } bool result = predicate(collectedArguments.ToArray()); collectedArguments.Clear(); return result; } }

keyboardDrummer · 2022-02-14T10:49:45Z

Source/Dafny/Compilers/Compiler-Csharp.cs

@@ -146,6 +199,7 @@ public CsharpCompiler(ErrorReporter reporter)

    private void EmitInitNewArrays(BuiltIns builtIns, ConcreteSyntaxTree wr) {
      var dafnyNamespace = CreateModule("Dafny", false, false, null, wr);
+      AddMultiMatcher(dafnyNamespace);


The name EmitInitNewArrays doesn't match this content. Consider moving the two statements

var dafnyNamespace = CreateModule("Dafny", false, false, null, wr); AddMultiMatcher(dafnyNamespace);

out of EmitInitNewArrays and passing dafnyNamespace to EmitInitNewArrays

Done! I also moved AddMultiMatcher, now renamed EmitMultiMatcher, to the CsharpMockWriter class.

keyboardDrummer · 2022-02-14T10:51:24Z

Source/Dafny/Compilers/Compiler-Csharp.cs

+
+      private readonly CsharpCompiler compiler;
+      // maps identifier names to the names of corresponding mocks:
+      private Dictionary<string, string> mockNames = new();


Consider renaming this to methodNameToMockName

Renamed to objectToMockName

keyboardDrummer · 2022-02-14T10:53:43Z

Source/Dafny/Compilers/Compiler-Csharp.cs

+      /// <summary>
+      /// Create a body of a method that mocks one or more objects
+      /// </summary>
+      public ConcreteSyntaxTree CreateMockMethod(Method m,


Can you write a full example of a Mock method in the documentation of CreateMockMethod ?

Added an example from the testing suite.

keyboardDrummer · 2022-02-14T10:57:27Z

Source/Dafny/Compilers/Compiler-Csharp.cs

+        wr.FormatLine($"{keywords}{returnType} {compiler.IdName(m)}{typeParameters}({parameterString}) {{");
+
+        // Initialize the mocks:
+        mockNames = new Dictionary<string, string>();


Consider writing

mockNames = m.Outs.ToDictionary(o => o.CompileName, o => compiler.idGenerator.FreshId(o.CompileName + "Mock")); foreach(var (methodName, mockName) in mockNames) { wr.FormatLine($"var {mockName} = new Mock<{compiler.TypeName(o.Type, wr, o.tok)}>();"); wr.FormatLine($"var {methodName} = {mockName}.Object;"); }

to separate the two concerns.

Consider doing something similar for the initialization of retNames.

keyboardDrummer

Looks great, thanks!

robin-aws

I mainly focussed on the API of this feature from an end-user POV, and made some suggestions that hopefully won't change the actual implementation very much.

One other top-level suggestion: as you mention, this style of mocking really is a form of synthesis, and it's entirely possible other target languages will want to implement this with more code generation and not rely on any mocking libraries. The term "mock" has a fairly specific meaning in testing libraries and given the current limitations of the implementation this feels more like "stubs" instead. I would consider naming the attribute something more generic, and allowing the Dafny code that uses it to label it based on usage instead.

robin-aws · 2022-02-22T17:34:53Z

Test/DafnyTests/TestAttribute.dfy

+    expect(e.IsValid());
+}
+
+method {:extern} {:mock} MockValidEven() returns (e:Even) 


I don't think we should require the {:extern} attribute on mock specifications as well, since there's no existing external code being linked in here. {:mock} is a way of saying you want the implementation synthesized instead, and I don't think it's hugely different from any other "external" code the compilers emit. :)

I can appreciate that requiring it is easier, since it avoids any errors about missing bodies. But we should be able to have {:mock} disable those errors as well.

Done! You no longer have to add the :extern attribute on methods annotated with :mock (now called :synthesize).

robin-aws · 2022-02-22T17:41:15Z

Source/Dafny/DafnyOptions.cs

+/compileMocks 
+    If true, automatically compile external methods annotated with {{:mock}}
+    into the target language (currently only supported for C#)


Thank you for adding documentation for the option! :) Do we really need the option though? Are we just worried about existing code that has that attribute for some reason? That seems extremely unlikely to me.

I also think we should move some of the documentation you wrote in the PR description into the PR itself, probably in the reference manual. The meaning and current limitations of the feature is definitely non-trivial, and we'll want to communicate them for Dafny users and not just Dafny contributors.

I have updated Attributes.md in the Reference Manual with a brief description of the :synthesize attribute (I renamed :mock to this).

My reasoning behind adding a command line option (now also renamed to :synthesize) is that synthesizing mocks is only possible with the Moq library, which we probably shouldn't require by default since it is not part of C#'s standard library. This command-line option would tell the compiler that it is OK to include Moq.

Alternatively, one can traverse the program's AST and only try to import Moq if there is a method annotated with :mock. The problem with this approach is that most of the compiler code is agnostic to the program currently being compiled. This would mean that I would have to compile all fields as virtual (necessary for using Moq) even if no mocking is actually performed because I don't know which program I am compiling at the moment. @keyboardDrummer previously mentioned that doing so might slow done the resuling binary, so I went for the command-line-argument approach. But I do have both approaches implemented locally, so I can easily make the change. Let me know if I should redo this one way or the other!

robin-aws · 2022-02-22T17:45:53Z

Test/DafnyTests/TestAttribute.dfy

+    }
+}
+
+method {:extern} {:fresh} freshEven() returns (e:Even) ensures fresh(e)


Could you get the same effect here by using {:mock} instead of {:fresh}, since the ensures clause is already expressing the requirement? I'm hoping we could get away with just the one new {:mock} feature. I understand that the implementation is currently different (instantiating a "real" compiled object instead of a mock) but is that difference actually observable to end users? I see below that you are able to set fields on mock objects as well.

I didn't realize one can do this before, but I was able to merge these two cases! From now on, a mocked object behaves exactly as the real object in all cases except for when a function call or field is explicitly stubbed.

robin-aws · 2022-02-22T17:59:40Z

Test/DafnyTests/TestAttribute.dfy

+method {:extern} {:mock} MockSumWithArgumentMatcher() returns (e:Even) 
+    ensures fresh(e) 
+    ensures forall a:int, b:int :: (b < a) ==> (e.Sum(a, b) == a * b)
+    ensures forall a:int, b:int :: (b >= a) ==> (e.Sum(a, b) == -a * b)


So technically this example is valid since Sum is drastically underspecified. :) But I'm troubled by the fact that you could use this feature to create a mock that violates the specification of the type you're mocking, and therefore make unsound tests that don't actually support true properties of the codebase.

I propose that the post-conditions for each function on a mock should be conjuncted with the post-conditions of the original function, so that you can't violate the latter. That will clearly sometimes result in expressions that don't fit into the grammar of supported expressions, but that's just fine and safer than introducing this kind of unsoundness.

I'm not sure forcing the mock to obey the original post-conditions is consistent with what we want the mocks to be able to do.

Mocks are not intended to be implementations of the original methods; rather, they provide some limited behavior, usually inconsistent with the original method behavior, to achieve some testing goal.

In other words, when using a mock, the goal is not to understand whether or not the original object is able to behave in a specific way in a complex context; rather, the goal is to generate test inputs to exercise a particular aspect of the code under test. Whether or not that input is feasible, although an interesting question, is orthogonal to the concern of testing the path.

Might we include a switch to enable or disable the addition of the original contract for the mocked method?

Thanks for the helpful discussion on this yesterday! I still believe that using a mock to drive code to behave in a way that is impossible otherwise is questionable (such as reaching a statement that is otherwise unreachable), but I can appreciate that there is at least some use for this for debugging.

Therefore I am adequately mollified if we add a switch for including the original contract, AND we make it on by default, with a warning in the documentation that turning it off can lead to unsound results.

As per the discussion on Slack, I have made it so that Dafny spits an error message if a stubbed method includes any post-postconditions (or if the code tries to mock an object's field) - see the updated test files for an example.

… into testFrameworkCSharp

Dargones · 2022-03-08T14:50:15Z

Thank you, @robin-aws, for all your feedback! I changed "mock" to "synthesize" to make the attribute name more generic and have made other changes you suggest above. Let me know if there is anything else you would like me to change!

robin-aws

Great changes, I'm super happy we were able to simplify the surface area of the feature! Just some relatively minor points to address.

Can you add a bullet point to RELEASE_NOTES.md for this feature too?

docs/DafnyRef/Attributes.md

robin-aws · 2022-03-16T22:11:27Z

Source/Dafny/Compilers/Compiler-Csharp.cs

-          cw.CtorBodyWriter.WriteLine($"this.{name} = {rhs};");
+        string ending = "";
+        if (isPublic) {
+          cw.InstanceMemberWriter.Write($"{publik} {virtuall} {typeName} {name} {{get; set;}}");


It looks like you're ignoring konst here and emitting a setter even if isConst is true. Is that intentional?

I borrowed this from @keyboardDrummer's proposed solution, which does seem to emit the setter regardless. In my latest commit I have changed the code so that it only emits it if isConst is false, as below. Would this approach make sense?

if (isPublic) { if (isConst) { cw.InstanceMemberWriter.Write($"{publik}{konst} {virtuall} {typeName} {name} {{get;}}"); } else { cw.InstanceMemberWriter.Write($"{publik} {virtuall} {typeName} {name} {{get; set;}}"); } } else { cw.InstanceMemberWriter.WriteLine($"{publik}{konst} {typeName} {name}"); ending = ";"; }

robin-aws · 2022-03-16T22:13:32Z

Source/Dafny/Compilers/Compiler.cs

@@ -1273,6 +1275,15 @@ protected class NullClassWriter : IClassWriter {
      public ConcreteSyntaxTree/*?*/ CreateMethod(Method m, List<TypeArgumentInstantiation> typeArgs, bool createBody, bool forBodyInheritance, bool lookasideBody) {
        return createBody ? block : null;
      }
+
+      public ConcreteSyntaxTree CreateFreshMethod(Method m) {


I think this is leftover from earlier revisions and can be deleted.

robin-aws · 2022-03-16T22:14:17Z

Source/Dafny/Compilers/Compiler.cs

+              classWriter.SynthesizeMethod(m, CombineAllTypeArguments(m), true, true, false);
+            } else {
+              Error(m.tok, "Method {0} is annotated with :synthesize but " +
+                           "does not have the correct specification or has a " +


Can you be more specific about what "the correct specification" is (i.e. static and returning at least one value) in the error message?

Changed to "...is not static, has a body, or does not return anything"

Source/Dafny/Compilers/Synthesizer-Csharp.cs

Source/Dafny/Verifier/Translator.ExpressionTranslator.cs

robin-aws · 2022-03-16T22:20:06Z

Test/DafnyTests/TestAttribute.dfy

+
+class StringMap {
+
+	var m:map<string, string>;


nit: the indentation on this file is all over the place. :) We've generally settled on a two-space indent.

Have changed everything to two-space indent.

robin-aws · 2022-03-16T22:22:13Z

Test/DafnyTests/TestAttribute.dfy

 // Remove the timestamp prefixes on the expected errors
 // RUN: sed 's/[^]]*\]//' "%t".testresults.raw >> "%t"


Off-topic, but I just realized this post-processing can be replaced with OutputCheck-style // CHECK: directives now that I've added that support to the xUnit lit test runner :)

Thank you! Have switched to using the //CHECK: directive

robin-aws · 2022-03-16T22:29:43Z

Source/Dafny/DafnyOptions.cs

+/synthesize 
+    If true, synthesizes bodies of methods annotated with  {{:synthesize}}
+    during compilation (currently only supported for C#)


My reasoning behind adding a command line option (now also renamed to :synthesize) is that synthesizing mocks is only possible with the Moq library, which we probably shouldn't require by default since it is not part of C#'s standard library. This command-line option would tell the compiler that it is OK to include Moq.

Alternatively, one can traverse the program's AST and only try to import Moq if there is a method annotated with :mock. The problem with this approach is that most of the compiler code is agnostic to the program currently being compiled. This would mean that I would have to compile all fields as virtual (necessary for using Moq) even if no mocking is actually performed because I don't know which program I am compiling at the moment. @keyboardDrummer previously mentioned that doing so might slow done the resuling binary, so I went for the command-line-argument approach. But I do have both approaches implemented locally, so I can easily make the change. Let me know if I should redo this one way or the other!

Okay - I would still prefer not to have the extra option, but the point about virtual fields being a potential performance hit is the most valid reason to keep it. If it's feasible to instead scan ahead for any {:synthesize} attributes and only then make fields virtual and add the using declaration, that would be great, but it's not a hard requirement.

I now scan the AST for {:synthesize} attribute instead of relying on the command line argument as a result. The result of the scan is stored in an instance variable that the compiler checks whenever it makes a decision about making fields virtual. A possible downside of this approach is potential issues when trying to parallelize compilation of multiple programs using a single compiler object (is such a situation likely?). In any case, this is my final commit at the moment so I can easily revert it back to the command-line-argument approach if needed!

You're already ahead of the game by not using a global variable, so I'm totally fine with a compiler instance variable. :)

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>

Dargones · 2022-03-20T09:48:41Z

Thank you, @robin-aws! I have added the feature to RELAEASE_NOTES.md and made all the other changes you have suggested. Update: I am failing one test but it appears to be a random failure because I was passing that same test before applying dotnet-format

robin-aws

Looks great! Thanks for all the improvements on this.

One last ask for @Dargones: can you update the PR description to reflect the fact that we ended up dropping the CLI option and the {:fresh} attribute? We'll use that content as the commit description when we merge and squash, and I wasn't 100% sure how you'd like to update it.

Dargones · 2022-03-28T19:44:46Z

Thank you, @robin-aws! I updated the PR description by adding a paragraph at the top that summarizes all the key differences with the original version.

Dargones added 24 commits October 21, 2021 01:20

Mocking for {:test} attribute

aa1cdcb

Fix accidental change

7ab10f0

A different test and a fix

c307c4e

fix(semanticCommit): learning new things every day also removed that …

4300897

…TODO

fix: making the pr semantic

a3405f7

Merge branch 'dafny-lang:master' into counterexamples

a832b13

Mocks using extern

b6e2df4

Dummy commit

f61a3a3

Merge branch 'dafny-lang:master' into testFrameworkCSharp

9648bb6

Mocking First Steps

9d69721

Basic Argument Matching

58c47ba

Mock Fields

c9fab47

MockWriter class

bf8ab5f

Merge branch 'dafny-lang:master' into testFrameworkCSharp

6f5c75b

Improve Readability

2237bd3

Merge branch 'testFrameworkCSharp' of https://github.com/Dargones/dafny…

e96574e

… into testFrameworkCSharp

Merge branch 'dafny-lang:master' into testFrameworkCSharp

dbe04a0

Compiler style changes

1b20628

Merge branch 'testFrameworkCSharp' of https://github.com/Dargones/dafny…

67bb487

… into testFrameworkCSharp

More tests

d643d70

Unique Identifiers

1eddfc7

Arbitrary Argument Order

e812b43

More detailed documentation

5f4aa99

compileMocks attribute

28df976

robin-aws self-requested a review February 10, 2022 18:30

CrossReferencing

1af8f55

keyboardDrummer reviewed Feb 14, 2022

View reviewed changes

Performance and code style

5ea83e0

keyboardDrummer previously approved these changes Feb 21, 2022

View reviewed changes

Merge branch 'master' into testFrameworkCSharp

52dcf8e

robin-aws requested changes Feb 22, 2022

View reviewed changes

Dargones added 4 commits March 8, 2022 08:43

Functional changes

e87a103

Rename mock to synthesize

db6d3a8

More renaming

f99c77d

Merge branch 'testFrameworkCSharp' of https://github.com/Dargones/dafny…

51c2d28

… into testFrameworkCSharp

Dargones dismissed keyboardDrummer’s stale review via 51c2d28 March 8, 2022 14:14

Inlcude Lists

d01a357

Merge branch 'dafny-lang:master' into testFrameworkCSharp

68a7a86

robin-aws requested changes Mar 16, 2022

View reviewed changes

Dargones and others added 6 commits March 20, 2022 02:38

Rename mock to synthesize in docs

5be5a55

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>

Update comments for Synthesizer-Csharp.cs

3a7f1b5

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>

Proposed changes

d3e2fa5

Merge changes from main repo

432defb

Use CHECK directive

1f2fb41

Scan AST for synthesize attribute

d793691

Dargones and others added 3 commits March 20, 2022 06:45

dotnet-format

dfca43c

dummy commit

70d2b92

Remove unintentional file add

6c87875

robin-aws approved these changes Mar 28, 2022

View reviewed changes

Merge branch 'master' into testFrameworkCSharp

42a86ce

Merge branch 'master' into testFrameworkCSharp

be37e48

robin-aws enabled auto-merge (squash) March 28, 2022 20:20

robin-aws merged commit c89b039 into dafny-lang:master Mar 28, 2022

Dargones mentioned this pull request Apr 30, 2022

fix: mocking objects in Dafny tests #1526

Closed

tbean79 mentioned this pull request Jun 27, 2022

Add support for Java mocking #2024

Open

		// Remove the timestamp prefixes on the expected errors
		// RUN: sed 's/[^]]*\]//' "%t".testresults.raw >> "%t"

Support for Mocking in C# Compiler #1809

Support for Mocking in C# Compiler #1809

Conversation

Dargones commented Feb 10, 2022 • edited Loading

UPDATE (Mar 28 2022):

ORIGINAL PR DESCRIPTION:

Dargones commented Feb 10, 2022

robin-aws commented Feb 11, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Feb 21, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Dargones Feb 17, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer left a comment

Choose a reason for hiding this comment

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ericmercer Feb 24, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Dargones commented Mar 8, 2022

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Dargones Mar 20, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Dargones Mar 20, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Dargones commented Mar 20, 2022 • edited Loading

robin-aws left a comment • edited Loading

Choose a reason for hiding this comment

Dargones commented Mar 28, 2022

Dargones commented Feb 10, 2022 •

edited

Loading

keyboardDrummer Feb 21, 2022 •

edited

Loading

Dargones Feb 17, 2022 •

edited

Loading

ericmercer Feb 24, 2022 •

edited

Loading

Dargones Mar 20, 2022 •

edited

Loading

Dargones Mar 20, 2022 •

edited

Loading

Dargones commented Mar 20, 2022 •

edited

Loading

robin-aws left a comment •

edited

Loading