0

我正在使用 Z3（2012-12-21 git 版本，最新的“主”版本）检查工具的可移植性，因此尝试在 Sparc64 上编译 Z3。我不得不摆弄，src/util/hwf.cpp以便它将 Sparc64 而不仅仅是 IA64 视为缺少 SIMD 内在函数和emmintrin.h. 编译成功。

不幸的是，生成的可执行文件在启动时崩溃，并在prime_generator::prime_generator(). 我不知道为什么。

Program received signal SIGBUS, Bus error.
0x009b1dac in global constructors keyed to _ZN15prime_generatorC2Ev ()
(gdb) bt
#0  0x009b1dac in global constructors keyed to _ZN15prime_generatorC2Ev ()

这对我来说不是很重要（我们的机器是 x86 或 x86-64），但可能与某些嵌入式应用程序相关。

4

1 回答 1

1

我认为在非 x86 机器上运行 Z3 没有任何兴趣，因此您很可能会发现一些问题。

特别是 SPARC 不允许像 x86 那样进行未对齐的内存访问。通过快速浏览，我可以看到未对齐的几个点可能来自。例如，memory::allocate() 通过 sizeof(size_t) 取消对齐 malloc 返回的指针。如果那不是 64 位，那么它将崩溃（因为 svector 数据）。然后，svector分配，也在数据前保留2*sizeof(unsigned)。如果 2*sizeof(unsigned) 不是 sizeof(uint64) 的倍数，那么你会崩溃。

等等。关键是，如果没有更多信息，就不可能为您提供帮助。您需要使用 -g 进行编译，如果需要，打印崩溃的汇编代码以帮助确定确切的位置。

另外，请不要使用主分支。那是很老了。请考虑使用不稳定的分支（它并不像名字听起来那么糟糕：）

于 2014-02-12T10:56:13.873 回答