Fresh binaries, fix test (take my own nag test’s suggestion :)

robin-aws · Nov 16, 2023 · c0623b9 · c0623b9
1 parent 19424a5
commit c0623b9
Show file tree

Hide file tree

Showing 12 changed files with 4 additions and 41 deletions.
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-arithmetic.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-arithmetic.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo
diff --git a/.../IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy b/.../IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy
@@ -1,29 +1,10 @@
 // This test just asserts what happens when you try to use a library
-// that isn't available for all backends.
+// that isn't available for all backends (see .check files).
 // Full testing of such libraries is handled in the DafnyStandardLibraries
 // project rather than here.
 
-// Valid:
-
-// RUN: %verify --standard-libraries:true "%s" > "%t"
-// RUN: %run --target:cs --standard-libraries:true "%s" >> "%t"
-// RUN: %run --target:java --standard-libraries:true "%s" >> "%t"
-// RUN: %run --target:go --standard-libraries:true "%s" >> "%t"
-// RUN: %run --target:js --standard-libraries:true "%s" >> "%t"
-// RUN: %run --target:py --standard-libraries:true "%s" >> "%t"
-
-// Invalid:
-
-// RUN: %exits-with 2 %run --target:cpp --standard-libraries:true "%s" >> "%t"
-// RUN: %exits-with 2 %run --target:rs --standard-libraries:true "%s" >> "%t"
-
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachCompiler "%s" -- --standard-libraries:true
 
 module UsesFileIO {
-
   import DafnyStdLibs.FileIO
-
-  method Main() {
-    var thisFile :- expect FileIO.ReadBytesFromFile("StandardLibraries_TargetSpecific.dfy");
-  }
 }
diff --git a/...onTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.cpp.check b/...onTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.cpp.check
@@ -0,0 +1 @@
+CHECK-L: StandardLibraries_TargetSpecific.dfy(9,22): Error: module FileIO does not exist (position 1 in path DafnyStdLibs.FileIO)
diff --git a/...ationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.expect b/...ationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.expect
@@ -1,20 +0,0 @@
-
-Dafny program verifier finished with 1 verified, 0 errors
-
-Dafny program verifier finished with 1 verified, 0 errors
-
-Dafny program verifier finished with 1 verified, 0 errors
-
-Dafny program verifier finished with 1 verified, 0 errors
-
-Dafny program verifier finished with 1 verified, 0 errors
-
-Dafny program verifier finished with 1 verified, 0 errors
-StandardLibraries_TargetSpecific.dfy(24,22): Error: module FileIO does not exist (position 1 in path DafnyStdLibs.FileIO)
-StandardLibraries_TargetSpecific.dfy(27,34): Error: unresolved identifier: ReadBytesFromFile
-StandardLibraries_TargetSpecific.dfy(27,17): Error: The type of the first expression to the right of ':-' could not be determined to be a failure type (got '?')
-3 resolution/type errors detected in the_program
-StandardLibraries_TargetSpecific.dfy(24,22): Error: module FileIO does not exist (position 1 in path DafnyStdLibs.FileIO)
-StandardLibraries_TargetSpecific.dfy(27,34): Error: unresolved identifier: ReadBytesFromFile
-StandardLibraries_TargetSpecific.dfy(27,17): Error: The type of the first expression to the right of ':-' could not be determined to be a failure type (got '?')
-3 resolution/type errors detected in the_program

diff --git a/...ionTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.rs.check b/...ionTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.rs.check
@@ -0,0 +1 @@
+CHECK-L: StandardLibraries_TargetSpecific.dfy(9,22): Error: module FileIO does not exist (position 1 in path DafnyStdLibs.FileIO)
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		CHECK-L: StandardLibraries_TargetSpecific.dfy(9,22): Error: module FileIO does not exist (position 1 in path DafnyStdLibs.FileIO)