0

我正在尝试在我们客户的专有安全关键系统模块上应用 frama-c/jessie。正在分析的函数非常大（图像 700 未注释的行数）有很多条件语句以及复杂的（&&、|| 等）。

我在 Ubuntu VM 64 位机器上运行它时收到此错误消息。似乎错误 137 与内存大小等有关。但我不太确定。

非常感谢任何有关如何处理此错误的建议。

[

formal_verification]$ frama-c -jessie  test.c
[kernel] preprocessing with "gcc -C -E -I.  -dD test.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir test.jessie
[jessie] File test.jessie/test.jc written.
[jessie] File test.jessie/test.cloc written.
[jessie] Calling Jessie tool in subdir tests.jessie
Generating Why function testFun
[jessie] Calling VCs generator.
gwhy-bin [...] why/test.why
Computation of VCs...
Killed
make: *** [test.stat] Error 137
4

1 回答 1

1

有很多条件语句以及复杂的（&&、|| 等）。

在分析具有大量嵌套条件的函数时，您应该使用所谓的“快速 WP”选项。否则，目标甚至不需要很大就可以引起爆炸。

它恰好是Jessie 手册中将选项传递给 Why 的示例（它实际上是一个 Why 选项）：

-jessie-why-opt=<s>
give an option to Why (e.g., -fast-wp)

因此，您将使用-jessie-why-opt=-fast-wp.

于 2014-01-01T10:37:42.527 回答