From 589437b92cdb3eee25cd9dcee9222bcca9dab1e3 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 23 Oct 2025 15:40:05 +0100 Subject: [PATCH 1/2] Substitute `this` in Parameter Refinements --- .../general_checkers/MethodsFunctionsChecker.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index 8b1806fd..79f36b6d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java @@ -374,6 +374,10 @@ private void checkParameters(CtElement invocation, List> arg for (String s : vars) if (map.containsKey(s)) c = c.substituteVariable(s, map.get(s)); + if (invocation.getMetadata(rtc.TARGET_KEY) != null) { + VariableInstance vi = (VariableInstance) invocation.getMetadata(rtc.TARGET_KEY); + c = c.substituteVariable(rtc.THIS, vi.getName()); + } rtc.checkSMT(c, invocation); } } From 29f4c179f56f30200bcb766af00c4c522ba90abd Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 23 Oct 2025 15:40:23 +0100 Subject: [PATCH 2/2] Add IndexOutOfBounds Tests --- .../ArrayListRefinements.java | 18 ++++++++++++++++++ .../index_out_of_bounds_correct/Test.java | 11 +++++++++++ .../ArrayListRefinements.java | 18 ++++++++++++++++++ .../index_out_of_bounds_error/Test.java | 10 ++++++++++ 4 files changed, 57 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_correct/ArrayListRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_correct/Test.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/ArrayListRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/Test.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_correct/ArrayListRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_correct/ArrayListRefinements.java new file mode 100644 index 00000000..bf886502 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_correct/ArrayListRefinements.java @@ -0,0 +1,18 @@ +package testSuite.classes.index_out_of_bounds_correct; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Ghost; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; + +@ExternalRefinementsFor("java.util.ArrayList") +@Ghost("int size") +public interface ArrayListRefinements { + + public void ArrayList(); + + @StateRefinement(to = "size(this) == size(old(this)) + 1") + public boolean add(E elem); + + public E get(@Refinement("_ < size(this)") int index); +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_correct/Test.java b/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_correct/Test.java new file mode 100644 index 00000000..99abdc3d --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_correct/Test.java @@ -0,0 +1,11 @@ +package testSuite.classes.index_out_of_bounds_correct; + +import java.util.ArrayList; + +public class Test { + public static void main(String[] args) { + ArrayList l = new ArrayList<>(); + l.add(1); + l.get(0); + } +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/ArrayListRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/ArrayListRefinements.java new file mode 100644 index 00000000..12bf3c69 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/ArrayListRefinements.java @@ -0,0 +1,18 @@ +package testSuite.classes.index_out_of_bounds_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Ghost; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; + +@ExternalRefinementsFor("java.util.ArrayList") +@Ghost("int size") +public interface ArrayListRefinements { + + public void ArrayList(); + + @StateRefinement(to = "size(this) == size(old(this)) + 1") + public boolean add(E elem); + + public E get(@Refinement("_ < size(this)") int index); +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/Test.java b/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/Test.java new file mode 100644 index 00000000..eb61dfae --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/Test.java @@ -0,0 +1,10 @@ +package testSuite.classes.index_out_of_bounds_error; + +import java.util.ArrayList; + +public class Test { + public static void main(String[] args) { + ArrayList l = new ArrayList<>(); + l.get(0); // index out of bounds + } +} \ No newline at end of file