-
Notifications
You must be signed in to change notification settings - Fork 8
Open
Labels
Description
At the moment JML annotations generated by Beetlz are essentially for JML2 version 5.4 and earlier and ESC/Java2. E.g., references are nullable by default. The annotations currently generated do not work with, for example, JML4c, as it does not understand non_null and nullable_by_default.
I suggest we add a new -target switch whose value can be one of JML2, ESCJava2, JML4c, or OpenJML.
I also suggest we add a new switch comparable to JML2's --nonnulltypes (-j) switch to enable and disable default non-null semantics for JML2 generation.