Expect and check files

robin-aws · Dec 6, 2023 · b8b7116 · b8b7116
1 parent d2a7d7d
commit b8b7116
Show file tree

Hide file tree

Showing 8 changed files with 11 additions and 16 deletions.
diff --git a/...e/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/Interop.cs b/...e/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/Interop.cs
@@ -7,13 +7,13 @@ public static partial class __default {
     public static BigInteger Int32ToInt(int value) {
       return new BigInteger(value);
     }
-    public static DafnyStdLibs.Wrappers._IOption<int> IntToInt32(BigInteger value) {
+    public static Std.Wrappers._IOption<int> IntToInt32(BigInteger value) {
       if (value > int.MaxValue || value < int.MinValue) {
-        return DafnyStdLibs.Wrappers.Option<int>.create_None();
+        return Std.Wrappers.Option<int>.create_None();
       }
       else
       {
-        return DafnyStdLibs.Wrappers.Option<int>.create_Some((int)value);
+        return Std.Wrappers.Option<int>.create_Some((int)value);
       }
     }
   }

diff --git a/...nTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/Interop/__default.java b/...nTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/Interop/__default.java
@@ -14,11 +14,11 @@ public static Integer IntegerMaxValue() {
   public static BigInteger Int32ToInt(Integer value) {
     return BigInteger.valueOf(value);
   }
-  public static DafnyStdLibs.Wrappers.Option<Integer> IntToInt32(BigInteger value) {
+  public static Std.Wrappers.Option<Integer> IntToInt32(BigInteger value) {
     try {
-      return DafnyStdLibs.Wrappers.Option.create_Some(TypeDescriptor.intWithDefault(0), (Integer)value.intValueExact());
+      return Std.Wrappers.Option.create_Some(TypeDescriptor.intWithDefault(0), (Integer)value.intValueExact());
     } catch(ArithmeticException e) {
-      return DafnyStdLibs.Wrappers.Option.create_None(TypeDescriptor.intWithDefault(0));
+      return Std.Wrappers.Option.create_None(TypeDescriptor.intWithDefault(0));
     }
   }
 }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/StdLibsOffByDefaultInTests.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/StdLibsOffByDefaultInTests.dfy
@@ -11,8 +11,3 @@ module TriesToUseWrappers {
     if b == 0 then None else Some(a/b)
   }
 }
-
-
-// TODO:
-// * Big ol README, especially regarding todos, standards, and brittleness
-// * remove libraries submodule (confusing!)
diff --git a/...tegrationTests/TestFiles/LitTests/LitTest/metatests/StdLibsOffByDefaultInTests.dfy.expect b/...tegrationTests/TestFiles/LitTests/LitTest/metatests/StdLibsOffByDefaultInTests.dfy.expect
@@ -1,4 +1,4 @@
-StdLibsOffByDefaultInTests.dfy(8,29): Error: module DafnyStdLibs does not exist (position 0 in path DafnyStdLibs.Wrappers)
+StdLibsOffByDefaultInTests.dfy(8,20): Error: module Std does not exist (position 0 in path Std.Wrappers)
 1 resolution/type errors detected in StdLibsOffByDefaultInTests.dfy
 
 Dafny program verifier finished with 1 verified, 0 errors
diff --git a/...e/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_Errors.dfy.expect b/...e/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_Errors.dfy.expect
@@ -2,7 +2,7 @@
 Dafny program verifier finished with 1 verified, 0 errors
 
 Dafny program verifier finished with 1 verified, 0 errors
-StandardLibraries_Errors.dfy(20,29): Error: module DafnyStdLibs does not exist (position 0 in path DafnyStdLibs.Wrappers)
+StandardLibraries_Errors.dfy(20,20): Error: module Std does not exist (position 0 in path Std.Wrappers)
 1 resolution/type errors detected in StandardLibraries_Errors.dfy
 CLI: Error: cannot load DafnyStandardLibraries-notarget.doo: --unicode-char is set locally to False, but the library was built with True
 CLI: Error: cannot load DafnyStandardLibraries.doo: --unicode-char is set locally to False, but the library was built with True

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