2

我尝试按照说明从 github 上的 README.md 文件为 MacOSX (yosemite) 构建 leon。

它运行良好，除了当我运行基本测试时，我遇到了一个找不到 scalaz3 库的问题：

 $ ./leon ./testcases/verification/sas2011-testcases/RedBlackTree.scala
java.lang.UnsatisfiedLinkError: no scalaz3 in java.library.path
    at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1865)
    at java.lang.Runtime.loadLibrary0(Runtime.java:870)
    at java.lang.System.loadLibrary(System.java:1122)
    at z3.Z3Wrapper.loadFromJar(Z3Wrapper.java:97)
    at z3.Z3Wrapper.<clinit>(Z3Wrapper.java:47)
    at z3.scala.Z3Config.<init>(Z3Config.scala:6)
    at leon.solvers.z3.FairZ3Solver.<init>(FairZ3Solver.scala:50)
    at leon.solvers.SolverFactory$$anonfun$leon$solvers$SolverFactory$$getSolver$1$1$$anon$1.<init>(SolverFactory.scala:50)
    at leon.solvers.SolverFactory$$anonfun$leon$solvers$SolverFactory$$getSolver$1$1.apply(SolverFactory.scala:50)
    at leon.solvers.SolverFactory$$anonfun$leon$solvers$SolverFactory$$getSolver$1$1.apply(SolverFactory.scala:50)
    at leon.solvers.SolverFactory$$anon$12.getNewSolver(SolverFactory.scala:18)
    at leon.verification.AnalysisPhase$.checkVC(AnalysisPhase.scala:129)
    at leon.verification.AnalysisPhase$$anonfun$10.apply(AnalysisPhase.scala:111)
    at leon.verification.AnalysisPhase$$anonfun$10.apply(AnalysisPhase.scala:110)
    at scala.collection.TraversableLike$WithFilter$$anonfun$map$2.apply(TraversableLike.scala:728)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$WithFilter.map(TraversableLike.scala:727)
    at leon.verification.AnalysisPhase$.checkVCs(AnalysisPhase.scala:110)
    at leon.verification.AnalysisPhase$.run(AnalysisPhase.scala:45)
    at leon.verification.AnalysisPhase$.run(AnalysisPhase.scala:15)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:12)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:12)
    at leon.Main$.execute(Main.scala:236)
    at leon.Main$.main(Main.scala:220)
    at leon.Main.main(Main.scala)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:497)
    at scala.reflect.internal.util.ScalaClassLoader$$anonfun$run$1.apply(ScalaClassLoader.scala:70)
    at scala.reflect.internal.util.ScalaClassLoader$class.asContext(ScalaClassLoader.scala:31)
    at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.asContext(ScalaClassLoader.scala:101)
    at scala.reflect.internal.util.ScalaClassLoader$class.run(ScalaClassLoader.scala:70)
    at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.run(ScalaClassLoader.scala:101)
    at scala.tools.nsc.CommonRunner$class.run(ObjectRunner.scala:22)
    at scala.tools.nsc.ObjectRunner$.run(ObjectRunner.scala:39)
    at scala.tools.nsc.CommonRunner$class.runAndCatch(ObjectRunner.scala:29)
    at scala.tools.nsc.ObjectRunner$.runAndCatch(ObjectRunner.scala:39)
    at scala.tools.nsc.MainGenericRunner.runTarget$1(MainGenericRunner.scala:65)
    at scala.tools.nsc.MainGenericRunner.run$1(MainGenericRunner.scala:87)
    at scala.tools.nsc.MainGenericRunner.process(MainGenericRunner.scala:98)
    at scala.tools.nsc.MainGenericRunner$.main(MainGenericRunner.scala:103)
    at scala.tools.nsc.MainGenericRunner.main(MainGenericRunner.scala)

我尝试从 EPFL 构建 ScalaZ3 包，这需要构建 Microsoft 的 Z3（来自 github）。构建 z3 本身可以找到，但构建 ScalaZ3 失败，缺少“gomp”库：

[error] ld: library not found for -lgomp
[error] clang: error: linker command failed with exit code 1 (use -v to see invocation)
[info] Bundling files:
[info]  - /Users/rouquett/git.leon/ScalaZ3/lib-bin/libscalaz3.dylib -> lib-bin/libscalaz3.dylib
[info]  - /Users/rouquett/git.leon/ScalaZ3/z3/4.3-osx-64b/lib/libz3.dylib -> lib-bin/libz3.dylib
[info]  - /Users/rouquett/git.leon/ScalaZ3/z3/4.3-osx-64b/lib/python2.7 -> lib-bin/python2.7
[info] Packaging /Users/rouquett/git.leon/ScalaZ3/target/scala-2.10/scalaz3_2.10-2.1.jar ...
[info] Done packaging.

我发现这里有一个适用于 MacOSX 的 Clang OMP 库：

http://brewformulas.org

但是，这可能需要调整一些构建脚本以指向 brew 安装的 clang-omp。

有没有人遇到过或解决过类似的问题？

  • 尼古拉斯。
4

1 回答 1

3

这些是我在 OSX 上运行最新版本的 Leon 所遵循的步骤：

git clone git@github.com:epfl-lara/leon.git
cd leon
git remote add osx git@github.com:mantognini/leon.git
git fetch osx
git checkout osx
git rebase origin/master # adds precompiled OSX binaries
sbt clean compile script

确保将leon二进制文件链接到您的$PATH，例如在最后一步运行之后ln -sv $(pwd)/leon /usr/local/bin/leon。

要将二进制文件更新到最新版本的 Leon，运行

git fetch origin
git rebase origin/master
sbt clean compile script

假设你在osx分支上。

于 2015-05-05T15:01:58.767 回答