1

我想使用另一个 java 项目中的 JPF（Java 路径查找器）。

我已经完成的步骤：

  1. 我创建了一个新的 Java 项目

  2. 在构建路径中引用了 jpf-core。

  3. 创建了一个 java 类（Test.java）打印 Hello world（在我的新项目中）。

  4. 在我提到的目标 = 测试中创建了一个 .jpf 文件（Test.jpf）。

  5. 在我提到的eclipse启动配置中

    project = jpf-core
Main Class = gov.nasa.jpf.tool.RunJPF

我的问题是如果我将相同的 .java 文件和 .jpf 文件放在 jpf-core 项目的 jpf-core/examples 包中，我就可以运行 jpf 文件并获得结果。但是当我试图从另一个 java 项目运行 .jpf 时，我无法这样做。我收到以下错误

[SEVERE] can't find startup class: Test`
[SEVERE] error initializing startup classes (check 'classpath')

请帮我解决这个问题。

更新：

我是否必须编写任何属性文件来提及我的测试类文件的类路径？如果我这样写，我如何将它们与 jpf.properties 联系起来？

4

2 回答 2

2

我希望这还不算太晚。我正在为 JPF 使用 Eclipse 插件。
从另一个 java 项目运行 JPF。我需要创建一个 jpf.properties 文件来设置配置。使用 eclipse 插件，它可以在创建 JPF 项目时自动生成。在 jpf.properties 文件中，需要将 .classpath 和 .sourcepath 配置设置为您的测试文件（总是从 build\XXX 开始，因为 JPF 正在加载 java 字节码）。然后右键单击.jpf 文件并单击“验证”（eclipse 插件）。在此之前，我需要告诉 eclipse jpf-core 目录。只需创建一个 site.properties 文件并编写“jpf-core = your JPFdirectory”即可。谢谢你。
正如 JPF 权威所建议的那样，JPF 通过插件支持更容易、更快捷。

于 2012-12-19T08:20:25.277 回答
0

您的其他项目需要引用包含 Test 类的项目。否则它显然不在类路径上。检查 Build-Path 下的 Project 选项卡。

于 2011-08-22T13:49:01.467 回答