diff --git a/liquidjava-example/src/main/java/testSuite/CorrectInterfaceStateSet.java b/liquidjava-example/src/main/java/testSuite/CorrectInterfaceStateSet.java new file mode 100644 index 00000000..8e4e9dcc --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectInterfaceStateSet.java @@ -0,0 +1,7 @@ +package testSuite; + +import liquidjava.specification.StateSet; + +@StateSet({"idle", "running"}) +public interface CorrectInterfaceStateSet { +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 7ff64f38..4935b457 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -263,40 +263,32 @@ private void createStateGhost(String string, CtElement element, SourcePosition p } protected String getQualifiedClassName(CtElement element) { - if (element.getParent() instanceof CtClass) { - return ((CtClass) element.getParent()).getQualifiedName(); - } else if (element instanceof CtClass) { - return ((CtClass) element).getQualifiedName(); - } - return null; + return getEnclosingType(element).map(CtType::getQualifiedName).orElse(null); } protected String getSimpleClassName(CtElement element) { - if (element.getParent() instanceof CtClass) { - return ((CtClass) element.getParent()).getSimpleName(); - } else if (element instanceof CtClass) { - return ((CtClass) element).getSimpleName(); - } - return null; + return getEnclosingType(element).map(CtType::getSimpleName).orElse(null); } protected Optional createStateGhost(int order, CtElement element) { - CtClass klass = null; - if (element.getParent() instanceof CtClass) { - klass = (CtClass) element.getParent(); - } else if (element instanceof CtClass) { - klass = (CtClass) element; - } - if (klass != null) { + Optional> enclosingType = getEnclosingType(element); + if (enclosingType.isPresent()) { + CtType type = enclosingType.get(); CtTypeReference ret = factory.Type().INTEGER_PRIMITIVE; - List params = Collections.singletonList(klass.getSimpleName()); + List params = Collections.singletonList(type.getSimpleName()); String name = String.format("state%d", order); - GhostFunction gh = new GhostFunction(name, params, ret, factory, klass.getQualifiedName()); + GhostFunction gh = new GhostFunction(name, params, ret, factory, type.getQualifiedName()); return Optional.of(gh); } return Optional.empty(); } + private Optional> getEnclosingType(CtElement element) { + if (element instanceof CtType type) + return Optional.of(type); + return Optional.ofNullable(element.getParent(CtType.class)); + } + protected void getGhostFunction(String value, CtElement element, SourcePosition position) throws LJError { GhostDTO f = getGhostDeclaration(value, position); CtType type = element instanceof CtType t ? t : element.getParent()instanceof CtType t ? t : null;