Unable to verify Java method using the fully qualified name

[orionpapadakis]

CBMC version: 5.58.1
Operating system: Ubuntu 20.04 - kernel 5.15.0-52-generic
Exact command line resulting in the issue: JBMC_BIN --classpath $JAVA_MODEL:./$TESTS my.petty.examples.SimpleMethod.foo:(Ljava/lang/String;)Z --unwind 5
What behaviour did you expect: To verify the method.
What happened instead: bash: syntax error near unexpected token ('`

The code of the method is:

public boolean foo(String m) {
        return m.equals("AB");
}

[tautschnig]

You will need to use quotes, this isn't really a problem we can handle on the JBMC side, it's your shell. (Other than us mangling names so that they don't contain characters the shell tries to interpret.) Here is what worked for me:

$ cat SimpleMethod.java
class SimpleMethod
{
  public boolean foo(String m) {
    return m.equals("AB");
  }
}
$ javac SimpleMethod.java
$ jbmc --function 'SimpleMethod.foo:(Ljava/lang/String;)Z' SimpleMethod
JBMC version 5.69.1 (cbmc-5.69.1-55-g022930703c) 64-bit x86_64 linux
Parsing ...
Trying to load Java main class: SimpleMethod
Found Java main class: SimpleMethod
[...]
VERIFICATION FAILED

[orionpapadakis]

Thank you for your answer. Actually I was missing 2 things:

1. the quotes, as you say
2. pass the the class name as argument, after the fully classified name of the method.

I kindly suggest to add an example to your documentation because none of the above is clear.

[peterschrammel]

There are multiple equivalent ways of calling JBMC. The simplest one is just to pass the fully qualified method name (if necessary with the descriptor if you have overloads).
So, JBMC_BIN --classpath $JAVA_MODEL:./$TESTS my.petty.examples.SimpleMethod.foo --unwind 5 should just work.
Surely, this can be better explained in the docs.

[orionpapadakis]

Indeed, that is the simplest way (and easily understood from the documentation). However, it is usual in Java to have multiple methods with the same name but with different signature. In such a case the fully qualified name of a method is the only way to be clear.