From b8b7116ab0b72505877987d6a2c5e9697f9ff551 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Dec 2023 10:52:09 -0800 Subject: [PATCH] Expect and check files --- .../LitTest/comp/replaceables/complex/Inputs/Interop.cs | 6 +++--- .../comp/replaceables/complex/Inputs/Interop/__default.java | 6 +++--- .../LitTest/metatests/StdLibsOffByDefaultInTests.dfy | 5 ----- .../LitTest/metatests/StdLibsOffByDefaultInTests.dfy.expect | 2 +- .../LitTest/stdlibs/StandardLibraries_Errors.dfy.expect | 2 +- .../stdlibs/StandardLibraries_TargetSpecific.dfy.cpp.check | 2 +- .../stdlibs/StandardLibraries_TargetSpecific.dfy.dfy.check | 2 +- .../stdlibs/StandardLibraries_TargetSpecific.dfy.rs.check | 2 +- 8 files changed, 11 insertions(+), 16 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/Interop.cs b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/Interop.cs index e15d29b5d44..a7d7eda5ee6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/Interop.cs +++ b/Source/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 IntToInt32(BigInteger value) { + public static Std.Wrappers._IOption IntToInt32(BigInteger value) { if (value > int.MaxValue || value < int.MinValue) { - return DafnyStdLibs.Wrappers.Option.create_None(); + return Std.Wrappers.Option.create_None(); } else { - return DafnyStdLibs.Wrappers.Option.create_Some((int)value); + return Std.Wrappers.Option.create_Some((int)value); } } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/Interop/__default.java b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/Interop/__default.java index b05bbd53d00..0c51ed5cf1a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/Interop/__default.java +++ b/Source/IntegrationTests/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 IntToInt32(BigInteger value) { + public static Std.Wrappers.Option 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)); } } } \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/StdLibsOffByDefaultInTests.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/StdLibsOffByDefaultInTests.dfy index e74ec08c65c..735db5931f4 100644 --- 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/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/StdLibsOffByDefaultInTests.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/StdLibsOffByDefaultInTests.dfy.expect index d447270d95f..8eec6b450fe 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/StdLibsOffByDefaultInTests.dfy.expect +++ b/Source/IntegrationTests/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/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_Errors.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_Errors.dfy.expect index c3e9db2cdb5..c00cecbcdf4 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_Errors.dfy.expect +++ b/Source/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/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.cpp.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.cpp.check index 73c3a21186e..0aa47749578 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.cpp.check +++ b/Source/IntegrationTests/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/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.dfy.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.dfy.check index 73c3a21186e..0aa47749578 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.dfy.check +++ b/Source/IntegrationTests/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/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.rs.check index 73c3a21186e..0aa47749578 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.rs.check +++ b/Source/IntegrationTests/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)