Skip to content
Merged
Show file tree
Hide file tree
Changes from 4 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
549 changes: 549 additions & 0 deletions Source/DafnyRuntime.Tests/CsRuntimeTest.cs

Large diffs are not rendered by default.

415 changes: 395 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