Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Source/DafnyCore/Backends/BoogieExtractor.cs
Original file line number Diff line number Diff line change
Expand Up @@ -187,7 +187,7 @@ public override void VisitMethod(Method method) {
}

private QKeyValue? GetKeyValues(IToken tok, Attributes attributes) {
Boogie.QKeyValue kv = null;
QKeyValue? kv = null;
var extractAttributes = Attributes.FindAllExpressions(attributes, AttributeAttribute);
if (extractAttributes != null) {
if (extractAttributes.Count == 0) {
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyDriver/Commands/VerifyCommand.cs
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,7 @@ public static async Task<int> HandleVerification(DafnyOptions options) {
var extractedProgram = BoogieExtractor.Extract(resolution.ResolvedProgram);
engine.PrintBplFile(options.BoogieExtractionTargetFile, extractedProgram, true, pretty: true);
} catch (ExtractorError extractorError) {
options.OutputWriter.WriteLine($"Boogie axiom extraction error: {extractorError.Message}");
await options.OutputWriter.WriteLineAsync($"Boogie axiom extraction error: {extractorError.Message}");
return 1;
}
}
Expand Down
551 changes: 551 additions & 0 deletions Source/DafnyRuntime.Tests/CsRuntimeTest.cs

Large diffs are not rendered by default.

416 changes: 396 additions & 20 deletions Source/DafnyRuntime.Tests/TupleTest.cs

Large diffs are not rendered by default.

2 changes: 2 additions & 0 deletions Source/DafnyRuntime/AssemblyInfo.cs
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
using System.Runtime.CompilerServices;
[assembly: InternalsVisibleTo("DafnyRuntime.Tests")]
6 changes: 3 additions & 3 deletions Source/DafnyRuntime/DafnyRuntime.cs
Original file line number Diff line number Diff line change
Expand Up @@ -1280,8 +1280,8 @@ public override int Count {
internal class ConcatSequence<T> : Sequence<T> {
// INVARIANT: Either left != null, right != null, and elmts's underlying array == null or
// left == null, right == null, and elmts's underlying array != null
private volatile ISequence<T> left, right;
private ImmutableArray<T> elmts;
internal volatile ISequence<T> left, right;
internal ImmutableArray<T> elmts;
private readonly int count;

internal ConcatSequence(ISequence<T> left, ISequence<T> right) {
Expand Down Expand Up @@ -1311,7 +1311,7 @@ public override int Count {
}
}

private ImmutableArray<T> ComputeElements() {
internal ImmutableArray<T> ComputeElements() {
// Traverse the tree formed by all descendants which are ConcatSequences
var ansBuilder = ImmutableArray.CreateBuilder<T>(count);
var toVisit = new Stack<ISequence<T>>();
Expand Down
4 changes: 3 additions & 1 deletion Source/DafnyRuntime/DafnyRuntime.csproj
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,9 @@
<ItemGroup>
<Folder Include="DafnyRuntimeJava\build\libs" />
</ItemGroup>

<ItemGroup>
<InternalsVisibleTo Include="$(MSBuildProjectName).Tests" />
</ItemGroup>
<ItemGroup>
<Content Update="DafnyRuntimeGo-gomod\dafny\dafny.go">
<CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
Expand Down
Loading