From 5e601ff97aadee43fe2d2bc2a4a6538b07656287 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 5 Jan 2024 16:12:19 +0100 Subject: [PATCH] Update textual references to compilation target --- .../BenchmarkInstrumentation.cs | 2 +- Source/DafnyCore/Feature.cs | 2 +- Source/DafnyCore/Resolver/ModuleResolver.cs | 2 +- .../benchmarks/sequence-race/SequenceRace.dfy | 2 +- .../benchmarks/sequence-race/SequenceRace.dfy.expect | 2 +- .../LitTests/LitTest/comp/CoverageReport.dfy.expect | 12 ++++++------ .../LitTests/LitTest/comp/NativeNumbers.dfy.js.check | 2 +- .../LitTest/dafny0/NativeTypeResolution.dfy.expect | 4 ++-- .../LitTests/LitTest/dafny0/RuntimeTypeTests0.dfy | 2 +- .../ConsistentWhenSupported.dfy.oldway.expect | 4 ++-- .../unicodechars/comp/NativeNumbers.dfy.js.check | 2 +- Source/TestDafny/MultiBackendTest.cs | 2 +- docs/HowToFAQ/Errors-CommandLine.md | 2 +- docs/HowToFAQ/FAQNewtype.md | 2 +- docs/HowToFAQ/onepage.md | 2 +- 15 files changed, 22 insertions(+), 22 deletions(-) diff --git a/Source/DafnyBenchmarkingPlugin/BenchmarkInstrumentation.cs b/Source/DafnyBenchmarkingPlugin/BenchmarkInstrumentation.cs index 9a8291c09f..a69a8c48bd 100644 --- a/Source/DafnyBenchmarkingPlugin/BenchmarkInstrumentation.cs +++ b/Source/DafnyBenchmarkingPlugin/BenchmarkInstrumentation.cs @@ -11,7 +11,7 @@ public override void Instrument(IExecutableBackend backend, SinglePassCodeGenera javaCompiler.AddInstrumenter(new JavaBenchmarkCompilationInstrumenter(Reporter)); } else { Reporter.Error(MessageSource.Compiler, ResolutionErrors.ErrorId.none, program.GetStartOfFirstFileToken(), - $"The benchmarking plugin does not support this compilation target: {codeGenerator} (--target:{backend.TargetId})"); + $"The benchmarking plugin does not support this translation target: {codeGenerator} (--target:{backend.TargetId})"); } } } \ No newline at end of file diff --git a/Source/DafnyCore/Feature.cs b/Source/DafnyCore/Feature.cs index 82958d87c8..7b3f4e471d 100644 --- a/Source/DafnyCore/Feature.cs +++ b/Source/DafnyCore/Feature.cs @@ -193,7 +193,7 @@ and where at least one variable has potentially infinite bounds. public class UnsupportedFeatureException : Exception { public const string MessagePrefix = - "Feature not supported for this compilation target: "; + "Feature not supported for this translation target: "; public readonly IToken Token; public readonly Feature Feature; diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index b697df8ac0..a2b882524e 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -2212,7 +2212,7 @@ void UpdateBounds(BigInteger? lo, BigInteger? hi) { } } else if (nativeTypeChoices != null) { reporter.Error(MessageSource.Resolver, dd, - "None of the types given in :nativeType arguments is supported by the current compilation target. Try supplying others."); + "None of the types given in :nativeType arguments is supported by the current translation target. Try supplying others."); } else if (mustUseNativeType) { reporter.Error(MessageSource.Resolver, dd, "Dafny's heuristics cannot find a compatible native type. " + diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/benchmarks/sequence-race/SequenceRace.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/benchmarks/sequence-race/SequenceRace.dfy index 29e449ccce..48b97c0429 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/benchmarks/sequence-race/SequenceRace.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/benchmarks/sequence-race/SequenceRace.dfy @@ -1,7 +1,7 @@ // Only because we're calling gradlew rather than gradlew.bat // UNSUPPORTED: windows -// Ensure trying to use an unsupported compilation target results in a clean error message. +// Ensure trying to use an unsupported translation target results in a clean error message. // RUN: %exits-with 3 %baredafny translate cs %args "%s" --plugin:DafnyBenchmarkingPlugin.dll > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/benchmarks/sequence-race/SequenceRace.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/benchmarks/sequence-race/SequenceRace.dfy.expect index 385c4482cf..f81f00bf8a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/benchmarks/sequence-race/SequenceRace.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/benchmarks/sequence-race/SequenceRace.dfy.expect @@ -1,4 +1,4 @@ Dafny program verifier finished with 2 verified, 0 errors -SequenceRace.dfy(35,0): Error: The benchmarking plugin does not support this compilation target: Microsoft.Dafny.Compilers.CsharpCompiler (--target:cs) +SequenceRace.dfy(35,0): Error: The benchmarking plugin does not support this translation target: Microsoft.Dafny.Compilers.CsharpCompiler (--target:cs) Wrote textual form of partial target program to SequenceRace.cs diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy.expect index 050212ee15..6d20e7d2ba 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy.expect @@ -1,18 +1,18 @@ Dafny program verifier finished with 0 verified, 0 errors -CoverageReport.dfy(20,0): Error: Feature not supported for this compilation target: Execution coverage report +CoverageReport.dfy(20,0): Error: Feature not supported for this translation target: Execution coverage report Dafny program verifier finished with 0 verified, 0 errors -CoverageReport.dfy(20,0): Error: Feature not supported for this compilation target: Execution coverage report +CoverageReport.dfy(20,0): Error: Feature not supported for this translation target: Execution coverage report Dafny program verifier finished with 0 verified, 0 errors -CoverageReport.dfy(20,0): Error: Feature not supported for this compilation target: Execution coverage report +CoverageReport.dfy(20,0): Error: Feature not supported for this translation target: Execution coverage report Dafny program verifier finished with 0 verified, 0 errors -CoverageReport.dfy(20,0): Error: Feature not supported for this compilation target: Execution coverage report +CoverageReport.dfy(20,0): Error: Feature not supported for this translation target: Execution coverage report Dafny program verifier finished with 0 verified, 0 errors -CoverageReport.dfy(20,0): Error: Feature not supported for this compilation target: Execution coverage report +CoverageReport.dfy(20,0): Error: Feature not supported for this translation target: Execution coverage report Dafny program verifier finished with 0 verified, 0 errors -CoverageReport.dfy(20,0): Error: Feature not supported for this compilation target: Execution coverage report +CoverageReport.dfy(20,0): Error: Feature not supported for this translation target: Execution coverage report diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/NativeNumbers.dfy.js.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/NativeNumbers.dfy.js.check index a28c44d375..0c59454703 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/NativeNumbers.dfy.js.check +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/NativeNumbers.dfy.js.check @@ -1 +1 @@ -// CHECK: Error: None of the types given in :nativeType arguments is supported by the current compilation target\. Try supplying others\. +// CHECK: Error: None of the types given in :nativeType arguments is supported by the current translation target\. Try supplying others\. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NativeTypeResolution.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NativeTypeResolution.dfy.expect index db6ee0f352..126603b4b3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NativeTypeResolution.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NativeTypeResolution.dfy.expect @@ -7,8 +7,8 @@ NativeTypeResolution.dfy(11,50): Info: newtype B resolves as {:nativeType "byte" NativeTypeResolution.dfy(12,50): Info: newtype C resolves as {:nativeType "int"} (detected range: 0 .. 256) NativeTypeResolution.dfy(14,35): Error: :nativeType 'reallylong' not known NativeTypeResolution.dfy(15,41): Error: :nativeType 'reallylong' not known -NativeTypeResolution.dfy(17,31): Error: None of the types given in :nativeType arguments is supported by the current compilation target. Try supplying others. -NativeTypeResolution.dfy(18,40): Error: None of the types given in :nativeType arguments is supported by the current compilation target. Try supplying others. +NativeTypeResolution.dfy(17,31): Error: None of the types given in :nativeType arguments is supported by the current translation target. Try supplying others. +NativeTypeResolution.dfy(18,40): Error: None of the types given in :nativeType arguments is supported by the current translation target. Try supplying others. NativeTypeResolution.dfy(21,22): Error: Dafny's heuristics cannot find a compatible native type. Hint: try writing a newtype constraint of the form 'i: int | lowerBound <= i < upperBound && (...any additional constraints...)' NativeTypeResolution.dfy(22,22): Info: newtype I resolves as {:nativeType "sbyte"} (detected range: -2 .. 30) NativeTypeResolution.dfy(23,27): Error: Dafny's heuristics cannot find a compatible native type. Hint: try writing a newtype constraint of the form 'i: int | lowerBound <= i < upperBound && (...any additional constraints...)' diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RuntimeTypeTests0.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RuntimeTypeTests0.dfy index dec3d0e25d..fdd84df652 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RuntimeTypeTests0.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RuntimeTypeTests0.dfy @@ -2,7 +2,7 @@ // RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" // The code in this file demonstrates complications in sorting out covariance in some -// compilation target languages. +// translation target languages. // // Part of the solution in Java is to use Java's wildcard types: a "Dafny.Sequence"" is assignable to // a "Dafny.Sequence". diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/ConsistentWhenSupported.dfy.oldway.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/ConsistentWhenSupported.dfy.oldway.expect index 5e1957e60b..47b9f4a9c2 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/ConsistentWhenSupported.dfy.oldway.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/ConsistentWhenSupported.dfy.oldway.expect @@ -11,10 +11,10 @@ Dafny program verifier did not attempt verification All done iterating! Dafny program verifier did not attempt verification -ConsistentWhenSupported.dfy(17,9): Error: Feature not supported for this compilation target: Iterators +ConsistentWhenSupported.dfy(17,9): Error: Feature not supported for this translation target: Iterators Dafny program verifier did not attempt verification -ConsistentWhenSupported.dfy(17,0): Error: Feature not supported for this compilation target: Unicode chars +ConsistentWhenSupported.dfy(17,0): Error: Feature not supported for this translation target: Unicode chars Dafny program verifier did not attempt verification All done iterating! diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/comp/NativeNumbers.dfy.js.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/comp/NativeNumbers.dfy.js.check index a28c44d375..0c59454703 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/comp/NativeNumbers.dfy.js.check +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/comp/NativeNumbers.dfy.js.check @@ -1 +1 @@ -// CHECK: Error: None of the types given in :nativeType arguments is supported by the current compilation target\. Try supplying others\. +// CHECK: Error: None of the types given in :nativeType arguments is supported by the current translation target\. Try supplying others\. diff --git a/Source/TestDafny/MultiBackendTest.cs b/Source/TestDafny/MultiBackendTest.cs index bbd861c141..059cc18b90 100644 --- a/Source/TestDafny/MultiBackendTest.cs +++ b/Source/TestDafny/MultiBackendTest.cs @@ -358,7 +358,7 @@ private int RunWithCompiler(ForEachCompilerOptions options, IExecutableBackend b return 1; } - // If we hit errors, check for known unsupported features or bugs for this compilation target + // If we hit errors, check for known unsupported features or bugs for this translation target if (error == "" && OnlyUnsupportedFeaturesErrors(backend, outputString)) { return 0; } diff --git a/docs/HowToFAQ/Errors-CommandLine.md b/docs/HowToFAQ/Errors-CommandLine.md index e12b19365c..2893f2e27a 100644 --- a/docs/HowToFAQ/Errors-CommandLine.md +++ b/docs/HowToFAQ/Errors-CommandLine.md @@ -121,7 +121,7 @@ a model view file using `/mv:` and The model view file is an arbitrary non-existent file that is created and used as a temporary file during the creation of the counterexamples. -## **Error: Feature not supported for this compilation target: _feature_** {#f_unsupported_feature} +## **Error: Feature not supported for this translation target: _feature_** {#f_unsupported_feature} ```dafny diff --git a/docs/HowToFAQ/FAQNewtype.md b/docs/HowToFAQ/FAQNewtype.md index 3cf3e49895..749fefad7a 100644 --- a/docs/HowToFAQ/FAQNewtype.md +++ b/docs/HowToFAQ/FAQNewtype.md @@ -25,7 +25,7 @@ This is evident in the allowed conversions, as shown in this example code: {% include_relative FAQNewtype.dfy %} ``` -The other important characteristic of `newtype`s is that they may have a different representation in the compilation target language. +The other important characteristic of `newtype`s is that they may have a different representation in the translation target language. Subset types are always represented in the same way as the base type. But a newtype may use a different representation. For example, the newtype defined above might use a `byte` representation in Java, whereas an `int` is a `BigInteger`. The representation of a newtype can be set by the program author using the [`{:nativeType}`](../DafnyRef/DafnyRef#sec-nativetype) attribute. diff --git a/docs/HowToFAQ/onepage.md b/docs/HowToFAQ/onepage.md index 5962fdee05..2ba85aab39 100644 --- a/docs/HowToFAQ/onepage.md +++ b/docs/HowToFAQ/onepage.md @@ -111,7 +111,7 @@ This is evident in the allowed conversions, as shown in this example code: {% include_relative FAQNewtype.dfy %} ``` -The other important characteristic of `newtype`s is that they may have a different representation in the compilation target language. +The other important characteristic of `newtype`s is that they may have a different representation in the translation target language. Subset types are always represented in the same way as the base type. But a newtype may use a different representation. For example, the newtype defined above might use a `byte` representation in Java, whereas an `int` is a `BigInteger`. The representation of a newtype can be set by the program author using the [`{:nativeType}`](../DafnyRef/DafnyRef#sec-nativetype) attribute.