diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect index 2bd757b626..7e24d9e430 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect @@ -50,4 +50,5 @@ Diff (changing expected into actual): +0 +(non-blocking) The Rust code generator is internal. Not having a '*.rs.check' file is acceptable for now. Executing on ResolvedDesugaredExecutableDafny... diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestBeyondVerifierExpect.dfy.testdafny.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestBeyondVerifierExpect.dfy.testdafny.expect index ce5735dda4..a881545e3b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestBeyondVerifierExpect.dfy.testdafny.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestBeyondVerifierExpect.dfy.testdafny.expect @@ -50,4 +50,5 @@ Diff (changing expected into actual): +hello +(non-blocking) The Rust code generator is internal. Not having a '*.rs.check' file is acceptable for now. Executing on ResolvedDesugaredExecutableDafny... diff --git a/Source/TestDafny/MultiBackendTest.cs b/Source/TestDafny/MultiBackendTest.cs index cbc2996835..6e9d6272ff 100644 --- a/Source/TestDafny/MultiBackendTest.cs +++ b/Source/TestDafny/MultiBackendTest.cs @@ -423,6 +423,12 @@ await output.WriteLineAsync( } await output.WriteLineAsync(diffMessage); + if (backend.IsInternal) { + await output.WriteLineAsync( + $"(non-blocking) The {backend.TargetName} code generator is internal. Not having a '*.{backend.TargetId}.check' file is acceptable for now."); + return 0; + } + return 1; } @@ -456,9 +462,25 @@ await output.WriteLineAsync( } } + if (backend.IsInternal && checkResult != 0) { + await output.WriteLineAsync( + $"(non-blocking) The {backend.TargetName} code generator is internal. An unmatched '*.{backend.TargetId}.check' file is acceptable for now."); + return 0; + } + return checkResult; } + + if (backend.IsInternal) { + await output.WriteLineAsync($"(non-blocking) Execution failed for the internal {backend.TargetName} code generator, for reasons other than known unsupported features. Output:"); + await output.WriteLineAsync(outputString); + await output.WriteLineAsync("Error:"); + await output.WriteLineAsync(error); + await output.WriteLineAsync( + $"The {backend.TargetName} code generator is internal. An unmatched '*.{backend.TargetId}.check' file is acceptable for now."); + return 0; + } await output.WriteLineAsync("Execution failed, for reasons other than known unsupported features. Output:"); await output.WriteLineAsync(outputString); await output.WriteLineAsync("Error:");