jstar eclipse plugin
Yevgeniy
I am a researcher at the AT&T security research center in new york.
We've been exploring the possibility of using JStar to verify java
code for one of our projects. It seems like a very powerful tool!
I've run into some trouble using the eclipse plugin: when trying to
run verification from inside eclipse on the LinkedList example and
unfortunately I get the following errors:
"
Fatal error: exception Assert_failure("corestar_src/utils/system.ml",
105, 2)
Exited with error code 2
Fatal error: exception Assert_failure("corestar_src/utils/system.ml",
105, 2)
Exited with error code 2
jStar Verification is completed.
"
I'm not sure how to interpret this: did JStar crash? Or was the
verification completed successfully?
Another issue that I'm having is that the very convenient looking
completion and templates that I saw in your demo video don't seem to
be working.
A final mystery is the "smt solver executable" field in the jstar
settings. The documentation seems to be referring to a version that
did not have this field, and I'm not sure what to put there.
Your input on any of the above issues will be greatly appreciated!
Best regards,
Yevgeniy Vahlis
Radu Grigore
> I get the following errors:
> Fatal error: exception Assert_failure("corestar_src/utils/system.ml",> 105, 2)
> I'm not sure how to interpret this: did JStar crash? Or was the
> verification completed successfully?
It crashed. Please submit an issue so we can ask for further info if
needed when we try to fix it. My guess, given the assertion that
fails, is that it has something to do with the SMT solver it tries to
run. These things tend to vary from one platform to another, which is
why we might need more information.
https://github.com/seplogic/corestar/issues
> Another issue that I'm having is that the very convenient looking
> completion and templates that I saw in your demo video don't seem to
> be working.
Oh, I created those code templates on my computer for the sole purpose
of making the video. You are right that we should look into shipping
them.
http://www.java-tips.org/other-api-tips/eclipse/how-to-add-your-own-code-template-in-eclipse.html
> A final mystery is the "smt solver executable" field in the jstar
> settings. The documentation seems to be referring to a version that
> did not have this field, and I'm not sure what to put there.
We use Z3 with the flags "/smt2 /in".
http://research.microsoft.com/en-us/um/redmond/projects/z3/
Note that it works with wine under non-windows operating systems.