Add --test-assumptions option (#3185)

### Changes

Add the `--test-assumptions` option to all execution commands:
run,build,translate,test

Note that I've written the description of the option to be aspirational,
so that it indicates what we want this option to do, with the note that
it's experimental and after that an explanation of what it currently
does. I've also simplified the option so it's just an off/on boolean,
instead of allowing using to choose under what conditions they want to
add tests, since I don't yet see a use-case for the previous
`:TestExterns` option. Feel free to discuss!

### Testing

Add the new option in a littish test

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Author: keyboardDrummer

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -1,5 +1,6 @@
 using System.Collections.Generic;
 using System.CommandLine;
+using System.Diagnostics.Tracing;
 using System.Linq;
 
 namespace Microsoft.Dafny; 
@@ -124,13 +125,26 @@ Note that quantifier variable domains (<- <Domain>) are available in both syntax
   public static readonly Option<bool> IncludeRuntime = new("--include-runtime",
     "Include the Dafny runtime as source in the target language.");
 
+  public enum TestAssumptionsMode {
+    None,
+    Externs
+  }
+
+  public static readonly Option<TestAssumptionsMode> TestAssumptions = new("--test-assumptions", () => TestAssumptionsMode.None, @"
+(experimental) When turned on, inserts runtime tests at locations where (implicit) assumptions occur, such as when calling or being called by external code and when using assume statements.
+
+Functionality is still being expanded. Currently only checks contracts on every call to a function or method marked with the {:extern} attribute.".TrimStart());
+
   static CommonOptionBag() {
     DafnyOptions.RegisterLegacyBinding(SolverPath, (options, value) => {
       if (!string.IsNullOrEmpty(value)) {
         options.ProverOptions.Add($"PROVER_PATH={value}");
       }
     });
 
+    DafnyOptions.RegisterLegacyBinding(TestAssumptions, (options, value) => {
+      options.TestContracts = value == TestAssumptionsMode.Externs ? DafnyOptions.ContractTestingMode.Externs : DafnyOptions.ContractTestingMode.None;
+    });
     DafnyOptions.RegisterLegacyBinding(ManualLemmaInduction, (options, value) => {
       if (value) {
         options.Induction = 1;

Source/DafnyCore/Options/ICommandSpec.cs

@@ -38,6 +38,7 @@ static ICommandSpec() {
     BoogieOptionBag.NoVerify,
     CommonOptionBag.EnforceDeterminism,
     CommonOptionBag.OptimizeErasableDatatypeWrapper,
+    CommonOptionBag.TestAssumptions
   }.Concat(VerificationOptions).ToList();
 
   public static IReadOnlyList<Option> ConsoleOutputOptions = new List<Option>(new Option[] {

Test/contract-wrappers/AllExterns.dfy

@@ -1,4 +1,4 @@
-// RUN: ! %dafny /compile:4 /noVerify /runAllTests:1 /testContracts:Externs %s %s.externs.cs > %t
+// RUN: ! %baredafny test %args --no-verify --test-assumptions=externs %s %s.externs.cs > %t
 // RUN: %diff "%s.expect" "%t"
 // RUN: %OutputCheck --file-to-check "%S/AllExterns.cs" "%s"
 // CHECK: .*Foo____dafny__checked\(x\).*