Entry points with SMACK-escaped character

[jjgarzella]

Right now, SMACK does not support having the entry point function have a character which Naming.cpp will escape. The problem is that the entry point annotation is done in top.py, which doesn't know about the escaping mechanism that llvmtobpl uses.

If a user specified an entry point with a colon in it, for example didMoveToView:, llvmtobpl currently changes that colon to an underscore (didMoveToView_) for it's purposes. However, when top.py tries to match this name to annotate it, the name doesn't match, because top.py doesn't know about the escape.

This is a problem in practice, methods with special characters in their name occur in almost every Objective-C and Kotlin method.

Current workaround: Add a command line option to manually specify the escaped entry points. This means that for an entry point with special characters, the user has to type in in twice, once normal and once escaped.

Proposed solutions:

1. make the escaping utility available to top.py through some type of utility
2. factor the annotations of boogie methods into llvmtobpl

[shaobo-he]

@jjgarzella is this issue resolved?

[jjgarzella]

@shaobo-he As far as I know, no. For example the VMCAI artifact uses the workaround with the manual command line option.

However, this only really affects Kotlin support, so it should not be a priority to fix.

[shaobo-he]

@shaobo-he As far as I know, no. For example the VMCAI artifact uses the workaround with the manual command line option.

However, this only really affects Kotlin support, so it should not be a priority to fix.

Thanks, JJ. So I will keep this issue open though we may not fix it anytime soon.