Ghost variables are not correctly initialized in interfaces
@pcanelas đang làm issue này rồi.
Từ ngày 4/7/2025.
Đánh giá
Issue này chưa được đánh giá.
Mô tả
Ghost variable initialization is dependent on declaring the constructor for the type the that the refinements are for. This declaration implicitly initializes int variables in a way equivalent to @StateRefinement(to = "var(this) == 0")
It is not possible to declare constructors for interface types as these don't have constructors. This prohibits the correct initialization of both Ghost variables and States for interfaces
@ExternalRefinementsFor("java.util.List")
@Ghost("int size2")
public interface ListRefinements<E> {
@StateRefinement(to = "size2(this) == (size2(old(this)) + 1)")
public boolean add(E elem);
@StateRefinement(from = "size2(this) > 0", to = "size2(this) == (size2(old(this)) - 1)")
public void remove(@Refinement("index >= 0") int index);
}
public static void main(String[] args) {
List<Integer> l = new ArrayList<>();
l.add(0);
int a = l.remove(0);
}
The error provided is Failed to check state transitions when calling l.remove(0)
This error messages is identical to the error message that would appear when attempting the same operation on a concrete class without a declared constructor in the Refinement definitions
- Ngôn ngữ chính
- Java
- Star
- 67
- Fork
- 36
- Merge trung bình
- 10 ngày 18 giờ
- Pull request đã merge (30 ngày)
- 3
Hướng dẫn đóng góp
Bắt đầu từ đâu
- Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
- Bình luận trên issue rằng bạn sẽ nhận — tránh hai người làm cùng một việc.
- Fork repository và làm thay đổi trên một nhánh.
- Mở pull request có tham chiếu số hiệu của issue.
Issue khác của liquid-java/liquidjava
-
enhancement
liquid-java/liquidjava#240 · 1 người được giao ·
-
enhancement ide
Độ khó 3/5 1-2 ngày Mức phù hợp với người mới 45/100
liquid-java/liquidjava#206 ·
-
tests
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 25/100
liquid-java/liquidjava#198 ·
-
Diagnostic Based Test Results Đang mởtests
Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 25/100
liquid-java/liquidjava#197 ·
-
tests
Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 35/100
liquid-java/liquidjava#196 · 2 bình luận ·
Tất cả issue của liquid-java/liquidjava
Issue tương tự
-
bug untriaged
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 84/100
opensearch-project/ml-commons#5094 ·
-
bug
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 85/100
-
emitter:client:csharp feature
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 72/100
-
affects/8.10 affects/8.9 component/clients kind/bug likelihood/mid severity/mid
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 78/100
-
Two open-case totals on one screen: the Programs tile says 15,858 and the nav badge says 15,868 Đang mởbug frontend maui-pilot
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 72/100