From 0a7e9b54fc2ac27a2c8b7468e01e7d7afefd036c Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Tue, 21 May 2024 15:27:59 +0200 Subject: [PATCH] implements the remaining CR suggestions by Joao --- .../frontend/info/implementation/property/Implements.scala | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/property/Implements.scala b/src/main/scala/viper/gobra/frontend/info/implementation/property/Implements.scala index 24756797f..3f30f9442 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/property/Implements.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/property/Implements.scala @@ -92,6 +92,11 @@ trait Implements { this: TypeInfoImpl => /** Returns true if the type is supported for interfaces. All finite types are supported except for structs with ghost fields. */ def supportedSortForInterfaces(t: Type): PropertyResult = { failedProp(s"The type $t is not supported for interface", !isIdentityPreservingType(t)) and + // the following restriction is in place because Go considers two struct values under an interface to be equal if + // they agree on their struct fields. I.e., for `type S struct { val int, ghost gval int }`, `any(S{0, 0}) == any(S{0, 42})` holds + // in Go (after erasing the ghost fields). While we could extend the interface encoding to permit structs with ghost fields + // to implement an interface, we currently reject such cases. However, note that we already support a _pointer_ to a struct with + // ghost fields implementing an interface. failedProp(s"Structs containing ghost fields are not supported for interface", isStructTypeWithGhostFields(t)) }