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 回答