diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_refinement_no_to_correct/ArrayListRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_refinement_no_to_correct/ArrayListRefinements.java new file mode 100644 index 00000000..493490f5 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_refinement_no_to_correct/ArrayListRefinements.java @@ -0,0 +1,22 @@ +package testSuite.classes.state_refinement_no_to_correct; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.RefinementPredicate; +import liquidjava.specification.StateRefinement; + +@ExternalRefinementsFor("java.util.ArrayList") +public interface ArrayListRefinements { + + @RefinementPredicate("int size(ArrayList l)") + @StateRefinement(to = "size(this) == 0") + public void ArrayList(); + + @StateRefinement(to = "size(this) == size(old(this)) + 1") + public boolean add(E e); + + @StateRefinement(from = "size(this) > 0") + public E get(int index); + + @StateRefinement(from = "size(this) == 2", to = "size(this) == size(old(this)) - 1") + public E remove(int index); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_refinement_no_to_correct/Test.java b/liquidjava-example/src/main/java/testSuite/classes/state_refinement_no_to_correct/Test.java new file mode 100644 index 00000000..8854afb8 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_refinement_no_to_correct/Test.java @@ -0,0 +1,13 @@ +package testSuite.classes.state_refinement_no_to_correct; + +import java.util.ArrayList; + +public class Test { + public void example() { + ArrayList list = new ArrayList<>(); + list.add(1); + list.add(2); + list.get(0); + list.remove(0); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_refinement_no_to_typestate_correct/Counter.java b/liquidjava-example/src/main/java/testSuite/classes/state_refinement_no_to_typestate_correct/Counter.java new file mode 100644 index 00000000..799fae7d --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_refinement_no_to_typestate_correct/Counter.java @@ -0,0 +1,23 @@ +package testSuite.classes.state_refinement_no_to_typestate_correct; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"empty", "one", "many"}) +public class Counter { + + @StateRefinement(to="empty(this)") + public Counter() {} + + @StateRefinement(from="empty(this)", to="one(this)") + public void addFirst() {} + + @StateRefinement(from="one(this)", to="many(this)") + public void addSecond() {} + + @StateRefinement(from="one(this) || many(this)") + public void inspect() {} + + @StateRefinement(from="many(this)") + public void consumeOne() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_refinement_no_to_typestate_correct/Test.java b/liquidjava-example/src/main/java/testSuite/classes/state_refinement_no_to_typestate_correct/Test.java new file mode 100644 index 00000000..f063d889 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_refinement_no_to_typestate_correct/Test.java @@ -0,0 +1,12 @@ +package testSuite.classes.state_refinement_no_to_typestate_correct; + +public class Test { + + public void test() { + Counter counter = new Counter(); + counter.addFirst(); + counter.addSecond(); + counter.inspect(); + counter.consumeOne(); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java index 45ac6c68..c64ba3d6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java @@ -55,7 +55,9 @@ public void setMessage(String message) { } public ObjectState clone() { - return new ObjectState(from.clone(), to.clone(), message); + Predicate clonedFrom = from == null ? null : from.clone(); + Predicate clonedTo = to == null ? null : to.clone(); + return new ObjectState(clonedFrom, clonedTo, message); } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 9d435dff..b96e6239 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -182,10 +182,6 @@ private static ObjectState getStates(CtAnnotation ctAnnota if (to != null) state.setTo(createStatePredicate(to, f.getTargetClass(), tc, e, true, prefix)); - // has from but not to, state remains the same - if (from != null && to == null) - state.setTo(createStatePredicate(from, f.getTargetClass(), tc, e, true, prefix)); - // has to but not from, state enters with true if (from == null && to != null) state.setFrom(new Predicate()); @@ -616,4 +612,4 @@ private static List> getStateAnnotation(CtEle .getCanonicalName().contentEquals("liquidjava.specification.StateRefinement")) .collect(Collectors.toList()); } -} \ No newline at end of file +}