Update textual references to compilation target

dafny-lang · Jan 5, 2024 · 5e601ff · 5e601ff
1 parent a5d98ae
commit 5e601ff
Show file tree

Hide file tree

Showing 15 changed files with 22 additions and 22 deletions.
diff --git 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})");
     }
   }
 }
diff --git 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
@@ -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
@@ -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/...egrationTests/TestFiles/LitTests/LitTest/benchmarks/sequence-race/SequenceRace.dfy.expect b/...egrationTests/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
@@ -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
@@ -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
@@ -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
@@ -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<T>"" is assignable to
 // a "Dafny.Sequence<? extends T>".

diff --git a/...ationTests/TestFiles/LitTests/LitTest/metatests/ConsistentWhenSupported.dfy.oldway.expect b/...ationTests/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/.../IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/comp/NativeNumbers.dfy.js.check b/.../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
@@ -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
@@ -121,7 +121,7 @@ a model view file using `/mv:<file>` 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}
 
 <!-- %check-run %exit 3 %options -t:cpp --unicode-char=true -->
 ```dafny

diff --git 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
@@ -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.