ESC/Java2 doesn't recognize generics, new for loop and external libraries

[atiti]

Hello,

I just installed Mobius in my Eclipse environment (using the Eclipse update site), opened the "Verification" perspective, and ran ESC/Java2 Simplify & Z3 on some Java projects.

I did first configure Simplify and Z3 to use the win32 version, and ESC/Java2 to support Java 1.6.

However, Simplify and Z3 are failing on these things:

• Iterator<Map.Entry<String, String>> iterator <- it has a problem with the comma: Fatal error: Unexpected token ',', expected ';' Iterator<Map.Entry<String, String>> iterator = ... ^
• for (DataObject rowItem : drsSearchResults.getRows()) { <- it has a problem with the colon: Fatal error: Unexpected token ':', expected ';' for (DataObject rowItem : drsSearchResults.getRows()) ... ^
• Fatal error: Unexpected token '{', expected ',' public enum Status{ ^
• Fatal error: Expected an identifier, found < private final List m_slices; ^
• It also doesn't recognize an imported library (a zip file) which Eclipse does recognize: Error: No such type: intradoc.common.SystemUtils import intradoc.common.SystemUtils; ^

These are the versions I have installed in Eclipse: Extended Static Checking 2.1.6 mobius.esc.feature.group Prover Editor 1.0.13 mobius.provereditor.feature.group Automated Theorem Provers 0.2.22 mobius.atp.feature.group RequiredPlugins Feature 1.0.10 mobius.required.feature.group RequiredPlugins Feature 1.0.10 mobius.required.feature.group

Am I doing something wrong? Or are these features not supported yet by ESC/Java2?

Thanks, Ludovic

[atiti]

From: kiniry (GH: kiniry) Date: Mon Jun 28 14:40:11 2010

As documented in the ESC/Java2 documentations and FAQ, ESC/Java2 does not support reasoning about Java 1.5+ source. You are consuming Java 1.5+ source in your example, as I see parameterized classes in your error message above. If you are attempting to reason about Java 1.4 source on a JDK 1.5+ VM, please let me know and I'll help you wish such.