如何查看OpenJML错误信息？Eclipse运行测试遇空指针异常求助

一、如何查看OpenJML的错误信息 #

OpenJML的错误信息可以通过几种方式获取，不同场景下各有用途：

• Eclipse插件内置视图：当你用OpenJML分析代码时，所有的JML规范错误、警告都会直接显示在Eclipse的Problems视图中。每条信息都会标注对应的代码文件、行号，以及具体的违规原因（比如前置条件不满足、类不变量被破坏等），双击条目就能直接跳转到问题代码位置。
• 命令行详细输出：如果习惯用命令行操作，运行openjml时加上-verbose或-showWarnings参数，控制台会输出完整的错误详情，包括精确的行号和规范违规描述。示例命令：

  openjml -verbose -check YourTargetJavaFile.java
  

• 运行时断言检查（RAC）：若要捕获运行时的JML规范违反，编译代码时加上-rac参数，运行程序时会触发断言并抛出异常，异常信息里会包含违规的代码位置和具体原因。

二、解决你遇到的NullPointerException问题 #

从你提供的栈跟踪来看，这个空指针出现在OpenJML初始化规范路径时，无法正确获取Eclipse平台的Bundle信息，这通常是版本不兼容或插件安装不完整导致的，给你几个排查方向：

• 核对版本兼容性：你使用的是JRE 1.8，建议确认OpenJML插件版本是否适配你的Eclipse版本。比如OpenJML 0.19.x系列对Java 8和Eclipse 2019-09及更早版本的兼容性更好，避免用过高版本的OpenJML搭配旧版Eclipse。
• 重新安装OpenJML插件：可能插件安装过程中依赖组件丢失，先卸载现有插件，再从官方更新站点重新安装，确保所有关联组件都被正确加载。
• 手动指定规范路径：如果自动初始化规范路径失败，可以在Eclipse的OpenJML设置中，手动指定JML规范文件所在的jmlspecs目录路径，绕过插件自动查找的逻辑。
• 用正确的方式运行测试：不要用普通JUnit运行器执行OpenJML测试，右键测试类后选择Run As > OpenJML Test，这样才能加载OpenJML的完整运行环境。

当你解决了这个空指针问题后，正常运行OpenJML测试时，只要代码存在JML规范违反，测试结果会清晰标注对应的代码文件、行号以及具体的问题类型，完全满足你想要的定位需求。

内容的提问来源于stack exchange，提问作者Siri Framboise