#47 JML4 without Eclipse

[jerome white]

Is it possible to use JML4 without eclipse? That is, via the command line. If so, what steps do I need to take?

[jlee]

Yes, you can use JML4 without Eclipse.

At Kansas State University, we are using JML4 to develop a symbolic-execution-based software verification tool, Kiasan, and Kiasan can be run through the terminal. You need to check out three projects, org.eclipse.jdt.core, org.jmlspecs.annotation,and org.jmlspecs.jml4.runtime. (The org.jmlspecs.annotation project was introduced to substitute org.jmlspecs.jml4.runtime, but I am not sure if this substitution is completely done at this point.) To the best of our knowledge, there is one location in the code that introduces the dependency on Eclipse. This location is at JmlFileFinder.java's line number 54-57. NameEnvironment used at this location imports Eclipse-dependent classes. Once you comment out this location, you should be able to create a jar file using a script, org.eclipse.jdt.core/scripts/export-ecj.xml.

[Gary T. Leavens]

Thanks Jooyong Lee for the comment. Patrice, I'm assigning this to you in case you have anything further to add, or if you want to make the dependency on Eclipse a bug report to fix. If you don't then you can close this.
- Gary

[jerome white]

Thanks Jooyong.

First, org.jmlspecs.annotation doesn't seem to exist; at least from the repository directory I'm checking out from: https://jmlspecs.svn.sourceforge.net/svnroot/jmlspecs/jml4/branches/3.3/ - is this the correct directory?

Secondly, I'm not quite sure where to alter JmlFileFinder (org.eclipse.jdt.core/compiler/org/jmlspecs/jml4/lookup/JmlFileFinder.java). In the version I have (from the repository location listed above) lines 54 through 57 are as follows:

<pre>
private File[] strings2files(String[] path) {
List list = new ArrayList(path.length);
for (int i=0, length=path.length; i < length; i++) {
String filename = path[i];
</pre>
Lines that deal with the "NameEnvironment" variable are just above that, 43 through 53:
<pre>
INameEnvironment iNameEnvironment= compiler.lookupEnvironment.n\ ameEnvironment;
//TODO: consider changing the ref to NameEnvironment below
// to a JML-specific subclass that has these 2 methods
if (iNameEnvironment instanceof NameEnvironment) {
NameEnvironment nameEnvironment = (NameEnvironment) iNa\ meEnvironment;
sourcePath = strings2files(nameEnvironment.getSourcePat\ h());
}
else {
sourcePath = emptyFileArray;
}
</pre>
What should I be changing?

[Gary T. Leavens]

I think in the SVN for the jmlspecs project there is a directory JMLAnnotations and from it's trunk you can find src/org/jmlspecs/annotation.

I don't know about the second problem and hope that someone else can help solve it...

[Patrice Chalin]

You can still make use of the batch compiler interface even without removing those lines, thought it is a bit more involved. In any case, I suspect that Jooyong meant to comment out the lines like this:

54: /* if (iNameEnvironment instanceof NameEnvironment) {
55: NameEnvironment nameEnvironment = ...
56: this.sourcePath = ...
57: this.sourceNameEnv = ...
58: } else */ if (iNameEnvironment instanceof FileSystem) {

but you will need to confirm with him as I have not tried it myself.

It may well be worth eliminating this dependency if possible. Keeping this ticket open as a reminder.