You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository was archived by the owner on Jul 4, 2026. It is now read-only.
Repository navigation
This repository was archived by the owner on Jul 4, 2026. It is now read-only.
Thanks for the repository. For my project, I need to translate jml to java code (into assertions). Unfortunately there is no documentation. I wanted to ask you
How do I build this into a jar usable from Java?
How can I use your jml2java module from Java?
I tried
# gradle init
gradle build
but I end up getting a few-byte jar file both with and without init. Also, the Github action build keeps failing too so that's not helping either.
You can use the regular Gradle targets, e.g., gradle classes, testClasses, or assemble to compile the class files, and also the test classes, or to finally build all artifacts. I also fixed some compiler errors.
The functionalities are rather in an unfinished state. For example you mentioned jml2java module: Some expressions are supported, but support for complicated constructs (especially, \old) is absent.
Currently, we are migrating JJBMC from openjml to jmlparser, which also implements a jml2java conversion feature, but designed for bounded model checker (e.g., use of nondet. variables).
Activity
[-]Need help building and using this[/-][+]Building issues[/+]wadoon commentedon May 11, 2024
You can use the regular Gradle targets, e.g.,
gradle classes,testClasses, orassembleto compile the class files, and also the test classes, or to finally build all artifacts. I also fixed some compiler errors.The functionalities are rather in an unfinished state. For example you mentioned
jml2javamodule: Some expressions are supported, but support for complicated constructs (especially,\old) is absent.Currently, we are migrating JJBMC from openjml to jmlparser, which also implements a jml2java conversion feature, but designed for bounded model checker (e.g., use of nondet. variables).
/cc @JonasKlamroth