GUI - cryptic messages in GUI at OpenJML analysis and parsing
Using the current GUI and the mythaistar project:
-
When I parse main.java with javaparser through I get
1612978475497 - javaParser called with Main.java -> Error
Why is this?
The same happens with the files Example1.java and UserManagementImpl.java
-
when I run OpenJML on the same file Main.java, already in the mythaistar project, I get
1612978832046 - OpenJML called with Main.java -> Created
Likewise, when I run OpenJML on BankingExample.java I get
1612979253824 - OpenJML called with BankingExample.java -> Created
What does this mean? In the first one, the analysis is obviously successful as there are no annotations in the code, but in the second example, the analysis goes wrong. Indeed, when I run the second analysis manually (i.e. from my terminal with OpenJML installed locally) on the same file, I get:
$ openjml banking.java
banking.java:1: error: class BankingExample is public, should be declared in a file named BankingExample.java
public class BankingExample {
^
banking.java:45: error: cannot find symbol
public /*@ pure @*/ int getBalance() throws BankingException {
^
symbol: class BankingException
location: class BankingExample
banking.java:10: error: Implicit references to 'this' are not permitted in constructor assignable clauses: balance
//@ assignable balance;
^
banking.java:44: error: cannot find symbol
//@ signals_only BankingException;
^
symbol: class BankingException
location: class BankingExample
banking.java:50: error: cannot find symbol
throw new BankingException();
^
symbol: class BankingException
location: class BankingExample
5 errors
- I think we should have the results of the OpenJML analyses stored in the Logs collection of the PKM, one item per error, so that the GUI can display it, e.g. as any artefact.
What do you think?