Enum types are used in examples (Order.java enum Status, UserProfile.java enum Theme / enum AccountType) and are a standard Java feature that no current JVerify issue covers.
Current state:
MissingContractCompiler.visitReference explicitly skips enum members with the comment "Do not add enum members, since enums are translated to datatypes". Actual enum translation to Laurel Datatype + DatatypeConstructor commands is not implemented in JavaToLaurelCompiler.- The comment reveals the intended design: map Java enums to Laurel datatypes with zero-arg constructors per enum case.
Work required:
JavaToLaurelCompiler.analyzeJavaCode: detect enum-flagged JCClassDecl (via Flags.ENUM).- Emit a
Command.DatatypeCommand with a Datatype whose constructors are zero-arg constructors named after each enum constant.
- Handle enum-constant reads and comparisons as constructor references.
Dependencies:
Enum types are used in examples (
Order.javaenum Status,UserProfile.javaenum Theme/enum AccountType) and are a standard Java feature that no current JVerify issue covers.Current state:
MissingContractCompiler.visitReferenceexplicitly skips enum members with the comment "Do not add enum members, since enums are translated to datatypes". Actual enum translation to LaurelDatatype+DatatypeConstructorcommands is not implemented inJavaToLaurelCompiler.Work required:
JavaToLaurelCompiler.analyzeJavaCode: detect enum-flaggedJCClassDecl(viaFlags.ENUM).Command.DatatypeCommandwith aDatatypewhose constructors are zero-arg constructors named after each enum constant.Dependencies:
Datatype,DatatypeConstructor,DatatypeConstructorListare all already inorg.strata.jverify.laurel.