Skip to content

Commit ffc24f8

Browse files
committed
Fix StateSet in Interface without ExternalRefinements
1 parent 3ac0f36 commit ffc24f8

2 files changed

Lines changed: 20 additions & 21 deletions

File tree

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.StateSet;
4+
5+
@StateSet({"idle", "running"})
6+
public interface CorrectInterfaceStateSet {
7+
}

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java

Lines changed: 13 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -263,40 +263,32 @@ private void createStateGhost(String string, CtElement element, SourcePosition p
263263
}
264264

265265
protected String getQualifiedClassName(CtElement element) {
266-
if (element.getParent() instanceof CtClass<?>) {
267-
return ((CtClass<?>) element.getParent()).getQualifiedName();
268-
} else if (element instanceof CtClass<?>) {
269-
return ((CtClass<?>) element).getQualifiedName();
270-
}
271-
return null;
266+
return getEnclosingType(element).map(CtType::getQualifiedName).orElse(null);
272267
}
273268

274269
protected String getSimpleClassName(CtElement element) {
275-
if (element.getParent() instanceof CtClass<?>) {
276-
return ((CtClass<?>) element.getParent()).getSimpleName();
277-
} else if (element instanceof CtClass<?>) {
278-
return ((CtClass<?>) element).getSimpleName();
279-
}
280-
return null;
270+
return getEnclosingType(element).map(CtType::getSimpleName).orElse(null);
281271
}
282272

283273
protected Optional<GhostFunction> createStateGhost(int order, CtElement element) {
284-
CtClass<?> klass = null;
285-
if (element.getParent() instanceof CtClass<?>) {
286-
klass = (CtClass<?>) element.getParent();
287-
} else if (element instanceof CtClass<?>) {
288-
klass = (CtClass<?>) element;
289-
}
290-
if (klass != null) {
274+
Optional<CtType<?>> enclosingType = getEnclosingType(element);
275+
if (enclosingType.isPresent()) {
276+
CtType<?> type = enclosingType.get();
291277
CtTypeReference<?> ret = factory.Type().INTEGER_PRIMITIVE;
292-
List<String> params = Collections.singletonList(klass.getSimpleName());
278+
List<String> params = Collections.singletonList(type.getSimpleName());
293279
String name = String.format("state%d", order);
294-
GhostFunction gh = new GhostFunction(name, params, ret, factory, klass.getQualifiedName());
280+
GhostFunction gh = new GhostFunction(name, params, ret, factory, type.getQualifiedName());
295281
return Optional.of(gh);
296282
}
297283
return Optional.empty();
298284
}
299285

286+
private Optional<CtType<?>> getEnclosingType(CtElement element) {
287+
if (element instanceof CtType<?> type)
288+
return Optional.of(type);
289+
return Optional.ofNullable(element.getParent(CtType.class));
290+
}
291+
300292
protected void getGhostFunction(String value, CtElement element, SourcePosition position) throws LJError {
301293
GhostDTO f = getGhostDeclaration(value, position);
302294
CtType<?> type = element instanceof CtType<?> t ? t : element.getParent()instanceof CtType<?> t ? t : null;

0 commit comments

Comments
 (0)