Skip to content

Commit

Permalink
method names should not be created via VariableRenamer
Browse files Browse the repository at this point in the history
  • Loading branch information
unp1 committed Jul 28, 2023
1 parent 40d836c commit efc11ce
Showing 1 changed file with 1 addition and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -847,7 +847,7 @@ public NullLiteral convert(recoder.java.expression.literal.NullLiteral nullLit)

/** convert a recoder Identifier to a KeY Identifier */
public ProgramElementName convert(recoder.java.Identifier id) {
return VariableNamer.parseName(id.getText(), collectComments(id).collect(Comment.class));
return new ProgramElementName(id.getText(), collectComments(id).collect(Comment.class));
}

public ProgramElementName convert(ImplicitIdentifier id) {
Expand Down

0 comments on commit efc11ce

Please sign in to comment.