summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
Diffstat (limited to 'Test')
-rw-r--r--Test/VSI-Benchmarks/b4.dfy2
-rw-r--r--Test/VSI-Benchmarks/b8.dfy2
-rw-r--r--Test/dafny0/Answer74
-rw-r--r--Test/dafny0/EqualityTypes.dfy89
-rw-r--r--Test/dafny0/Modules0.dfy25
-rw-r--r--Test/dafny0/SmallTests.dfy2
-rw-r--r--Test/dafny0/Termination.dfy4
-rw-r--r--Test/dafny0/TypeParameters.dfy4
-rw-r--r--Test/dafny0/TypeTests.dfy3
-rw-r--r--Test/dafny0/runtest.bat2
-rw-r--r--Test/dafny1/Celebrity.dfy2
-rw-r--r--Test/dafny1/UltraFilter.dfy2
-rw-r--r--Test/dafny2/MajorityVote.dfy12
-rw-r--r--Test/vstte2012/BreadthFirstSearch.dfy2
14 files changed, 167 insertions, 58 deletions
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index b70ff4d0..76e1ffa7 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -14,7 +14,7 @@
// that the specification can use mathematical sequences while the
// implementation uses a linked list.
-class Map<Key,Value> {
+class Map<Key(==),Value> {
ghost var Keys: seq<Key>;
ghost var Values: seq<Value>;
ghost var Repr: set<object>;
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index 383bccfd..2149df25 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -250,7 +250,7 @@ class WriterStream {
-class Map<Key,Value> {
+class Map<Key(==),Value> {
var keys: seq<Key>;
var values: seq<Value>;
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 5f80df86..7510363a 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -58,7 +58,6 @@ class C {
Dafny program verifier finished with 0 verified, 0 errors
-------------------- TypeTests.dfy --------------------
-TypeTests.dfy(89,9): Error: sorry, cannot instantiate collection type with a subrange type
TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)
TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)
TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)
@@ -88,11 +87,12 @@ TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the
TypeTests.dfy(84,2): Error: LHS of array assignment must denote an array element (found seq<C>)
TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
-TypeTests.dfy(90,9): Error: sorry, cannot instantiate type parameter with a subrange type
-TypeTests.dfy(91,8): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(90,6): Error: sorry, cannot instantiate collection type with a subrange type
+TypeTests.dfy(91,9): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type
-TypeTests.dfy(116,4): Error: cannot assign to non-ghost variable in a ghost context
-TypeTests.dfy(117,7): Error: cannot assign to non-ghost variable in a ghost context
+TypeTests.dfy(93,8): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(117,4): Error: cannot assign to non-ghost variable in a ghost context
+TypeTests.dfy(118,7): Error: cannot assign to non-ghost variable in a ghost context
TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
36 resolution/type errors detected in TypeTests.dfy
@@ -719,33 +719,32 @@ Modules0.dfy(43,18): Error: The name T ambiguously refers to a type in one of th
Modules0.dfy(44,15): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
Modules0.dfy(46,16): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
Modules0.dfy(47,18): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
-Modules0.dfy(43,13): Error: Function body type mismatch (expected T, got T)
-Modules0.dfy(48,19): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
-Modules0.dfy(48,12): Error: new can be applied only to reference types (got T)
-Modules0.dfy(54,12): Error: Undeclared top-level type or type parameter: T (did you forget a module import?)
-Modules0.dfy(70,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)
-Modules0.dfy(71,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
-Modules0.dfy(81,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
-Modules0.dfy(105,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget a module import?)
-Modules0.dfy(244,11): Error: Undeclared top-level type or type parameter: X (did you forget a module import?)
-Modules0.dfy(250,15): Error: unresolved identifier: X
-Modules0.dfy(251,17): Error: member DoesNotExist does not exist in class X
-Modules0.dfy(294,16): Error: member R does not exist in class B
-Modules0.dfy(294,6): Error: expected method call, found expression
-Modules0.dfy(317,18): Error: second argument to "in" must be a set or sequence with elements of type Q_Imp.Node, or a map with domain Q_Imp.Node (instead got set<Node>)
-Modules0.dfy(321,13): Error: arguments must have the same type (got Q_Imp.Node and Node)
-Modules0.dfy(322,11): Error: Undeclared module name: LongLostModule (did you forget a module import?)
-Modules0.dfy(323,11): Error: Undeclared module name: Wazzup (did you forget a module import?)
-Modules0.dfy(324,17): Error: Undeclared class name Edon in module Q_Imp
-Modules0.dfy(326,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)
-Modules0.dfy(327,30): Error: member Create does not exist in class Klassy
-Modules0.dfy(140,11): Error: ghost variables are allowed only in specification contexts
-Modules0.dfy(154,11): Error: old expressions are allowed only in specification and ghost contexts
-Modules0.dfy(155,11): Error: fresh expressions are allowed only in specification and ghost contexts
-Modules0.dfy(156,11): Error: allocated expressions are allowed only in specification and ghost contexts
-Modules0.dfy(172,10): Error: match source expression 'tree' has already been used as a match source expression in this context
-Modules0.dfy(211,12): Error: match source expression 'l' has already been used as a match source expression in this context
-37 resolution/type errors detected in Modules0.dfy
+Modules0.dfy(52,19): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
+Modules0.dfy(52,12): Error: new can be applied only to reference types (got T)
+Modules0.dfy(57,12): Error: Undeclared top-level type or type parameter: T (did you forget a module import?)
+Modules0.dfy(73,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)
+Modules0.dfy(74,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
+Modules0.dfy(84,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
+Modules0.dfy(108,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget a module import?)
+Modules0.dfy(247,11): Error: Undeclared top-level type or type parameter: X (did you forget a module import?)
+Modules0.dfy(256,13): Error: unresolved identifier: X
+Modules0.dfy(257,15): Error: member DoesNotExist does not exist in class X
+Modules0.dfy(299,16): Error: member R does not exist in class B
+Modules0.dfy(299,6): Error: expected method call, found expression
+Modules0.dfy(322,18): Error: second argument to "in" must be a set or sequence with elements of type Q_Imp.Node, or a map with domain Q_Imp.Node (instead got set<Node>)
+Modules0.dfy(326,13): Error: arguments must have the same type (got Q_Imp.Node and Node)
+Modules0.dfy(327,11): Error: Undeclared module name: LongLostModule (did you forget a module import?)
+Modules0.dfy(328,11): Error: Undeclared module name: Wazzup (did you forget a module import?)
+Modules0.dfy(329,17): Error: Undeclared class name Edon in module Q_Imp
+Modules0.dfy(331,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)
+Modules0.dfy(332,30): Error: member Create does not exist in class Klassy
+Modules0.dfy(143,11): Error: ghost variables are allowed only in specification contexts
+Modules0.dfy(157,11): Error: old expressions are allowed only in specification and ghost contexts
+Modules0.dfy(158,11): Error: fresh expressions are allowed only in specification and ghost contexts
+Modules0.dfy(159,11): Error: allocated expressions are allowed only in specification and ghost contexts
+Modules0.dfy(175,10): Error: match source expression 'tree' has already been used as a match source expression in this context
+Modules0.dfy(214,12): Error: match source expression 'l' has already been used as a match source expression in this context
+36 resolution/type errors detected in Modules0.dfy
-------------------- Modules1.dfy --------------------
Modules1.dfy(74,16): Error: assertion violation
@@ -1328,6 +1327,17 @@ Dafny program verifier finished with 12 verified, 3 errors
Dafny program verifier finished with 12 verified, 0 errors
+-------------------- EqualityTypes.dfy --------------------
+EqualityTypes.dfy(31,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype
+EqualityTypes.dfy(32,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality
+EqualityTypes.dfy(37,11): Error: arbitrary type 'X' is not allowed to be replaced by a datatype that takes type parameters
+EqualityTypes.dfy(38,8): Error: arbitrary type 'Y' is not allowed to be replaced by a class that takes type parameters
+EqualityTypes.dfy(42,11): Error: datatype 'X' is used to refine an arbitrary type with equality support, but 'X' does not support equality
+EqualityTypes.dfy(43,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality
+EqualityTypes.dfy(63,7): Error: == can only be applied to expressions of types that support equality (got Dt<T>)
+EqualityTypes.dfy(82,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0)
+8 resolution/type errors detected in EqualityTypes.dfy
+
-------------------- SplitExpr.dfy --------------------
Dafny program verifier finished with 5 verified, 0 errors
diff --git a/Test/dafny0/EqualityTypes.dfy b/Test/dafny0/EqualityTypes.dfy
new file mode 100644
index 00000000..251b2e2f
--- /dev/null
+++ b/Test/dafny0/EqualityTypes.dfy
@@ -0,0 +1,89 @@
+module A {
+ datatype Explicit<T(==)> = Nil | Cons(set<T>, Explicit<T>);
+ datatype Inferred<T> = Nil | Cons(set<T>, Inferred<T>);
+
+ class C {
+ method M<T>(x: Explicit<T>)
+ method N<T>(x: Inferred<T>)
+ }
+}
+
+module B refines A {
+ class C {
+ method M<T>(x: Explicit<T>)
+ method N<T(==)>(x: Inferred<T>)
+ }
+}
+
+// ----------------------------
+
+module C {
+ type X(==);
+ type Y(==);
+}
+
+module D refines C {
+ class X { }
+ datatype Y = Red | Green | Blue;
+}
+
+module E refines C {
+ codatatype X = Next(int, X); // error: X requires equality and codatatypes don't got it
+ datatype Y = Nil | Something(Z) | More(Y, Y); // error: Y does not support equality
+ codatatype Z = Red | Green(X) | Blue;
+}
+
+module F refines C {
+ datatype X<T> = Nil | Cons(T, X<T>); // error: not allowed to add a type parameter to type X
+ class Y<T> { } // error: not allowed to add a type parameter to type Y
+}
+
+module G refines C {
+ datatype X = Nil | Next(Z, X); // error: X does not support equality
+ datatype Y = Nil | Something(Z) | More(Y, Y); // error: Y does not support equality
+ codatatype Z = Red | Green | Blue;
+}
+
+// ----------------------------
+
+module H {
+ datatype Dt<T> = Nil | Cons(T, Dt);
+
+ datatype BulkyList<T> = Nothing | Wrapper(T, BulkyListAux);
+ datatype BulkyListAux<T> = Kons(set<T>, BulkyListAuxAux);
+ datatype BulkyListAuxAux<T> = GoBack(BulkyList);
+
+ codatatype Stream<T> = Next(head: T, tail: Stream<T>);
+
+ method M<T(==)>(x: T)
+ { }
+ function method F<T>(x: BulkyList<T>, y: BulkyList<T>): int
+ { if x == y then 5 else 7 } // this equality is allowed
+ function method G<T>(x: Dt<T>, y: Dt<T>): int
+ { if x == y then 5 else 7 } // error: the equality is not allowed, because Dt<T> may not support equality
+ function method G'<T(==)>(x: Dt<T>, y: Dt<T>): int
+ { if x == y then 5 else 7 } // fine
+
+ method Caller0(b: BulkyList, y: int) {
+ match (b) {
+ case Nothing =>
+ case Wrapper(t, bla) =>
+ var u;
+ if (y < 100) { u := t; }
+ // The following call is allowed, because it will be inferred that
+ // 'u' is of a type that supports equality
+ M(u);
+ }
+ }
+ method Caller1(d: Dt) {
+ match (d) {
+ case Nil =>
+ case Cons(t, rest) =>
+ M(t); // error: t may be of a type that does not support equality
+ }
+ }
+ method Caller2(co: Stream) {
+ var d := Cons(co, Nil);
+ Caller1(d); // case in point for the error in Caller1
+ }
+}
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index cc66c3c1..80ac7eef 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -45,9 +45,12 @@ module A imports N, M { // Note, this has the effect of importing two different
{ x }
method M(x: T) // error: use of the ambiguous name T
returns (y: T) // error: use of the ambiguous name T
- { var g := new T; } // error: use of the ambiguous name T
}
}
+module A' imports N, M {
+ method M()
+ { var g := new T; } // error: use of the ambiguous name T
+}
module B0 imports A {
class BadUse {
@@ -241,15 +244,17 @@ module BTr imports ATr {
module CTr imports BTr {
class Z {
var b: Y; // fine
- var a: X; // error: imports don't reach name name X explicitly
- method P() {
- var y := new Y;
- var x := y.N(); // this is allowed and will correctly infer the type of x to
- // be X, but X could not have been mentioned explicitly
- var q := x.M();
- var r := X.Q(); // error: X is not in scope
- var s := x.DoesNotExist(); // error: method not declared in class X
- }
+ var a: X; // error: imports don't reach name X explicitly
+ }
+}
+module CTs imports BTr {
+ method P() {
+ var y := new Y;
+ var x := y.N(); // this is allowed and will correctly infer the type of x to
+ // be X, but X could not have been mentioned explicitly
+ var q := x.M();
+ var r := X.Q(); // error: X is not in scope
+ var s := x.DoesNotExist(); // error: method not declared in class X
}
}
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index e8b618d7..40df1135 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -294,7 +294,7 @@ method QuantifierRange1<T>(a: seq<T>, x: T, y: T, N: int)
assert x != y;
}
-method QuantifierRange2<T>(a: seq<T>, x: T, y: T, N: int)
+method QuantifierRange2<T(==)>(a: seq<T>, x: T, y: T, N: int)
requires 0 <= N && N <= |a|;
requires exists k | 0 <= k && k < N :: a[k] == y;
ensures forall k | 0 <= k && k < N :: a[k] == y; // error
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index 1482dc24..bf3702ae 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -92,8 +92,8 @@ class Termination {
ensures a == List.Cons(val, b);
{
match a {
- case Cons(v, r) => val := v; b := r;
- }
+ case Cons(v, r) => val := v; b := r;
+ }
}
}
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index d6804661..cb9b5660 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -1,11 +1,11 @@
-class C<U> {
+class C<U(==)> {
method M<T>(x: T, u: U) returns (y: T)
ensures x == y && u == u;
{
y := x;
}
- function method F<X>(x: X, u: U): bool
+ function method F<X(==)>(x: X, u: U): bool
{
x == x && u == u
}
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 8434f06c..2dea7a52 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -86,7 +86,8 @@ method ArrayRangeAssignments(a: array<C>, c: C)
// --------------------- tests of restrictions on subranges (nat)
-method K(s: set<nat>) { // error: not allowed to instantiate 'set' with 'nat'
+method K() {
+ var s: set<nat>; // error: not allowed to instantiate 'set' with 'nat'
var d: MutuallyRecursiveDataType<nat>; // error: not allowed to instantiate with 'nat'
var a := new nat[100]; // error: not allowed the type array<nat>
var b := new nat[100,200]; // error: not allowed the type array2<nat>
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index ac7c8aed..d352cf44 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -17,7 +17,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
Comprehensions.dfy Basics.dfy ControlStructures.dfy
Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy
TypeParameters.dfy Datatypes.dfy Coinductive.dfy Corecursion.dfy
- TypeAntecedents.dfy NoTypeArgs.dfy SplitExpr.dfy
+ TypeAntecedents.dfy NoTypeArgs.dfy EqualityTypes.dfy SplitExpr.dfy
LoopModifies.dfy Refinement.dfy RefinementErrors.dfy
ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy
CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy
diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy
index 21b895aa..4c761671 100644
--- a/Test/dafny1/Celebrity.dfy
+++ b/Test/dafny1/Celebrity.dfy
@@ -10,7 +10,7 @@ static function IsCelebrity<Person>(c: Person, people: set<Person>): bool
}
method FindCelebrity0<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
- requires (exists c :: IsCelebrity(c, people));
+ requires exists c :: IsCelebrity(c, people);
ensures r == c;
{
var cc; assume cc == c; // this line essentially converts ghost c to non-ghost cc
diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy
index c8419890..c78d5e81 100644
--- a/Test/dafny1/UltraFilter.dfy
+++ b/Test/dafny1/UltraFilter.dfy
@@ -1,6 +1,6 @@
// ultra filter
-class UltraFilter<G> {
+class UltraFilter<G(==)> {
static function IsFilter(f: set<set<G>>, S: set<G>): bool
{
(forall A, B :: A in f && A <= B ==> B in f) &&
diff --git a/Test/dafny2/MajorityVote.dfy b/Test/dafny2/MajorityVote.dfy
index a7512486..af67ee92 100644
--- a/Test/dafny2/MajorityVote.dfy
+++ b/Test/dafny2/MajorityVote.dfy
@@ -31,6 +31,10 @@
// choice, if there is such a choice, and then passes in that choice as the ghost parameter K
// to the main algorithm. Neat, huh?
+// Language comment:
+// The "(==)" that sits after some type parameters in this program says that the actual
+// type argument must support equality.
+
// Advanced remark:
// There is a subtle situation in the verification of DetermineElection. Suppose the type
// parameter Candidate denotes some type whose instances depend on which object are
@@ -47,7 +51,7 @@
// to the Count function. Alternatively, one could have added the antecedent "c in a" or
// "old(allocated(c))" to the "forall c" quantification in the postcondition of DetermineElection.
-function method Count<T>(a: seq<T>, s: int, t: int, x: T): int
+function method Count<T(==)>(a: seq<T>, s: int, t: int, x: T): int
requires 0 <= s <= t <= |a|;
ensures Count(a, s, t, x) == 0 || x in a;
{
@@ -57,7 +61,7 @@ function method Count<T>(a: seq<T>, s: int, t: int, x: T): int
// Here is the first version of the algorithm, the one that assumes there is a majority choice.
-method FindWinner<Candidate>(a: seq<Candidate>, ghost K: Candidate) returns (k: Candidate)
+method FindWinner<Candidate(==)>(a: seq<Candidate>, ghost K: Candidate) returns (k: Candidate)
requires 2 * Count(a, 0, |a|, K) > |a|; // K has a (strict) majority of the votes
ensures k == K; // find K
{
@@ -93,7 +97,7 @@ method FindWinner<Candidate>(a: seq<Candidate>, ghost K: Candidate) returns (k:
// Here is the second version of the program, the one that also computes whether or not
// there is a majority choice.
-method DetermineElection<Candidate>(a: seq<Candidate>) returns (hasWinner: bool, cand: Candidate)
+method DetermineElection<Candidate(==)>(a: seq<Candidate>) returns (hasWinner: bool, cand: Candidate)
ensures hasWinner ==> 2 * Count(a, 0, |a|, cand) > |a|;
ensures !hasWinner ==> forall c :: 2 * Count(a, 0, |a|, c) <= |a|;
{
@@ -107,7 +111,7 @@ method DetermineElection<Candidate>(a: seq<Candidate>) returns (hasWinner: bool,
// antecedent "hasWinner ==>" and the two checks for no-more-votes that may result in a "return"
// statement.
-method SearchForWinner<Candidate>(a: seq<Candidate>, ghost hasWinner: bool, ghost K: Candidate) returns (k: Candidate)
+method SearchForWinner<Candidate(==)>(a: seq<Candidate>, ghost hasWinner: bool, ghost K: Candidate) returns (k: Candidate)
requires hasWinner ==> 2 * Count(a, 0, |a|, K) > |a|; // K has a (strict) majority of the votes
ensures hasWinner ==> k == K; // find K
{
diff --git a/Test/vstte2012/BreadthFirstSearch.dfy b/Test/vstte2012/BreadthFirstSearch.dfy
index 5153b053..4373136b 100644
--- a/Test/vstte2012/BreadthFirstSearch.dfy
+++ b/Test/vstte2012/BreadthFirstSearch.dfy
@@ -1,4 +1,4 @@
-class BreadthFirstSearch<Vertex>
+class BreadthFirstSearch<Vertex(==)>
{
// The following function is left uninterpreted (for the purpose of the
// verification problem, it can be thought of as a parameter to the class)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 19:41:36 +0000