diff --git a/liquidjava-example/src/main/java/testSuite/CorrectStringConcat.java b/liquidjava-example/src/main/java/testSuite/CorrectStringConcat.java new file mode 100644 index 00000000..3a9596a7 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectStringConcat.java @@ -0,0 +1,8 @@ +package testSuite; + +public class CorrectStringConcat { + + void example() { + System.out.println("Hello, " + "World!"); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index 94c6a830..bfdfa173 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -87,6 +87,8 @@ public void getBinaryOpRefinements(CtBinaryOperator operator) throws Pars operator.putMetadata(rtc.REFINE_KEY, Predicate.createEquals(Predicate.createVar(rtc.WILD_VAR), oper)); } else if (types.contains(type)) { operator.putMetadata(rtc.REFINE_KEY, Predicate.createEquals(Predicate.createVar(rtc.WILD_VAR), oper)); + } else if (type.equals("java.lang.String")) { + // skip strings } else { throw new NotImplementedException("Literal type not implemented"); } @@ -238,6 +240,10 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab } else if (element instanceof CtLiteral) { CtLiteral l = (CtLiteral) element; + if (l.getType().getQualifiedName().equals("java.lang.String")) { + // skip strings + return new Predicate(); + } return new Predicate(l.getValue().toString(), element, rtc.getErrorEmitter()); } else if (element instanceof CtInvocation) {